The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hello,

I stumbled across another universe behavior where I am not sure whether
this is a bug or not.

I have declared a bunch of Universes, say L,S,M and U and used them in a
bunch of definitions. This ensures that U,S <= L as can be witnessed by:

Fail Constraint L < S.
Fail Constraint L < U.

Now I can enforce S = L before some definition:

Constraint S = L.
Definition foo := Foo Type@{U} ... (@eq)
Constraint S = L.

In this case, everything typechecks. However, if I remove the first
line, then the universe constraints imposed by foo change (become
stronger) and the third line yields a universe inconsisteny.

In the first case, the constraints imposed by foo are:
  U < M and U <= Coq.Init.Logic.8 (the argument of eq)

Without the constraint "S = L", I get
  U < M and U = Coq.Init.Logic.8

So S = L is consistent with foo, but ruled out by it unless enforced before.

The concrete example is again too large, but having discovered the
"Constraint" command, coming up with a reasonably sized example may be
feasible.

Best,
Christian

PS. It would be nice if the automatically generated universe names were
actually names in the Coq sense, so that one could use them with the
Constraint command.

On 10/09/18 14:53, Matthieu Sozeau wrote:
> Dear Christian,
> 
> There is documentation in dev/doc/universes about the changes necessary.
> The main idea is that if your tactic produces a term with polymorphic
> constants in it, it must produce one fresh instance of the constant at
> each use. Before giving the final proof term containing those fresh
> instances, you can call a type inference function to gather the universe
> constraints necessary for the whole term to typecheck automatically.
> Maybe a look at the OCaml code you use could help us fix this.
> The « cannot ensure that i <= j » error could also be because that
> constraint is not present in the graph you produce in a tactic I believe.
> 
> The order-of-Imports issue is a bug for sure. Note that if you have a
> module A with everything polymorphic then importing it incurs no global
> constraints so the bug couldn’t happen in that case.
> 
> Best,
> — Matthieu
> Le lun. 10 sept. 2018 à 14:28, Christian Doczkal
> <christian.doczkal AT ens-lyon.fr
>  
> <mailto:christian.doczkal AT ens-lyon.fr>>
>  a
> écrit :
> 
>     Hi,
>     >> - Require Import A B. succeeds
>     >> - Require Import B A. fails
>     >
>     > That sounds like a bug, you can open an issue on github with
>     > reproduction instructions and we will look into it.
> 
>     Unfortunately, that's an internal repository with well over 10K lines,
>     and the problem occurs at the end. Should I manage to find a small
>     example, I will open an issue.
> 
>     >> globalization of polymorphic reference <ID> would forget universes.
>     >
>     > Unfortunately various tactics and commands do not support or badly
>     > support universe polymorphism. This error means some function hasn't
>     > been adapted. It should probably be an anomaly.
>     > Depending on what exactly is failing it may be possible for us to fix
>     > it, or it could be beyond our current manpower.
> 
>     This happens when calling one of our own tactics written in OCaml. So
>     how does one have to adapt tactics in order to properly support universe
>     polymorphism? (The error occurred while trying to see what happens if I
>     make just about everything universe polymorphic, so it may or may not be
>     necessary to fix this)
> 
>     Thanks for the pointers,
>     Christian
>