[Agda] Type and termination checking around with clauses

[Nils Anders Danielsson]

On Wed, Apr 30, 2008 at 2:24 AM, Peter Berry <pwberry at gmail.com> wrote:
>
>  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?

I suggested a fix for this problem:

http://code.google.com/p/agda/issues/detail?id=59

However, Ulf didn't approve of my hand-waving. :)

I'm becoming more and more convinced that, in the long run, we should
aim for some more semantic or type-based termination criterion, to
avoid having to deal with these syntactic nuisances.

-- 
/NAD