Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Unexpected restriction in universe-polymorphic definition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Unexpected restriction in universe-polymorphic definition


Chronological Thread 
  • From: Dominik Kirst <kirst AT ps.uni-saarland.de>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Unexpected restriction in universe-polymorphic definition
  • Date: Wed, 13 Sep 2017 10:26:04 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kirst AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=kirst AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT theia.rz.uni-saarland.de
  • Ironport-phdr: 9a23:sZT7CBxeJ8RNNLrXCy+O+j09IxM/srCxBDY+r6Qd0uwXIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2NBXupSi56idXERHiPyJ0IP70E8jclZeZzee3rrHUZgROhTn1QrJoNwn++QbQrNIKqZN5bLs3y17Sq3JSf+1QySVkKATAzF7H+s6s8cs7oGxrsPU7+psYXA==

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



Archive powered by MHonArc 2.6.18.

Top of Page