[Agda] Yet another way Agda --without-K is incompatible with univalence

[Nils Anders Danielsson]

On 2014-01-17 12:19, Jesper Cockx wrote:
> test : {e : myPoint ≡ myPoint} → (a : Foo e) → (i : a ≡ a) → i ≡ refl
> test foo refl = refl

This definition contains a hidden dot pattern:

   test : {e : myPoint ≡ myPoint} → (a : Foo e) → (i : a ≡ a) → i ≡ refl
   test .{e = refl} foo refl = refl

The example would have been rejected if the --without-K analysis had
been applied to the dot pattern.

-- 
/NAD