coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Unexpected universe level assignment
- Date: Mon, 17 Jul 2017 11:12:53 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT ens-lyon.fr; spf=Neutral smtp.mailfrom=gaetan.gilbert AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
- Ironport-phdr: 9a23:EvpF9hRSEh8m9nZPqsP5ZFyS0dpsv+yvbD5Q0YIujvd0So/mwa69bB2N2/xhgRfzUJnB7Loc0qyN4v+mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/nzJhMx+jKxVoxyvqBJwzIHWfI6bO+Fzfr/ecN4AWWZNQshcWi5HD4ihb4UPFe0BPeNAoof8vVQBswe+ChOqBOjyyzFIh3v20rYk3OQ7DQHNwQstH90Uv3vKsNX6LqESXfq6zKnJyTXMdO1Z2S3h6IXTbB8hp+qMUat0ccvRzkkvERnJjluKqYH8OT6ey+oDs2+e7+V6VOKvjXYqqwB3oji1x8cjkJPFhowPyl3C6C53w541KMWlREN0fdKoCplduiOAO4drQ84vQXtktDgkxrEYoZK2fTYGxI46yxLDdfCLaZWE7x3gWeqLPDt1hWxpdbSijBio60eg0PfzVsys3VZKsCVFlt7Mu2gJ1xPJ8ceIUeVy8l2/1jaJzADf8+VEIEAzlardMZIhzKQwmoISsUTFACD2hF37gLKZe0k44OSl6ebqbq/7qpKdNYJ4kB/yProwlsCnBOQ3KAkOX2yV+eSm073j+FX0QLpQgfIojqnWqpbaKd4Upq64Bw9ayZgs6wyjDzq9ztsYm2IHIEtBeBOHiIjpPUvCIP7iDfunmVSjjC9rx+zaPr3mGpjCMn/DkK74cblh705c1RE8wMtE55NUD7EBOOj8VlXwtNzeFB85Mha7z/zpCNVnhcsiXjeEBbbcO6fPu3eJ4PguKq+Cftw7ojH4ftcs6uLnizcWmFsXcLO1lc8YYX2kF/IgLESda3f2nv8MF3xPuhs5SqrkkgvRAnZoe3+uUvdktXkAA4W8ANKbSw==
It's a consequence of a minimization heuristic. See https://coq.inria.fr/refman/Reference-Manual032.html#sec807
You can do [Unset Universe Minimization ToSet] as the link says or you can make the universe explicit so that it won't be unified with Set.
Gaëtan Gilbert
On 14/07/2017 13:16, Dominik Kirst wrote:
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
- Re: [Coq-Club] Unexpected universe level assignment, Gaetan Gilbert, 07/17/2017
Archive powered by MHonArc 2.6.18.