I have files `A.v`

and `B.v`

. In a third file, `C.v`

, I have `Require Import A B.`

which yields a universe problem. To fix it, I added `Require A.`

as the first line of `B.v`

, and all problems are gone. Any idea how that is even possible? (if somebody wants to glance over the real files, the added line is here)

A imposes some constraint

inference for B tries to impose a contradictory constraint but if forced to avoid it still succeeds

eg

```
Universes i j.
Module B.
Axiom f : Type@{i} -> nat.
Definition g := f : Type@{j} -> nat.
Print g.
End B.
Module A.
Constraint j < i.
End A.
```

if A is last as I wrote, `Print g`

says `= f`

and the Constraint fails

if you move A before B, Print g says `= fun x : Type => f x`

ie it had to eta expand (because conversion is not contravariant in the domain of forall)

the difference in generated terms is specific to the example, it's also possible that it unified the wrong universes instead of avoiding the eta expansion

Last updated: Jun 15 2024 at 08:01 UTC