Universe bug in product CMRA?

Stream: iris-lean

[Markus de Medeiros]

I'm trying to track down a universe bug that seems to arise when I use operations from the product CMRA. I've collected examples here.

Examples

def test (α : Type _) [OFE α] (a : Option (Agree A)) := @CMRA.core _ _ a -- No bug
-- def test' (α : Type _) [OFE α] (a : Option (Agree A)) := @CMRA.core _ _ (a, a) -- Bug
def test'' (α : Type _) [CMRA α] (a : α) := @CMRA.core α _ a -- No bug
def test''' (α : Type _) [CMRA α] (a : α) := @CMRA.core (α × α) _ (a, a) -- No bug
def test'''' (α : Type _) [CMRA α] (a : α) := @CMRA.core (Option α) _ (some a) -- No bug
-- def test''''' (α : Type _) [CMRA α] (a : α) := @CMRA.core ((Option α) × (Option α)) _ (some α, some α) -- Bug
def test6 (α : Type _) [OFE α] (a : Agree A) := @CMRA.core _ _ a -- No bug
-- def test7 (α : Type _) [OFE α] (a : Agree A) := @CMRA.core _ _ (a, a) -- Bug
def test8 (α : Type _) [OFE α] (a : Agree A) := @CMRA.pcore _ _ a -- No Bug
-- def test9 (α : Type _) [OFE α] (a : Agree A) := @CMRA.pcore _ _ (a, a) -- Bug
def test10 (α : Type _) [OFE α] (a : Agree A) := @CMRA.op _ _ a a -- No Bug
-- def test11 (α : Type _) [OFE α] (a : Agree A) := @CMRA.op _ _ (a, a) (a, a) -- Bug
def test12 (α : Type _) [OFE α] (a : Agree A) := @CMRA.Valid _ _ a -- No Bug
-- def test13 (α : Type _) [OFE α] (a : Agree A) := @CMRA.Valid _ _ (a, a) -- Bug

The errors look like

stuck at solving universe constraint
  max ?u.15227 ?u.15228 =?= max ?u.15223 ?u.15224
while trying to unify
  Type (max ?u.15227 ?u.15228) : Type ((max ?u.15227 ?u.15228) + 1)
with
  Type (max ?u.15223 ?u.15224) : Type ((max ?u.15223 ?u.15224) + 1)

which maybe suggests that it's the two branches of the product having different universe levels, but I'm not sure how to trace where the universe variables come from.

@suhr Did you encounter anything like this when you were initially implementing the product CMRA?

[Mario Carneiro]

Are α and A supposed to be related to each other?

[Mario Carneiro]

the issue is this instance:

#check cmraProd
-- Iris.cmraProd.{u_1, u_2} {α β : Type (max u_1 u_2)} [CMRA α] [CMRA β] : CMRA (α × β)

[Mario Carneiro]

note that the two inputs are not in general universes, so this results in an unsolvable unification problem to make α and β have the same universe and to determine u_1 and u_2 from their common level

[Mario Carneiro]

and the reason for that is because of this use of monad bind:

  pcore x := do
    let a <- CMRA.pcore x.fst
    let b <- CMRA.pcore x.snd
    return (a,b)

This forces the two calls to CMRA.pcore to live in the same universe. You should use Option.bind directly instead, which is more universe polymorphic than the Bind instance:

  pcore x :=
    (CMRA.pcore x.fst).bind fun a =>
    (CMRA.pcore x.snd).bind fun b =>
    return (a,b)

[Markus de Medeiros]

Nice, thanks! I don't think I would have ever guessed that.