What to think about the following (inconsistent constraints between monomorphic universes in the local graph of a polymorphic constant):

```
Universe u v.
Definition a := Type : Type@{v}.
Definition f := fun A : Type@{u} => True.
Set Universe Polymorphism.
Definition g@{} := f a.
Unset Universe Polymorphism.
Definition c := Type@{u} : Type@{v}.
Print Assumptions g. (* Closed under the global context *)
Fail Definition h := g. (* Universe inconsistency: Cannot enforce v <= u because u < v *)
```

Shouldn't we at least report that the constraints needed to instantiate `h`

are unsatisfiable? Or register the constraints between global universes in polymorphic constants as global? (The latter being a priori more difficult since it requires to take a transitive closure, but we already have the function `Constraints.diff `

for that.)

I think we already had this discussion in some github issue, and the conclusion was that it's not a bug but a feature. In practice I'm not sure it matters really anyways.

https://github.com/coq/coq/issues/9359

Indeed, I remember the discussion. I'm somehow re-asking from a different perspective: should we consider it to be a bug or an incompleteness in the implementation if a polymorphic constant has also a monomorphic graph attached to it (see anomaly "Local universes in non-opaque polymorphic definition" in `Declare.cast_proof_entry`

, as well as a similar `assert (Univ.ContextSet.is_empty uctx)`

in `cast_opaque_proof_entry`

). Somehow, if we had a way in the syntax to specify that we want some of the constraints between monomorphic universes to be registered as global, there would be no theoretical obstacle to it?? The reason #9359 concluded not to do it was, it seems, mostly practical, in the sense that we did not know what choice of monomorphic subgraph of constraints to register in the general case.

For instance, user side, we can equally do:

```
Definition a@{u} := Type@{u}. (* u is global *)
```

and

```
Universe u.
Definition a := Type@{u}. (* u is global *)
```

We can also do:

```
Universe u.
#[universes(polymorphic)] Definition a := Type@{u}. (* u is global *)
```

but we have no similar syntactic way to say directly from the universe declaration of a polymorphic definition that we want some variables of the definition to be global.

Or, to put it in another way: it might be convenient, both user side and implementation side, to consider universe polymorphism not as a yes/no feature of a definition but as the ability for any definition to select a particular subgraph over which we want to generalize.

In this case, there would also be a clear strategy to decide which constraints are local and which are global. E.g., if I have the graph `u v w | u < v, v < w`

and I want to generalize over `u`

, then the polymorphic part is `u | u < v`

and the global part is `v w | v <w`

. Relatively to #9359, that is:

```
Universes i j.
Polymorphic Definition foo := Type@{i} : Type@{j}.
```

the strategy would tell to generalize `i < j`

over the empty set and would give the empty set for the polymorphic part and `i < j`

for the monomorphic part, as intuitively expected.

That is, the question raised in #9359 would move from: "how to report at the global level the constraints over global universes that *derive* from a set of constraints where some universes are abstracted", which is difficult, to "how to *abstract* a set of constraints over a selection of universes which we want to consider variables", which is easy.

Trying to find my way in `UState.ml`

, it seems that such split between the constraints involving at least one variable and the constraints involving only global universes can be done in `UState.context`

(and I guess this would be ok also in the presence of algebraic constraints?).

is it really worth spending time on this?

I would say so, because it would make the implementation smoother.

sounds like it would make the implementation more complex to me

Not at all! On the contrary, it would allow to see monomorphic declarations as the subset of polymorphic definitions which abstract over zero variables. So, all the code making a distinction between polymorphic and monomorphic would disappear.

didn't we decide that's bad? https://github.com/coq/coq/pull/9380

OK, let's not draw too quickly too drastic conclusions. I don't know up to where seeing monomorphic declarations as a particular case of polymorphic declarations can be pushed (I need to understand https://github.com/coq/coq/pull/9380, its motivation and its closing) so, let's go by steps.

For instance, the distinction between `Entries.universes_entry`

and `UState.universes_entry`

could be dropped: any declaration would have a global graph and an optional local graph. `Entries.universes_entry`

would be reduced to an option type of this local graph and `UState.universes_entry`

to the pair of a global graph and an `Entries.universes_entry`

.

Altogether with the `poly`

flag, this is again equivalent to two graphs, the second one being feeded only when `poly`

is on. So, at least in `declare.ml`

, this would induce quite a lot of simplifications.

Last updated: Oct 13 2024 at 01:02 UTC