[Agda] Divergence in inference with constructor-headed functions

[Brandon Moore]

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