[Agda] Dealing with HOAS

[Vag Vagoff]

How to express syntax of Simply Type Lambda Calculus using HOAS?

This encoding gives an error about Exp on left side of ->:

data Typ : Set where
_⟶_ : Typ → Typ → Typ
type : String → Typ

data Val : Typ → Set where
num : ℕ → Val Int

data Exp : Typ → Set where
val : ∀ {t} → Val t → Exp t
lam : ∀ {t₁ t₂} → (Exp t₁ → Exp t₂) → Exp (t₁ ⟶ t₂)
app : ∀ {t₁ t₂} → Exp (t₁ ⟶ t₂) → Exp t₂ → Exp t₁

How to hack this representation to get rid of error?