coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Unexpected universe level assignment

From: Dominik Kirst <kirst AT ps.uni-saarland.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Unexpected universe level assignment
Date: Fri, 14 Jul 2017 13:16:19 +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:OoIR0RZqtUt4bwGI3kdgKO//LSx+4OfEezUN459isYplN5qZoMi6bnLW6fgltlLVR4KTs6sC0LuJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57G7ZhcN/gr9YrhyvuRJxxJXZYJ2MNPp7Yq/dfc8WSGhHU81MVyJBGIS8b44XAuQPOuZYqoj9p10PrRu9GAKiAeLvyiVThn/qwKY31OchEQDc3Aw7A9IDq2zUrM7vOKcPV+C1zbDEzS7ZYPxMwzf97JLHchY8rv2WQL1/b9PcxE8yHA3GllWdsZHpMj2a2+gXt2WW7vBsWOC1h2Mptg19uiWjy8kjh4XTgo8Yy0rI+Th6zYs0P9G0VVJ3bcOiHZBNrS+VLZF2TdknQ2xwuCY11LkGuZmjcSgWyJQo2R/fZOadf4iS4xPvTvuRITF5hH58Y7KwnQy98VKkyuLmUMm7zUxGoTdbndXUt3AN0QLc6tSfR/dg8Eqs1iyD2gTS5+1eI004j6TWJ4M5zr41jJUTsEDDHiHsmEXxia+bbkYk+umy6+T8frXrvYecN5RuhgHjNKQum9WzAf8iPQcURWib/f6z1Lv+8kHjXbpFkOU6krPFv5DCOcQbuqm5DhdJ3YYk8hazFiup0NAFnXYcN19FYxKGj43xO17UOvz4DPG/g06tkDhx3fzGMKfhUd3xKS3Il66kdrJg4WZdzhAyxJZR/cF6ELYEdd70X073td+QLR4jKBD8l+XmEs5h/psFH3+JA+qCOarItVaO6qQjLr/fN8cupD/hJq19tLbVhngjlApFcA==

Hello,

the following code produces some unexpected behaviour:

——

Set Universe Polymorphism.
Set Printing Universes.

Inductive Tree : Type :=
| sup : forall X : Type, (X -> Tree) -> Tree.

Definition pair s t :=
@sup bool (fun b => if b then s else t).

About pair.

"pair@{} : Tree@{Set} -> Tree@{Set} -> Tree@{Set}"

——

Although the function “pair" is inferred to be universe-polymorphic, the
input trees and return trees are restricted to Set. This should not be the
case since the operation is valid for all universe levels. In fact, other
operations such as union and power (that do not refer to explicit types like
bool in their definitions) are typed correctly. Is that intended or a bug?

Thanks for your help,
Dominik Kirst

[Coq-Club] Unexpected universe level assignment, Dominik Kirst, 07/14/2017
- Re: [Coq-Club] Unexpected universe level assignment, Gaetan Gilbert, 07/17/2017
  - Re: [Coq-Club] Unexpected universe level assignment, Dominik Kirst, 07/17/2017