The Coq mailing list

[Tillmann Rendel <rendel AT cs.au.dk>]

Adam Chlipala wrote:
> Coq includes a kind of fake, "template-style" universe polymorphism, 
> where inductive definitions are effectively copied automatically to make 
> it possible to use [Set] instead of [Type] in some places.  The Coq 
> type-checker automatically detects opportunities to do this.

Lauri Alanko wrote:
> This is explained in the manual:
>
> http://www.lix.polytechnique.fr/coq/distrib/current/refman/Reference-Manual006.html#@default345

That's very interesting. I guess it could help with certain universe 
inconsistencies I experienced lately. But I find the behavior of the 
typechecker somewhat confusing.

For example, with the standard definition of [option].

  < Inductive option (A : Type) : Type :=
  <   | Some : A -> option A
  <   | None : option A.

We cannot define an optional [option].

  < Check (Some _ option).
  > Error: Universe inconsistency.

However, it works after eta-expanding [option]:

  < Check (Some _ (fun A => option A)).
  > Some (Type -> Type) (fun A : Type => option A)
  >      : option (Type -> Type)

I guess this because the new rule Ind-Family is triggered by the term 
[option A], but still, this behavior is not very intuitive. Would it be 
possible to extend Ind-Family to cover such cases? (If not, why not?)

Thanks,
  Tillmann