Mismatched lattice instances?

Stream: mathlib4

[Wojciech Nawrocki]

I encountered the following error with newest mathlib on a proof that used to work. I am not sure how to interpret it: should I just fix it by writing out the specific instance like below, or is this an issue with the instance hierarchy?

import Mathlib.Order.BooleanAlgebra

example (a b c : Bool) : ((a || b) && (a || c)) ≤ (a || (b && c)) :=
  show (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ (b ⊓ c) from
  /- type mismatch
    le_sup_inf
  has type
    @Sup.sup Bool (@SemilatticeSup.toSup Bool (@Lattice.toSemilatticeSup Bool DistribLattice.toLattice)) a b ⊓
        (a ⊔ ?m.42838) ≤
      a ⊔ b ⊓ ?m.42838 : Prop
  but is expected to have type
    @Sup.sup Bool (@SemilatticeSup.toSup Bool (@Lattice.toSemilatticeSup Bool GeneralizedCoheytingAlgebra.toLattice)) a
          b ⊓
        (a ⊔ c) ≤
      a ⊔ b ⊓ c : Prop -/
  le_sup_inf

example (a b c : Bool) : ((a || b) && (a || c)) ≤ (a || (b && c)) :=
  show (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ (b ⊓ c) from
  @le_sup_inf _ (GeneralizedCoheytingAlgebra.toDistribLattice) a b c

[Eric Wieser]

I think this is fallout from std4#183

[Eric Wieser]

The #mwe is

example :
  (GeneralizedCoheytingAlgebra.toLattice : Lattice Bool).sup =
    DistribLattice.toLattice.sup :=
  rfl -- fails

[Kyle Miller]

Just to confirm,

import Mathlib.Order.BooleanAlgebra
import Mathlib.Tactic.DefeqTransformations

example (a b c : Bool) : ((a || b) && (a || c)) ≤ (a || (b && c)) :=
  show (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ (b ⊓ c) from
  by
    convert le_sup_inf
    -- ⊢ GeneralizedCoheytingAlgebra.toLattice = DistribLattice.toLattice
    unfold_projs
    congr!
    -- ⊢ or = max
    -- ⊢ and = min

[Eric Wieser]

Or:

example : instDistribLatticeBool.sup = (· || ·) := rfl  -- fails
example : instBooleanAlgebraBool.sup = (· || ·) := rfl -- ok

(src#instDistribLatticeBool, src#instBooleanAlgebraBool)

[Eric Wieser]

There is a fix in the works in std, though ideally mathlib wouldn't be constructing these two things in different ways; I would have expected the rfl in my first message to succeed, but the other two to fail...

[Eric Wieser]

#8099