[Agda] Why aren't free vars in types automatically generalized

[Darin Morrison]

Hi Stefan,

On Fri, Mar 27, 2009 at 11:42 PM, Stefan Monnier
<monnier at iro.umontreal.ca> wrote:
> Coming from Twelf and ML, I keep wondering why I have to write:
>
>   data Ω : ℕ → Set where
>     tNat  : ∀{l} → Ω l
>     tArw  : ∀{l} → Ω l → Ω l → Ω l
>     tPoly : ∀{l} → Ω (suc l) → Ω l
>     tVar  : ∀{l} → Fin l → Ω l

Although not quite what you want, you can come close:

  data Ω (l : ℕ) : Set where
    tNat  : Ω l
    tArw  : Ω l → Ω l → Ω l
    tPoly : Ω (suc l) → Ω l
    tVar  : Fin l → Ω l

> Even more so for things like
>
>   data TExp : ∀{l} → TEnv l → Ω l → Set where
>     teLit  : ∀{l Γ} → ℕ → TExp{l} Γ tNat
>     ...

You may be able to write something like:

  data TExp {l} {Γ} : TEnv l → Ω l → Set where
    teLit  : ℕ → TExp Γ tNat


-- 
Darin