[Agda] type inference error?

[Peter Divianszky]

Hi,

Is the following a known error in Agda?
My student have found this.

---------------------------------------
data ℕ : Set where
   zero : ℕ
   suc : ℕ → ℕ

data _≡_ {A : Set} (x : A) : A → Set where
   refl : x ≡ x

data ⊥ : Set where
   suc : ⊥ → ⊥

-- it looks like Agda can't tell (suc : ℕ → ℕ) apart from the other suc
-- this is unreasonable: the type of suc should be inferred from the
-- fact that (x : ℕ)

lemma : (x : ℕ) → suc x ≡ suc x
lemma _ = refl
---------------------------------------


Peter