[Agda] Pattern-matching operation order

[Pierre Boutillier]

Hi list,
Andreas Abel and I have face the problem that using Agda 2.2.6 with  
the definitions :

data Nat : Set where
   zz : Nat
   ss : Nat → Nat

_+_ : Nat -> Nat -> Nat
zz + n = n
ss m + n = ss (m + n)

data _<_ : Nat → Nat → Set where
    LE : ∀ {i} → (d : Nat) → i < (d + i)

the definition :

minus : ∀ {m n} → m < n → Nat
minus (LE d) = d

typechecks but :

minusSS : ∀ {m n} → m < (ss n) → Nat
minusSS .{ss n}{n} (LE {ss .n} zz) = {!zz!}
minusSS a = ?

doesn't.
The reason seems to be that the unification problem n =?= d + i has a  
"most general" success whereas ss n =?= d + i doesn't.
Nevertheless, why in our case the contraints i =?= ss n and d =?= zz  
then zz + ss n \beta= ss n are not given before  ss n =?= d + i. There  
must be examples where things have to be done in the order used by  
Agda but I can't find any by myself !

All the best,
Pierre
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PBMatch.agda
Type: application/octet-stream
Size: 371 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100217/975073b8/PBMatch.obj
-------------- next part --------------