[Agda] This works in Idris by not in agda. (updating the type from the values of the constructor)

[Roman]

If you postpone unication a bit, `tn` type checks:

open import Relation.Binary.PropositionalEquality

data Test : ℕ → Set where
  Tist : Test zero
  Tostq : ∀ {m} → (n : ℕ) → m ≡ fn n → Test m

pattern Tost n = Tostq n refl

tn : (n : ℕ) → Test (fn n) → ℕ
tn zero  Tist          = zero
tn zero (Tost  zero)   = zero
tn zero (Tost (suc n)) = zero
tn (suc y) x = {!!}

Is Agda's unifier too eager in this case?