[Agda] non-constructor indices

[Ulf Norell]

Dan wrote:

> height : Indexed Z -> Nat
> height B = Z
>

The error message (which shouldn't involve panicking) tells you that you
can't pattern match on the argument, because the type checker can't figure
out if I is a valid constructor. In order to do this it would have to solve
the unification problem Z = plus n m, which it can't.

The problem is that the index isn't a variable, which makes the unification
problem too hard. The standard trick is to make the index a variable:

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

height' : {n : Nat} -> Indexed n -> n == Z -> Nat
height' B             refl = Z
height' (I {Z}   l r) refl = ?  -- you forgot about this case
height' (I {S n} l r) ()        -- impossible case

height : Indexed Z -> Nat
height i = height' i refl

In the I case (which you left out) we need to match on the size of the left
sub-tree in order to be able to inspect the proof object. The reason your
version of this approach didn't go through is that you need to *first* match
on the tree and *then* on the proof object (otherwise we're back in the same
situation as we started in). Pattern matching happens from left to right, so
you need the proof argument to appear after the tree argument.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20080116/d86a3bd4/attachment.html