[Agda] Type and termination checking around with clauses

[Ulf Norell]

On Wed, Apr 30, 2008 at 3:24 AM, Peter Berry <pwberry at gmail.com> wrote:

>
> 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?
>

Yeah, this is a known issue. It wouldn't work even when the as-pattern bug
is fixed. We have some vague ideas on how to solve the problem but nothing
concrete yet.

A possible work around might be to include the recursive calls in the with
clause (untested):

merge (x :: xs) (y :: ys) with x <= y | merge xs (y :: ys) | merge (x :: xs)
ys
... | true   | rec | _ = x :: rec
... | false | _ | rec = y :: rec

This isn't very nice, but at least it should make the termination checker
happy. Of course, in this particular case an if_then_else_ would also work.

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.)


If p : P l then in ?1 you should have p : P (x :: xs). If you don't there's
a bug. A concrete example might be helpful.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080430/a91d4ca5/attachment-0001.html