Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Unexpected universe level assignment

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unexpected universe level assignment


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page