isDefEq on projections

Stream: lean4 dev

[Reid Barton]

Is it expected that when we test two projections x.1 =?= y.1 for defeq, we try to test x =?= y even if x and y might not have the same type at all?

[Reid Barton]

mwe:

structure Pair :=
(x : Bool)
(y : Bool)

structure Triple :=
(a : Bool)
(b : Bool)
(c : Bool)

def myPair : Pair := ⟨true, false⟩

def myTriple : Triple := ⟨true, true, true⟩

set_option trace.Meta.isDefEq true

theorem test : myPair.1 = myTriple.1 :=
  rfl

[Reid Barton]

trace:

[Meta.isDefEq] ✅ Bool =?= Bool
[Meta.isDefEq] ✅ Bool =?= Bool
[Meta.isDefEq] ✅ Bool =?= Bool
[Meta.isDefEq] ✅ Bool =?= ?m.796
  [Meta.isDefEq] Bool [nonassignable] =?= ?m.796 [assignable]
  [Meta.isDefEq] ✅ Sort ?u.795 =?= Type
[Meta.isDefEq] ✅ Bool =?= Bool
[Meta.isDefEq] ✅ Pair =?= Pair
[Meta.isDefEq] ✅ Triple =?= Triple
[Meta.isDefEq] ✅ myPair.x = myTriple.a =?= ?m.800 = ?m.800
  [Meta.isDefEq] ✅ Bool =?= ?m.799
    [Meta.isDefEq] Bool [nonassignable] =?= ?m.799 [assignable]
    [Meta.isDefEq] ✅ Sort ?u.798 =?= Type
  [Meta.isDefEq] ✅ myPair.x =?= ?m.800
    [Meta.isDefEq] myPair.x [nonassignable] =?= ?m.800 [assignable]
    [Meta.isDefEq] ✅ Bool =?= Bool
  [Meta.isDefEq] ✅ myTriple.a =?= myPair.x
    [Meta.isDefEq] ✅ myTriple.a =?= myPair.x
      [Meta.isDefEq] ✅ myTriple.1 =?= myPair.1
        [Meta.isDefEq] ❌ myTriple =?= myPair    <--- ???
          [Meta.isDefEq] ❌ { a := true, b := true, c := true } =?= { x := true, y := false }
            [Meta.isDefEq] ❌ Triple.mk =?= Pair.mk
            [Meta.isDefEq.onFailure] ❌ { a := true, b := true, c := true } =?= { x := true, y := false }
            [Meta.isDefEq.onFailure] ❌ { a := true, b := true, c := true } =?= { x := true, y := false }
        [Meta.isDefEq] ✅ true =?= true
[Meta.isDefEq] ✅ myPair.x = myPair.x =?= myPair.x = myTriple.a
  [Meta.isDefEq] ✅ myPair.x =?= myPair.x
  [Meta.isDefEq] ✅ myPair.x =?= myTriple.a
    [Meta.isDefEq] ✅ myPair.1 =?= myTriple.1
      [Meta.isDefEq] ❌ myPair =?= myTriple    <--- ???
        [Meta.isDefEq] ❌ { x := true, y := false } =?= { a := true, b := true, c := true }
          [Meta.isDefEq] ❌ Pair.mk =?= Triple.mk
          [Meta.isDefEq.onFailure] ❌ { x := true, y := false } =?= { a := true, b := true, c := true }
          [Meta.isDefEq.onFailure] ❌ { x := true, y := false } =?= { a := true, b := true, c := true }
      [Meta.isDefEq] ✅ true =?= true
  [Meta.isDefEq] ✅ Bool =?= Bool

[Reid Barton]

Even if this is intentional, it seems like potentially you could do a lot of work reducing x and y without noticing that the types were not even the same in the first place

[Mauricio Collares]

https://github.com/leanprover/lean4/pull/2003#issuecomment-1380524624 seems related

[Reid Barton]

Right and 2003 changes this behavior somewhat from what I remember (it checks that x and y are at least instances of the same structure, though other parameters in the type could still differ)

[Reid Barton]

e.g. if the first field in the structure is of some constant type, like Int

[Gabriel Ebner]

That PR also contains a bug fix for the issue you're seeing: https://github.com/leanprover/lean4/pull/2003/commits/31242cb497aa1c2c4e8de579df40dcb3327c0638