Hello,

I'm afraid I am not the first one to ask questions of this flavor, but I am trying to solve universe inconsistencies that I have met for some time in the ctrees library, and I'm a bit at a loss.

These inconsistencies seem to depend on the interaction between several other libraries, and in particular a (relatively) small first case can be exhibited with only the `itree`

library and the `relation-algebra`

one: https://github.com/DeepSpec/InteractionTrees/issues/254

However, after turning a couple of sensible definitions universe polymorphic, I end up in a situation where things break more or less depending on order of imports, inlining, and so on, without having much of an idea of what might be going on.

Would anyone have a little well of wisdom to make progress to diagnosis and hopefully solve this kind of problem?

Maybe you are already familiar with this, but one common problem that I am aware of is https://github.com/coq-community/coq-ext-lib/issues/124 . This issues arises quite easily, so maybe relation-algebra accidentally constraints some universes of common types that are then used by other definitions?

Ah thanks for the pointer! I need to read this in details, that seems indeed very relevant. Coincidentally I've been meaning to cut `ext-lib`

off from `itrees`

, that might be a good time to do so...

But that's not really an ext-lib bug. Can you entirely avoid higher-kinded abstractions like Kleisli/Monad? Or can you avoid their instances for template-polymorphic datatypes like option and list?

MackieLoeffel said:

Maybe you are already familiar with this, but one common problem that I am aware of is https://github.com/coq-community/coq-ext-lib/issues/124 . This issues arises quite easily, so maybe relation-algebra accidentally constraints some universes of common types that are then used by other definitions?

Reading through this makes me wonder: how much of these issues boil down to product types being equivariant rather than contravariant on their domains? The problems showing up specifically for higher-order abstractions and being possibly fixable by η-expansion makes me think this is relevant

Paolo Giarrusso said:

But that's not really an ext-lib bug. Can you entirely avoid higher-kinded abstractions like Kleisli/Monad? Or can you avoid their instances for template-polymorphic datatypes like option and list?

No I definitely cannot, and I don't expect cutting ext-lib to solve the issue, I just hope it'll narrow it better for me to understand what is happening. I for instance am quite confused to see the problematic constraints involve `ext-lib`

's `MonadFix`

, where as far as I can think we should not depend on at all.

The root is about template polymorphism being pretty broken: all uses of a partially applied template-polymorphic datatype share the same universe.

IIRC, eta-expanding gives a place to store different instances

it should definitely be worthwhile to try to fix this by η-expanding template poly on the fly, I've been thinking about that for a while

I'm not even sure it'd be *that* hard

A problem is hiding this from ltac matches

Patterns are a different kind of beast, though.

I mean that we're already doing a lot of fancy quotients in the upper layers (with relative success)

In practice we might be able to pull it off without breaking too much stuff

if this is one of the successful cases instead of primitive projections, yes it'd be great, if there isn't a more fundamental fix

(the alternative is to force partially applied template poly inductives to have an instance)

@Meven Lennon-Bertrand that _might_ be relevant if you're talking of universe variance, but I'm not sure if _subtyping_ constraints using a shared universe would be fine; you should check out https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 for more details

Paolo Giarrusso said:

Meven Lennon-Bertrand that _might_ be relevant if you're talking of universe variance, but I'm not sure if _subtyping_ constraints using a shared universe would be fine; you should check out https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 for more details

AFAIKT, if you have `list : Type@{list.u0} -> Type@{list.u1}`

and `F : (Type@{F.u0} -> Type@{F.u1}) -> Y`

and write `F (fun X : Type@{i} => list X)`

you get the following constraints: `F.u0 = i <= list.u0, list.u1 <= F.u1`

(the equality comes from equivariance on domains), while if you do not η-expand, you get instead `F.u0 = list.u0, list.u1 <= F.u1`

, and the first equality is what kills you. In a setting with contravariance on domains (as any good subtyping should have), you'd get `F.u0 <= list.u0, list.u1 <= F.u1`

, which is equivalent to the first set of constraints, without the extra generated `i`

.

So what η-expansion buys you with its extra instance is exactly contravariance on domains

This trick is used elsewhere in the code: if the elaborator chokes on a `X -> Y <= X' -> Y'`

constraint because it cannot get `X' = X`

, it tries again after having η-expanded the function `f`

of type `X -> Y`

to `fun x : X' => f x`

, which now has type `X' -> Y'`

whenever `X' <= X`

(rather than an equality)

that backtracking makes definition commute _less_ than we'd like, so you'd probably want the extra flexibility unconditionally (arguably, even in the existing use, but that's an existing a separate discussion because of the performance cost and questions about use-cases).

Re "contravariant subtyping", I thought that make things undecidable already in System F-omega_sub?

it's not completely crazy subtyping, we don't have unions or intersections

(that said it's not true in the Set model and I wouldn't be surprised if it contradicted mildly classical axioms)

Ok I'm not yet to the point of properly understanding the Template polymorphism and other clever parts mentioned above, but a couple of more naive questions:

- Is there any way for
`Print Universes Subgraph (u)`

to print all the constraints involving`u`

? At least the direct neighbours in the graph if not the smallest CC containing it? It's quite paintful to explore the full graph to find all the relevant variables before being able to prune it (and even worse, if I understand correctly I can't provide constant universes such as`Coq.Relations.Relation_Operators.7`

to the Subgraph?) - Does anyone have a minimal example/explanation as to why inlining sometimes solves an incoherence?

For the second point, it boils down to the typing rules of template poly. It's a limited (and ad-hoc) form of universe poly, so e.g. if you write

```
Inductive Box (A : Type) := box : A -> Box A.
```

the typing rule of Box is morally the one you'd get writing

```
#[universes(polymorphic)]
Inductive Box@{u} (A : Type@{u}) := box : A -> Box A.
```

In particular `Box A`

does not create a universe constraint. Unfortunately this polymorphism is local, i.e. it doesn't extend to any other construction of the language. So if you write

```
Definition myBox := Box.
```

this definition is totally monomorphic, so you get one fixed universe for the argument. By contrast, unfolding myBox would make the expression polymorphic.

Otherwise said, template poly inductive types and their constructors are "special".

Ah this is great, thanks a lot!

Wait no I'm actually confused: I read you as this monomorphisation by Definition as being a quirk of the template polymorphism, but the same happens with the more general universe polymorphic one doesn't it?

```
Inductive Box (A : Type) := box : A -> Box A.
#[universes(polymorphic)] Inductive Box'@{u} (A : Type@{u}) := box' : A -> Box' A.
#[universes(polymorphic)] Inductive Box''@{u v} (A : Type@{u}) : Type@{v} := box'' : A -> Box'' A.
(* Mono, one universe fixed *)
Definition myBox := Box.
(* Mono, one universe fixed *)
Definition myBox' := Box'.
(* Mono, two universes fixed *)
Definition myBox'' := Box''.
```

Am I missing your point?

you can do `Polymorphic Definition`

but not template polymorphic

@Yannick Zakowski the same applies if you mix univ poly / mono definitions indeed, but my point was about the fact that inlining can reduce the amount of universe breakage.

Last updated: Oct 04 2023 at 23:01 UTC