[Agda] ANNOUNCE: Agda 2.2.10

[Dan Doel]

On Tuesday 22 February 2011 12:16:16 PM Andreas Abel wrote:
> On 2/22/11 4:12 PM, Jean-Philippe Bernardy wrote:
> > I tried to define:
> > 
> > data Eq (A : Set) (a : A) : .A ->  Set where
> > 
> >    refl : Eq A a a
> 
> This should be rejected by Agda, so this is where the bug is located.
> If you spell this out it means
> 
>    data Eq A a .b : Set where
>      refl : a == b -> Eq A a b
> 
> but b is declared irrelevant.  I will have to revisit irrelevant family
> indices!

This definition should simply not be allowed, I'd say. If we think about:

  Eq A a : .A -> Set

then this means that the second A should be irrelevant for the purpose of 
determining what _set_ is returned. Which implies that Eq A a b and Eq A a c 
should be in some sense the same set even if b and c are different. But this 
is clearly not what Eq is trying to accomplish. It'd only work in incidental 
cases (A = Top for instance).

Types like .A -> Set can make sense, but it is essentially specifying that the 
A is phantom.

  data K (A : Set) .(B : Set) : Set where
    k : A -> K A B

And I'm not really certain that this is even useful.

-- Dan