[Agda] Absurd catch all pattern

[Andreas Abel]

To save myself O(n^2) impossible cases, I'd like to write something like

module CatchAllAbsurdPattern where

data Zero : Set where

record One : Set where

data Three : Set where
   zero : Three
   one  : Three
   two  : Three

Eq : Three -> Three -> Set
Eq zero zero = One
Eq one one = One
Eq two two = One
Eq _ _ = Zero

sym : forall x y -> Eq x y -> Eq y x
sym zero zero H = H
sym one  one  H = H
sym two  two  H = H
sym _    _   ()

The last line is rejected by Agda, since it cannot see that Eq x y is  
empty in the catch-all case.

Is it thinkable to get this accepted?  From my half-knowledge on the  
pattern completeness checker I know that Agda splits on arguments  
during type-checking patterns.  So if it split the catch-all clause as  
well (which it has to do to arrive at a case-tree), it would find  
nothing to complain.  Ulf?

Cheers,
Andreas


-------------- next part --------------
A non-text attachment was scrubbed...
Name: CatchAllAbsurdPattern.agda
Type: application/octet-stream
Size: 361 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100304/0aa12ade/CatchAllAbsurdPattern.obj
-------------- next part --------------




Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41