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

[Carsten SchŸuermann]

Hi all,
>> As mentioned, Twelf has been doing this for years
> Does the Twelf approach ever give rise to any surprises? Do people stay
> away from certain kinds of definitions because they would be hard to
> interpret? (This is not necessarily a bad thing: Giving people the
> ability to shoot themselves in the foot can be useful, if you get
> something else in return.)
I don't think so.  In Twelf you always have the choice to make implicit 
arguments explicit.
You may write (in the type preservation example)

tps : eval E V -> of E T -> of  V T -> type.

or

tps : {E:exp}eval E V -> of E T -> of  V T -> type.

or

tps : {E:exp}{V:exp}{T:exp}eval E V -> of E T -> of  V T -> type.

Whichever option you choose, Twelf requires you to stick with your 
choice.   Let evz : eval z z, ofz : of z nat.  In the base case (z 
evaluates to z) case, you need to write

tpz : tps evz ofz ofz.

or

tpz: tps z evz ofz ofz.

or

tpz: tps z z nat evz ofz ofz.

respectively.  If arguments can be determined by higher-order 
unification (which they can here), you may also write.

tpz: tps _ _ _ evz ofz ofz.

instead of the third case, where _ should be read as logic variable.  
Twelf will let you know if it cannot infer the instantiation of _ / what 
you meant.  Then you have to provide additional information (e.g. in 
form of type ascriptions).

I hope this clears things up.
Best,
-- Carsten