[Agda] another possible without-K problem

Jason Reed jcreed at gmail.com
Tue Jul 9 17:31:22 CEST 2013

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

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

{-# 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

Note that this covers both the possible definitions of the identity type
mentioned by Guillaume in

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/20130709/a876c4f7/attachment.html

More information about the Agda mailing list