Stream: Coq users

Topic: Why does my fix for a universe problem work?

Yannick Forster (Dec 14 2021 at 18:23):

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)

Gaëtan Gilbert (Dec 14 2021 at 18:29):

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: Oct 01 2023 at 19:01 UTC