The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Monday 13 September 2010 12:25:05 pm Randy Pollack wrote:

> > I don't know what you mean by "outermost".
> 
> Universe polymorphism is analagous to Hindley-Milner type
> polymorphism; i.e. outermost (implicit) quantification.

Oh, in that case, Agda allows more than that:

  foo : (T    : (i : Level) → Set i → Set i)
      → (nil  : (i : Level) → (S : Set i) → T i S)
      → (cons : (i : Level) → (S : Set i) → S → T i S → T i S)
      → T (suc (suc zero)) Set₁
  foo T nil cons = cons (suc (suc zero)) Set₁ (T (suc zero) Set₀)
                  (nil (suc (suc zero)) Set₁)

  data List (i : Level) (A : Set i) : Set i where
    []   : List i A
    _::_ : A → List i A → List i A

  l : List (suc (suc zero)) Set₁
  l = foo List (λ i S → []) (λ i S → _::_) -- List (suc zero) Set :: []

-- Dan