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

[Stefan Monnier]

>> Whichever option you choose, Twelf requires you to stick with your choice.
> Assuming that we have the definitions

>  Ctxt : Set
>  Ty   : Ctxt → Set
>  Tm   : Ty Γ → Set  (meaning ∀ {Γ} → Ty Γ → Set)
>  ⋆    : Ty Γ        (meaning ∀ {Γ} → Ty Γ),

> does this mean that there is no direct way to write
>  El : ∀ {Γ} → Tm (⋆ {Γ}) → Ty Γ  ?

Indeed: Twelf does not provide the user any way to explicitly specify an
implicit argument.  So you wouldn't define

    ⋆    : Ty Γ
but
    ⋆    : ∀ (Γ) → Ty Γ

I haven't used Twelf enough to know if it occurs often that parameters
can usually be inferred, but not always.

The choice of how to pass implicit args explicitly (in the case of
Twelf: never) and the use of free-vars-are-implicit-args are mostly
independent, AFAIK.  Except obviously that if you can't pass implict
args explicitly, you don't need to worry about ordering of
implicit args.


        Stefan