coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Unexpected restriction in universe-polymorphic definition, Dominik Kirst, 09/13/2017
- Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition, Guillaume Melquiond, 09/14/2017
- Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition, Amin Timany, 09/14/2017
- Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition, Dominik Kirst, 09/18/2017
- Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition, Amin Timany, 09/14/2017
- Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition, Guillaume Melquiond, 09/14/2017
Archive powered by MHonArc 2.6.18.