[Agda] Divergence in inference with constructor-headed functions

[Andreas Abel]

Hello Brandon,

thanks for the report.  I cannot reproduce the behavior you describe on 
the darcs version of Agda.  Type checking is instantaneous and yields 
yellow:

_26 : ℕ
_28 : f _26

So, probably you have to pull the darcs version or wait for the next 
release if this bug in 2.2.10 is critical for you...

Cheers,
Andreas


On 7/27/11 9:05 PM, Brandon Moore wrote:
> Hello
>
>
> In 2.2.10 the following code seems to cause typechecking
> to diverge.
>
> \begin{code}
>
> f : ℕ → Set
> f zero = ⊤
> f (suc n) = ℕ × f n
>
> enum : (n : ℕ) → f n
> enum zero = tt
> enum (suc n) = n , enum n
>
> n : ℕ
> n = _
>
> test : f n
> test = enum (suc n)
> \end{code}
>
> This typechecks quickly if the definition
> of test is changed to
>
>
> test = enum n
>
> (If you previously tried to typecheck the code again, the*ghci*
> process will still be stuck, and must be killed or interrupted first)
>
>
> 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.
>
>
> Here is the module header and self-contained definitions
> for the code above
>
>
> \begin{code}
>
> module infbad where
>
> data ⊤ : Set where
>    tt : ⊤
>
> data ℕ : Set where
>    zero : ℕ
>    suc : ℕ → ℕ
>
> data _×_ (A B : Set) : Set where
>    _,_ : A → B → A × B
> \end{code}
>
> Brandon

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/