[Agda] another possible without-K problem

[Jason Reed]

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