[Agda] Type and termination checking around with clauses

[Peter Berry]

module MergeNonterm where

{- Booleans. -}
data Bool : Set where
  false : Bool
  true  : Bool

{- Natural numbers. -}
data ℕ : Set where
  Z : ℕ
  S : ℕ -> ℕ

{- Ordering of natural numbers. -}
_<=_ : ℕ -> ℕ -> Bool
Z   <= n   = true
S _ <= Z   = false
S n <= S m = n <= m

{- Lists. -}
data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

infixr 30 _::_

merge : List ℕ -> List ℕ -> List ℕ
merge xs        [] = xs
merge []        ys = ys
merge (x :: xs) (y :: ys) with x <= y -- should be l@(x :: xs) but for the bug
... | true  = x :: merge xs (y :: ys)
... | false = y :: merge (x :: xs) ys


These last two lines trip the termination checker. Clearly the
arguments are (as a whole) strictly smaller, but a new list is made,
which presumably makes the termination checker think they're getting
bigger. With at-patterns in with clauses working properly (i.e. bug 56
fixed, see http://code.google.com/p/agda/issues/detail?id=56) and
using l instead of x :: xs, would it pass? Or are there plans to make
the checker spot this kind of 'reconstructing patterns'? Is that even
feasible?

Possibly related: suppose I have a 'with' clause, say

contrived (dprod l p) with l
... | [] = ?0
... | x :: xs = ?1

where p : P l for some function P : List ℕ -> Set, say a property
which p is a proof of, and somewhere in ?1 I need something of type P
(x :: xs) (like a proof of the same property). Clearly x :: xs = l so
p will do, but somehow the type checker misses this - it won't unify P
l = P (x :: xs). (If you want a concrete example I can provide one.)

-- 
Peter Berry <pwberry at gmail.com>
Please avoid sending me Word or PowerPoint attachments.
See http://www.gnu.org/philosophy/no-word-attachments.html