[Agda] Divergence in inference with constructor-headed functions

[Nils Anders Danielsson]

On 2011-07-27 21:05, Brandon Moore wrote:
> I think the problem is that the body has type ℕ × f n,
> and unifying it with the expected type f n invokes the
> constructor-headed function specialization to resolve
> n to suc n', and the process repeats.

Yes, this is what happens.

The problem still exists in the development version:

   mutual

     n : ℕ
     n = _

     test : f n
     test = enum (suc n)

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

-- 
/NAD