[Agda] another possible without-K problem

[Altenkirch Thorsten]

This looks like a bug ¡V please add it to the bug tracker.

We really need to understand what we are doing when checking wether pattern satisfy the ¡Xwithout-K condition. It seems that Conor's work on translating pattern matching to eliminators (with J and K) would be a good starting point.

At the same time we know that many types support UIP by structure. Michael Hedberg showed that all types with a decidable equality support UIP and it is not hard to see that this can be extended to stable equality (non-not closed). (Little puzzle: without extensionality ¡V are there any types which have stable but not decidable equality ?)

We also want to quantify over all HSets (I.e. types with UIP) and so on.

Thorsten

From: Jason Reed <jcreed at gmail.com<mailto:jcreed at gmail.com>>
Date: Tue, 9 Jul 2013 16:31:22 +0100
To: "agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>" <agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>>
Subject: [Agda] another possible without-K problem

I'm experiencing something that I think is a violation of the intent of the --without-K flag, similar to what Thorsten was talking about in https://lists.chalmers.se/pipermail/agda/2012/004104.html.

The following file checks fine for me under current darcs Agda:

<<<begin>>>
{-# OPTIONS --without-K #-}

module Test where

data S1 : Set where
    base : S1

module test where
   data _¡Ý_ {A : Set} (a : A) : A ¡÷ Set where
    refl : a ¡Ý a

   bad : (p q : base ¡Ý base) -> p ¡Ý q
   bad refl refl = refl

module test2 where
   data _¡Ý_ {A : Set} : A ¡÷ A ¡÷ Set where
       refl : {x : A} ¡÷ x ¡Ý x

   bad : (p q : base ¡Ý base) -> p ¡Ý q
   bad refl refl = refl
<<<end>>>

Note that this covers both the possible definitions of the identity type mentioned by Guillaume in https://lists.chalmers.se/pipermail/agda/2012/004105.html

Any ideas what should be done here? Does the K-check need to be further strengthened when there aren't parameters around? Am I misunderstanding something trivial?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130710/1b466a62/attachment.html