[Coq-Club] Debugging Universe Inconsistencies

[Christian Doczkal]

Hello everyone,

We have a large development where we have generic structures and some
concrete instances for them. One of these is for relations (X -> Y ->
Prop) with (X,Y : Set).

Now I was trying to generalize this to all instances with (X,Y : Type).
This leads to a universe inconsistency thousands of lines down the road.
I would hope that this is merely a problem of making certain things
universe polymorphic, but I don't manage to come up with a minimal
example reproducing the problem.

At first, I only got the rather uninformative "Universe Inconsistency"
error when trying to load two separately compiled parts of the library.

With some trial and error I got to the point where I have statement that
type checks before the generalized instances are imported and fails to
type check afterwards. This gives me an Error of the form:

"... cannot ensure that "Type@{foo.2}" is a subtype of Type@{bar.3}"

I can use "Print Universes" before and after the Import, but that yields
thousands of constraints and even the diff is not too enlightening.

If I understand the universe mechanism and the error message correctly,
this actually means that assuming "foo.2 <= bar.3" is inconsistent with
the current collection of universe constraints. So here are some questions:

1) Is my understanding correct?

2) If yes, is there a way to obtain a minimal (or at least sufficiently
small) subset of the current collection of constraints, proving that
"foo.2 <= bar.3" cannot be consistently added.

3) What other things can I do to shed some light onto what is happening?

Any help would be appreciated.

Best,
Christian

[Gaëtan Gilbert]

1) yes

2) and 3)
if you enable printing of universes (Set Printing Universes. in
coqtop/proof general/etc, some GUI toggle in coqide) universe
inconsistencies should print that information

Gaëtan Gilbert

Post by Christian Doczkal
Hello everyone,
We have a large development where we have generic structures and some
concrete instances for them. One of these is for relations (X -> Y ->
Prop) with (X,Y : Set).
Now I was trying to generalize this to all instances with (X,Y : Type).
This leads to a universe inconsistency thousands of lines down the road.
I would hope that this is merely a problem of making certain things
universe polymorphic, but I don't manage to come up with a minimal
example reproducing the problem.
At first, I only got the rather uninformative "Universe Inconsistency"
error when trying to load two separately compiled parts of the library.
With some trial and error I got to the point where I have statement that
type checks before the generalized instances are imported and fails to
I can use "Print Universes" before and after the Import, but that yields
thousands of constraints and even the diff is not too enlightening.
If I understand the universe mechanism and the error message correctly,
this actually means that assuming "foo.2 <= bar.3" is inconsistent with
1) Is my understanding correct?
2) If yes, is there a way to obtain a minimal (or at least sufficiently
small) subset of the current collection of constraints, proving that
"foo.2 <= bar.3" cannot be consistently added.
3) What other things can I do to shed some light onto what is happening?
Any help would be appreciated.
Best,
Christian

[Gaëtan Gilbert]

Definition T1 := Type.
Definition T2 := Type.
Definition T3 := Type.

Definition T1_le_T2 : T1 -> T2 := fun x => x.
Definition T2_le_T3 : T2 -> T3 := fun x => x.

Fail Definition T3_lt_T1 : T1 := T3.
(* The term "T3" has type "Type" while it is expected to have type "T1"
(universe inconsistency). *)

Set Printing Universes.
Fail Definition T3_lt_T1 : T1 := T3.
(* The term "T3" has type "Type@{Top.3+1}" while it is expected to have
type
"T1" (universe inconsistency: Cannot enforce Top.3 < Top.1 because Top.1
<= Top.2 <= Top.3).
*)


Linking constraints to specific definitions is currently not something
Coq helps you with.

Gaëtan Gilbert

Hello,
I already had used "Set Printing Universes". As far as I can tell, the
only thing "Set Printing Universes" does is cause "Print/Check term." to
print the universe levels of all occurrences of "Type" occurring in a
particular definition as well as the constraints enforced by a
particular definition.
I have a constraint system with thousands of constraints arising from
hundreds of definitions and I would like to know which constraints
contribute to the inconsistency and which definitions/lemmas give rise
to a given constraint.
For instance, Print Universes might mention
"Coq.Relations.Relation_Definitions.1" which I could correctly guess is
relation =
But its not always that easy to guess the definitions introducing a
particular universe index and even harder to guess which definition or
lemma enforces a given constraint.
Best,
Christian

Post by Gaëtan Gilbert
1) yes
2) and 3)
if you enable printing of universes (Set Printing Universes. in
coqtop/proof general/etc, some GUI toggle in coqide) universe
inconsistencies should print that information
Gaëtan Gilbert

Post by Christian Doczkal
Hello everyone,
We have a large development where we have generic structures and some
concrete instances for them. One of these is for relations (X -> Y ->
Prop) with (X,Y : Set).
Now I was trying to generalize this to all instances with (X,Y : Type).
This leads to a universe inconsistency thousands of lines down the road.
I would hope that this is merely a problem of making certain things
universe polymorphic, but I don't manage to come up with a minimal
example reproducing the problem.
At first, I only got the rather uninformative "Universe Inconsistency"
error when trying to load two separately compiled parts of the library.
With some trial and error I got to the point where I have statement that
type checks before the generalized instances are imported and fails to
I can use "Print Universes" before and after the Import, but that yields
thousands of constraints and even the diff is not too enlightening.
If I understand the universe mechanism and the error message correctly,
this actually means that assuming "foo.2 <= bar.3" is inconsistent with
1) Is my understanding correct?
2) If yes, is there a way to obtain a minimal (or at least sufficiently
small) subset of the current collection of constraints, proving that
"foo.2 <= bar.3" cannot be consistently added.
3) What other things can I do to shed some light onto what is happening?
Any help would be appreciated.
Best,
Christian

[Christian Doczkal]

Hello,

I already had used "Set Printing Universes". As far as I can tell, the
only thing "Set Printing Universes" does is cause "Print/Check term." to
print the universe levels of all occurrences of "Type" occurring in a
particular definition as well as the constraints enforced by a
particular definition.

I have a constraint system with thousands of constraints arising from
hundreds of definitions and I would like to know which constraints
contribute to the inconsistency and which definitions/lemmas give rise
to a given constraint.

For instance, Print Universes might mention
"Coq.Relations.Relation_Definitions.1" which I could correctly guess is
the first argument of "relation":

relation =
fun A : Type@{Coq.Relations.Relation_Definitions.1} => A -> A -> Prop
: Type@{Coq.Relations.Relation_Definitions.1} ->
Type@{max(Coq.Relations.Relation_Definitions.1,Set+1)}

But its not always that easy to guess the definitions introducing a
particular universe index and even harder to guess which definition or
lemma enforces a given constraint.

Best,
Christian

Post by Gaëtan Gilbert
1) yes
2) and 3)
if you enable printing of universes (Set Printing Universes. in
coqtop/proof general/etc, some GUI toggle in coqide) universe
inconsistencies should print that information
Gaëtan Gilbert

Post by Christian Doczkal
Hello everyone,
We have a large development where we have generic structures and some
concrete instances for them. One of these is for relations (X -> Y ->
Prop) with (X,Y : Set).
Now I was trying to generalize this to all instances with (X,Y : Type).
This leads to a universe inconsistency thousands of lines down the road.
I would hope that this is merely a problem of making certain things
universe polymorphic, but I don't manage to come up with a minimal
example reproducing the problem.
At first, I only got the rather uninformative "Universe Inconsistency"
error when trying to load two separately compiled parts of the library.
With some trial and error I got to the point where I have statement that
type checks before the generalized instances are imported and fails to
I can use "Print Universes" before and after the Import, but that yields
thousands of constraints and even the diff is not too enlightening.
If I understand the universe mechanism and the error message correctly,
this actually means that assuming "foo.2 <= bar.3" is inconsistent with
1) Is my understanding correct?
2) If yes, is there a way to obtain a minimal (or at least sufficiently
small) subset of the current collection of constraints, proving that
"foo.2 <= bar.3" cannot be consistently added.
3) What other things can I do to shed some light onto what is happening?
Any help would be appreciated.
Best,
Christian

[Jan-Oliver Kaiser]

Hey Christian,

You can print entire modules using [Print] or [Print Module] in case of
ambiguities. With [Set Printing Universes] enabled you can at least
search for particular universes quickly within a module. (There's one
annoying thing here which is that submodules are not automatically
expanded. Maybe there is an option for that that I don't know?)

Apart from that, [Set Printing Universes] should *sometimes* show the
full universe cycle when an inconsistency occurs, but it depends very
much on the particular error that appears.

Regarding the actual inconsistency: One quick way of eliminating a
particular egregious class of inconsistencies is to look for partial
applications of template-polymorphic types (such as datatypes from the
standard library). These partial applications restrict all future uses
of the partially-applied type and can very easily lead to hard-to-find
inconsistencies. An example would be a type classes such as [FMap] with
an instance [FMap list]. Together with another definition that mixes
[FMap] and [list] and introduces the opposite universe constraint of the
[FMap] instance for [list], this can lead to inconsistencies.

If you do find any such partial applications, try to see if the universe
cycle includes any of the relevant universes. Or, equivalently, start
with the universes in the cycle—attainable by massaging the failing
definition with explicit universes until you get the right *kind* of
universe error—and see if any of them are related to the standard
library or your own template-polymorphic inductive types and work
backwards from there to find partial applications of such types.

Sadly even this process can take a long time.

Best,
Janno

Hello,
I already had used "Set Printing Universes". As far as I can tell, the
only thing "Set Printing Universes" does is cause "Print/Check term." to
print the universe levels of all occurrences of "Type" occurring in a
particular definition as well as the constraints enforced by a
particular definition.
I have a constraint system with thousands of constraints arising from
hundreds of definitions and I would like to know which constraints
contribute to the inconsistency and which definitions/lemmas give rise
to a given constraint.
For instance, Print Universes might mention
"Coq.Relations.Relation_Definitions.1" which I could correctly guess is
relation =
But its not always that easy to guess the definitions introducing a
particular universe index and even harder to guess which definition or
lemma enforces a given constraint.
Best,
Christian

Post by Gaëtan Gilbert
1) yes
2) and 3)
if you enable printing of universes (Set Printing Universes. in
coqtop/proof general/etc, some GUI toggle in coqide) universe
inconsistencies should print that information
Gaëtan Gilbert

Post by Christian Doczkal
Hello everyone,
We have a large development where we have generic structures and some
concrete instances for them. One of these is for relations (X -> Y ->
Prop) with (X,Y : Set).
Now I was trying to generalize this to all instances with (X,Y : Type).
This leads to a universe inconsistency thousands of lines down the road.
I would hope that this is merely a problem of making certain things
universe polymorphic, but I don't manage to come up with a minimal
example reproducing the problem.
At first, I only got the rather uninformative "Universe Inconsistency"
error when trying to load two separately compiled parts of the library.
With some trial and error I got to the point where I have statement that
type checks before the generalized instances are imported and fails to
I can use "Print Universes" before and after the Import, but that yields
thousands of constraints and even the diff is not too enlightening.
If I understand the universe mechanism and the error message correctly,
this actually means that assuming "foo.2 <= bar.3" is inconsistent with
1) Is my understanding correct?
2) If yes, is there a way to obtain a minimal (or at least sufficiently
small) subset of the current collection of constraints, proving that
"foo.2 <= bar.3" cannot be consistently added.
3) What other things can I do to shed some light onto what is happening?
Any help would be appreciated.
Best,
Christian

[Christian Doczkal]

Hello,

You can print entire modules using [Print] or [Print Module] in case of ambiguities.

Thank you, I simply hadn't thought of that. Pretty useful.

Apart from that, [Set Printing Universes] should *sometimes* show the
full universe cycle when an inconsistency occurs, but it depends very
much on the particular error that appears.

This I find very interesting. Could someone with insight into the
algorithm comment on which kind of type checking problems are more
likely to trigger an error message providing a full cycle?

Other than that, has anyone played with dumping the output of print
universes plus the constraint that is reported as inconsistent into some
external tool that finds irreducible infeasible subsets for the
underlying ILP? (Does there even exist open source software finding these?)

Best,
Christian

[Christian Doczkal]

Hello,

I got back to investigating universe inconsistencies, and I realize that
I still don't quite understand the mechanics. So here are two more
questions:

1) I have two modules, say A and B such that:
- Require Import A B. succeeds
- Require Import B A. fails

So what is happening to the universe constraints upon Require Import
that makes this order sensitive? In would have expected that either
order yields the union of the constraints imposed by A and B. In this
particular case, A contains universe polymorphic instances of classes
that are common ancestors of A and B.

2) While experimenting with making more and more things universe
polymorphic, I encountered an error message I don't understand:

globalization of polymorphic reference <ID> would forget universes.

This seems to be undocumented, so what is the problem here? (e.g., is
there a minimal example triggering this message?)

Best,
Christian

Hello,

You can print entire modules using [Print] or [Print Module] in case of ambiguities.

Thank you, I simply hadn't thought of that. Pretty useful.

Apart from that, [Set Printing Universes] should *sometimes* show the
full universe cycle when an inconsistency occurs, but it depends very
much on the particular error that appears.

This I find very interesting. Could someone with insight into the
algorithm comment on which kind of type checking problems are more
likely to trigger an error message providing a full cycle?
Other than that, has anyone played with dumping the output of print
universes plus the constraint that is reported as inconsistent into some
external tool that finds irreducible infeasible subsets for the
underlying ILP? (Does there even exist open source software finding these?)
Best,
Christian

[Gaëtan Gilbert]

Post by Christian Doczkal
- 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.

Post by Christian Doczkal
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.

Gaëtan Gilbert

Post by Christian Doczkal
Hello,
I got back to investigating universe inconsistencies, and I realize that
I still don't quite understand the mechanics. So here are two more
- Require Import A B. succeeds
- Require Import B A. fails
So what is happening to the universe constraints upon Require Import
that makes this order sensitive? In would have expected that either
order yields the union of the constraints imposed by A and B. In this
particular case, A contains universe polymorphic instances of classes
that are common ancestors of A and B.
2) While experimenting with making more and more things universe
globalization of polymorphic reference <ID> would forget universes.
This seems to be undocumented, so what is the problem here? (e.g., is
there a minimal example triggering this message?)
Best,
Christian

Hello,

You can print entire modules using [Print] or [Print Module] in case of ambiguities.

Thank you, I simply hadn't thought of that. Pretty useful.

Apart from that, [Set Printing Universes] should *sometimes* show the
full universe cycle when an inconsistency occurs, but it depends very
much on the particular error that appears.

This I find very interesting. Could someone with insight into the
algorithm comment on which kind of type checking problems are more
likely to trigger an error message providing a full cycle?
Other than that, has anyone played with dumping the output of print
universes plus the constraint that is reported as inconsistent into some
external tool that finds irreducible infeasible subsets for the
underlying ILP? (Does there even exist open source software finding these?)
Best,
Christian

[Christian Doczkal]

Hi,

Post by Gaëtan Gilbert

Post by Christian Doczkal
- 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.

Post by Gaëtan Gilbert

Post by Christian Doczkal
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

[Matthieu Sozeau]

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 <

Post by Christian Doczkal
Hi,

Post by Gaëtan Gilbert

Post by Christian Doczkal
- 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.

Post by Gaëtan Gilbert

Post by Christian Doczkal
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

[Christian Doczkal]

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.

Post by Matthieu Sozeau
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
Hi,

Post by Gaëtan Gilbert

Post by Christian Doczkal
- 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.

Post by Gaëtan Gilbert

Post by Christian Doczkal
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

[Matthieu Sozeau]

Hi Christian,

this is a bit surprising but I don't think it is a bug. I guess what
happens is that your use
of @eq partially applied in foo, results in a cumulativity test of the form
Type@{Coq.Init.Logic.8} -> ? <= Type@{U} -> ?

Which by default forces U = Coq.Init.Logic.8. If you enforce your
constraint, it might force
that assignment U = Coq.Init.Logic.8 to fail, and in that case the Coq
typechecker will backtrack
and eta-expand @eq to (fun A : U => @eq A) and only enforce U <=
Coq.Init.Logic.8. You can
confirm this by looking at the definition of foo in the first case, it
should have this eta expansion.
The conclusion is that you should avoid partial applications of "template"
polymorphic constants
like eq, that's one of the quirks of the feature.

Best regards,
-- Matthieu

On Tue, Sep 11, 2018 at 4:04 PM Christian Doczkal <

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
Fail Constraint L < S.
Fail Constraint L < U.
Constraint S = L.
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.
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.

Post by Matthieu Sozeau
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
Hi,

Post by Gaëtan Gilbert

Post by Christian Doczkal
- 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,

Post by Matthieu Sozeau
and the problem occurs at the end. Should I manage to find a small
example, I will open an issue.

Post by Gaëtan Gilbert

Post by Christian Doczkal
globalization of polymorphic reference <ID> would forget

universes.

Post by Matthieu Sozeau

Post by Gaëtan Gilbert
Unfortunately various tactics and commands do not support or badly
support universe polymorphism. This error means some function

hasn't

Post by Matthieu Sozeau

Post by Gaëtan Gilbert
been adapted. It should probably be an anomaly.
Depending on what exactly is failing it may be possible for us to

fix

Post by Matthieu Sozeau

Post by Gaëtan Gilbert
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

Post by Matthieu Sozeau
polymorphism? (The error occurred while trying to see what happens

if I

Post by Matthieu Sozeau
make just about everything universe polymorphic, so it may or may

not be

Post by Matthieu Sozeau
necessary to fix this)
Thanks for the pointers,
Christian

[Christian Doczkal]

Hi Matthieu,

Thank you very much for your explanation, this seems to be pretty much
exactly what is happening. I don't yet know whether that will allow me
to achieve what I was trying to do last month, but at least I now have
small example exhibiting exactly the behavior you describe.

Naturally, this leads to the question whether there are other
circumstances where the universe constraints inferred for a particular
definition are stronger than what could be inferred or can be inferred
for a convertible definition (or a slight variation).

Also, do you think it would make sense to name the universes of the most
important template polymorphic inductive types (e.g., eq, list, etc.).
That is, replace the definition of eq with:

Universe eq.
Inductive eq (A : Type@{eq}) (x : A) : A -> Prop := eq_refl : eq A x x.

If I understand the mechanisms correctly, this by itself should not
introduce any compatibility issues and might help understand the output
of "Print Universes".

Similarly, reusing this universe for basic lemmas might be a way to
avoid introducing unnecessary universes without introducing too many
compatibility issues, but I'm less sure about that.

Best,
Christian

Post by Matthieu Sozeau
Hi Christian,
  this is a bit surprising but I don't think it is a bug. I guess what
happens is that your use 
Which by default forces U = Coq.Init.Logic.8. If you enforce your
constraint, it might force
that assignment U = Coq.Init.Logic.8 to fail, and in that case the Coq
typechecker will backtrack
Coq.Init.Logic.8. You can 
confirm this by looking at the definition of foo in the first case, it
should have this eta expansion.
The conclusion is that you should avoid partial applications of
"template" polymorphic constants
like eq, that's one of the quirks of the feature.
Best regards,
-- Matthieu
On Tue, Sep 11, 2018 at 4:04 PM Christian Doczkal
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
Fail Constraint L < S.
Fail Constraint L < U.
Constraint S = L.
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.
  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.

Post by Matthieu Sozeau
Dear Christian,
There is documentation in dev/doc/universes about the changes

necessary.

Post by Matthieu Sozeau
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

Post by Matthieu Sozeau
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.

Post by Matthieu Sozeau
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

Post by Matthieu Sozeau
constraints so the bug couldn’t happen in that case.
Best,
— Matthieu
Le lun. 10 sept. 2018 à 14:28, Christian Doczkal
     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,

Post by Matthieu Sozeau
     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.

Post by Matthieu Sozeau
     >
     > Unfortunately various tactics and commands do not support or

badly

Post by Matthieu Sozeau
     > support universe polymorphism. This error means some

function hasn't

Post by Matthieu Sozeau
     > been adapted. It should probably be an anomaly.
     > Depending on what exactly is failing it may be possible for

us to fix

Post by Matthieu Sozeau
     > it, or it could be beyond our current manpower.
     This happens when calling one of our own tactics written in

OCaml. So

Post by Matthieu Sozeau
     how does one have to adapt tactics in order to properly

support universe

Post by Matthieu Sozeau
     polymorphism? (The error occurred while trying to see what

happens if I

Post by Matthieu Sozeau
     make just about everything universe polymorphic, so it may or

may not be

Post by Matthieu Sozeau
     necessary to fix this)
     Thanks for the pointers,
     Christian

[Gaëtan Gilbert]

Post by Christian Doczkal
Also, do you think it would make sense to name the universes of the most
important template polymorphic inductive types (e.g., eq, list, etc.).

In https://github.com/coq/coq/issues/2829#issuecomment-350265818 I talk
about a branch of mine which tries to do this automatically, such that
for instance the universe on eq is called eq.0
In it I mention some issues but the universe naming system has changed
some since so maybe it can be made to work reliably (also those issues
were not that bad in the first place).

I'll look into updating it and getting it into Coq.

Gaëtan Gilbert

Post by Christian Doczkal
Hi Matthieu,
Thank you very much for your explanation, this seems to be pretty much
exactly what is happening. I don't yet know whether that will allow me
to achieve what I was trying to do last month, but at least I now have
small example exhibiting exactly the behavior you describe.
Naturally, this leads to the question whether there are other
circumstances where the universe constraints inferred for a particular
definition are stronger than what could be inferred or can be inferred
for a convertible definition (or a slight variation).
Also, do you think it would make sense to name the universes of the most
important template polymorphic inductive types (e.g., eq, list, etc.).
Universe eq.
If I understand the mechanisms correctly, this by itself should not
introduce any compatibility issues and might help understand the output
of "Print Universes".
Similarly, reusing this universe for basic lemmas might be a way to
avoid introducing unnecessary universes without introducing too many
compatibility issues, but I'm less sure about that.
Best,
Christian

Post by Matthieu Sozeau
Hi Christian,
  this is a bit surprising but I don't think it is a bug. I guess what
happens is that your use
Which by default forces U = Coq.Init.Logic.8. If you enforce your
constraint, it might force
that assignment U = Coq.Init.Logic.8 to fail, and in that case the Coq
typechecker will backtrack
Coq.Init.Logic.8. You can
confirm this by looking at the definition of foo in the first case, it
should have this eta expansion.
The conclusion is that you should avoid partial applications of
"template" polymorphic constants
like eq, that's one of the quirks of the feature.
Best regards,
-- Matthieu
On Tue, Sep 11, 2018 at 4:04 PM Christian Doczkal
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
Fail Constraint L < S.
Fail Constraint L < U.
Constraint S = L.
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.
  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.

Post by Matthieu Sozeau
Dear Christian,
There is documentation in dev/doc/universes about the changes

necessary.

Post by Matthieu Sozeau
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

Post by Matthieu Sozeau
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.

Post by Matthieu Sozeau
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

Post by Matthieu Sozeau
constraints so the bug couldn’t happen in that case.
Best,
— Matthieu
Le lun. 10 sept. 2018 à 14:28, Christian Doczkal
     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,

Post by Matthieu Sozeau
     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.

Post by Matthieu Sozeau
     >
     > Unfortunately various tactics and commands do not support or

badly

Post by Matthieu Sozeau
     > support universe polymorphism. This error means some

function hasn't

Post by Matthieu Sozeau
     > been adapted. It should probably be an anomaly.
     > Depending on what exactly is failing it may be possible for

us to fix

Post by Matthieu Sozeau
     > it, or it could be beyond our current manpower.
     This happens when calling one of our own tactics written in

OCaml. So

Post by Matthieu Sozeau
     how does one have to adapt tactics in order to properly

support universe

Post by Matthieu Sozeau
     polymorphism? (The error occurred while trying to see what

happens if I

Post by Matthieu Sozeau
     make just about everything universe polymorphic, so it may or

may not be

Post by Matthieu Sozeau
     necessary to fix this)
     Thanks for the pointers,
     Christian

[Christian Doczkal]

If someone is touching the naming of universes it would be nice if the automatically generated names were actually Coq-identifiers. This would allow using them with the "Constraint" command.

In the same vein, it would be nice if there were also commands like "Consistent Constraint U <= V" that checks whether "U <= V" is consistent but does not add it and "Implied Constraint U < V" that checks whether "U < V" is implied by the current universe constraint.

Best,
Christian

Post by Christian Doczkal
Also, do you think it would make sense to name the universes of the most
important template polymorphic inductive types (e.g., eq, list, etc.).

In https://github.com/coq/coq/issues/2829#issuecomment-350265818 I talk about a branch of mine which tries to do this automatically, such that for instance the universe on eq is called eq.0
In it I mention some issues but the universe naming system has changed some since so maybe it can be made to work reliably (also those issues were not that bad in the first place).
I'll look into updating it and getting it into Coq.
Gaëtan Gilbert

Post by Christian Doczkal
Hi Matthieu,
Thank you very much for your explanation, this seems to be pretty much
exactly what is happening. I don't yet know whether that will allow me
to achieve what I was trying to do last month, but at least I now have
small example exhibiting exactly the behavior you describe.
Naturally, this leads to the question whether there are other
circumstances where the universe constraints inferred for a particular
definition are stronger than what could be inferred or can be inferred
for a convertible definition (or a slight variation).
Also, do you think it would make sense to name the universes of the most
important template polymorphic inductive types (e.g., eq, list, etc.).
Universe eq.
If I understand the mechanisms correctly, this by itself should not
introduce any compatibility issues and might help understand the output
of "Print Universes".
Similarly, reusing this universe for basic lemmas might be a way to
avoid introducing unnecessary universes without introducing too many
compatibility issues, but I'm less sure about that.
Best,
Christian

Post by Matthieu Sozeau
Hi Christian,
   this is a bit surprising but I don't think it is a bug. I guess what
happens is that your use
Which by default forces U = Coq.Init.Logic.8. If you enforce your
constraint, it might force
that assignment U = Coq.Init.Logic.8 to fail, and in that case the Coq
typechecker will backtrack
Coq.Init.Logic.8. You can
confirm this by looking at the definition of foo in the first case, it
should have this eta expansion.
The conclusion is that you should avoid partial applications of
"template" polymorphic constants
like eq, that's one of the quirks of the feature.
Best regards,
-- Matthieu
On Tue, Sep 11, 2018 at 4:04 PM Christian Doczkal
     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
     Fail Constraint L < S.
     Fail Constraint L < U.
     Constraint S = L.
     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.
       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.
     > 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
     >
     >     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
     >

[Gaëtan Gilbert]

It may not be as pretty but you can do "Fail Fail Constraint U <= V."
for the first and "Fail Constraint V <= U." for the second.

Gaëtan Gilbert

Post by Christian Doczkal
If someone is touching the naming of universes it would be nice if the automatically generated names were actually Coq-identifiers. This would allow using them with the "Constraint" command.
In the same vein, it would be nice if there were also commands like "Consistent Constraint U <= V" that checks whether "U <= V" is consistent but does not add it and "Implied Constraint U < V" that checks whether "U < V" is implied by the current universe constraint.
Best,
Christian

Post by Christian Doczkal
Also, do you think it would make sense to name the universes of the most
important template polymorphic inductive types (e.g., eq, list, etc.).

In https://github.com/coq/coq/issues/2829#issuecomment-350265818 I talk about a branch of mine which tries to do this automatically, such that for instance the universe on eq is called eq.0
In it I mention some issues but the universe naming system has changed some since so maybe it can be made to work reliably (also those issues were not that bad in the first place).
I'll look into updating it and getting it into Coq.
Gaëtan Gilbert

Post by Christian Doczkal
Hi Matthieu,
Thank you very much for your explanation, this seems to be pretty much
exactly what is happening. I don't yet know whether that will allow me
to achieve what I was trying to do last month, but at least I now have
small example exhibiting exactly the behavior you describe.
Naturally, this leads to the question whether there are other
circumstances where the universe constraints inferred for a particular
definition are stronger than what could be inferred or can be inferred
for a convertible definition (or a slight variation).
Also, do you think it would make sense to name the universes of the most
important template polymorphic inductive types (e.g., eq, list, etc.).
Universe eq.
If I understand the mechanisms correctly, this by itself should not
introduce any compatibility issues and might help understand the output
of "Print Universes".
Similarly, reusing this universe for basic lemmas might be a way to
avoid introducing unnecessary universes without introducing too many
compatibility issues, but I'm less sure about that.
Best,
Christian

Post by Matthieu Sozeau
Hi Christian,
   this is a bit surprising but I don't think it is a bug. I guess what
happens is that your use
Which by default forces U = Coq.Init.Logic.8. If you enforce your
constraint, it might force
that assignment U = Coq.Init.Logic.8 to fail, and in that case the Coq
typechecker will backtrack
Coq.Init.Logic.8. You can
confirm this by looking at the definition of foo in the first case, it
should have this eta expansion.
The conclusion is that you should avoid partial applications of
"template" polymorphic constants
like eq, that's one of the quirks of the feature.
Best regards,
-- Matthieu
On Tue, Sep 11, 2018 at 4:04 PM Christian Doczkal
     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
     Fail Constraint L < S.
     Fail Constraint L < U.
     Constraint S = L.
     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.
       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.
     > 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
     >
     >     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
     >

[Gaëtan Gilbert]

This is an error from calling constr_of_global (from module Universes,
in Coq master from module UnivGen) on some universe polymorphic global.

Tacmach.pf_global is a wrapper of it. You're unlikely to be using any
other caller in an ocaml tactic.

This is a function to turn a constant or inductive into a term, but when
the argument is universe polymorphic the universes need to be provided.

The standard solution is to use
[Evarutil.new_global : evar_map -> GlobRef.t -> evar_map * constr]
it will create new flexible (as
https://coq.inria.fr/distrib/current/refman/addendum/universe-polymorphism.html#conversion-and-unification)
universes to feed to your global.
You then have to pass around the updated evar map to work with it and to
update the tactic layer (tclEVARS or the like), if you drop it you will
get undeclared universe errors.

Gaëtan Gilbert

Post by Christian Doczkal
Hi,

Post by Gaëtan Gilbert

Post by Christian Doczkal
- 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.

Post by Gaëtan Gilbert

Post by Christian Doczkal
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