[Agda] Re: 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

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

[...]

Thanks, it partly helps.  But it doesn't really answer the question
about "why it's not done as in Twelf and HM"?


        Stefan