The Coq mailing list

[Dominik Kirst <kirst AT ps.uni-saarland.de>]

Hello,

checking the following code puts an unexpected restriction on the codomain of the function emb’:

_____________________________________________

Set Universe Polymorphism.

Inductive Tree : Type :=

  sup : forall A : Type, (A -> Tree) -> Tree.

Fixpoint emb' (s : Tree) :=

  let (A, f) := s in

  sup A (fun a => emb' (f a)).

Fail Definition T :=

  sup Tree emb'.

Monomorphic Universe U1 U2.

Fixpoint emb (s : Tree@{U1}) : Tree@{U2} :=

  let (A, f) := s in

  sup A (fun a => emb (f a)).

Definition T :=

  sup Tree emb.

_____________________________________________

Tree is universe-polymorphic and emb’ is supposed to embed smaller copies of Tree into larger copies. However, both the domain and codomain get assigned the same universe level and so defining a tree T as supremum of emb’ fails.

When tagging the function type explicitly with two (unconstrained) universe variables, the exact level of the codomain is kept variable and the supremum becomes definable. Is this behaviour an intended minimisation?

Thanks,

Dominik