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

[Stefan Monnier]

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

rather than

   data Ω : ℕ → 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
     ...

where I'd much rather write just

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

It seems it would be easy to make such a change (just collect the free
vars, sort them topologically, and tuck them in front), so ...
where's the catch?


        Stefan