[Agda] ANNOUNCE: Agda 2.2.10

[Dan Doel]

On Tuesday 22 February 2011 8:28:50 PM Dan Doel wrote:
> Is it? Here's the situation I can come up with in which it could actually
> be used:
> 
>   foo : (A : Set) (x : A) .(y : A) -> Eq A x y -> ...
>   foo A x .x refl = ...

Sorry for the reply-to-self. I've been thinking about this, and I think it 
still may be fishy. Essentially what it's doing is saying, "we're not supposed 
to care what y is, but when we match on the Eq term, we might as well assume 
it's x." However, consider the following:

  El : Fin 3 -> Set
  El 0 = Empty
  El 1 = Unit
  El 2 = Bool

So, this turns Fin 3 into a simple universe of sorts. And using the dependent 
version of the irrelevant types, we should be able to write an id that is 
guaranteed to be parametric:

  id : .(n : Fin 3) -> El n -> El n
  id n x = x

we can't do case analysis on n, because it's irrelevant. But, what if we do 
this:

  foo : .(n : Fin 3) -> Eq (Fin 3) 0 n -> El n -> El n
  foo .0 refl x = ?

Now what. Should we treat n as if it's 0? That has implications in the type of 
x. If we do treat it that way, then the following makes sense as a definition:

  foo .0 refl ()

but then what happens when we call foo as:

  foo 2 refl false

And we can, because refl proves Eq (Fin 3) 0 2. So allowing the Eq to refine 
even the irrelevant variable seems to have been a bad decision.

To tie this together, what if we try to use squash equality? Then we have to 
write:

  foo : (sn : Squash (Fin 3)) -> Eq (Fin 3) 0 sn -> El (out sn) -> El (out sn)

Assuming we can even project out of the Squash in this way. Then we write:

  foo .(squash 0) refl x = ?

Now, we've assumed that sn = squash 0. What is out (squash 0)? According to 
Andreas' proposed desugaring of irrelevant projections, I believe it's 
something like 'irr (squash 0)' for an opaque builtin/postulate irr. 
Importantly, it isn't 0. x has type 'El (irr (squash 0))' with which we can't 
do anything but write:

  foo .(squash 0) refl x = x

Anyhow, this is tricky business.

-- Dan