Stream: Coq users

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


view this post on Zulip 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)

view this post on Zulip 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: Jan 29 2023 at 03:28 UTC