Simp and rw regressions in 4.29.0-rc2?

Stream: lean4

[IntGrah]

Might be a skill issue, but the theorem marked with guard_msgs raises an error in 4.29.0-rc2, with simp seemingly not able to close the cheap rfl goal, whilst it does not in 4.28.0-rc1.

/- Works in 4.28.0-rc1 and 4.29.0-rc2 -/
example {X} : @Sum.map PUnit PUnit X X id id = id := by
  simp only [Sum.map_id_id]

def Opt (X : Type) := PUnit ⊕ X

def Opt.map {X Y : Type} (f : X → Y) : Opt X → Opt Y := Sum.map id f

/- Works in 4.28.0-rc1, but does not in 4.29.0-rc2 -/
/-- error:
unsolved goals
X : Type
⊢ id = id
-/
#guard_msgs in
example {X} : Opt.map (id : X → X) = id := by
  simp only [Opt.map, Sum.map_id_id]

def Opt.map' {X Y : Type} (f : X → Y) : PUnit ⊕ X → PUnit ⊕ Y := Sum.map id f

/- Works in 4.28.0-rc1 and 4.29.0-rc2 -/
example {X} : Opt.map' (id : X → X) = id := by
  simp only [Opt.map', Sum.map_id_id]

[IntGrah]

yet to find a good rw example

[IntGrah]

I was bumping some code from .28 to .29 and many rw, simp, and calc proofs stopped working with weird error messages like
"failed to synthesise Trans Eq Eq", or "could not find instance of foo + bar" (when the goal clearly has foo + bar), and simp failing to close many goals.

[IntGrah]

My code generally uses explicit "simp only" sets, so I don't suspect this is because of the simp set changing

[IntGrah]

Working on getting rw and calc examples

[Robin Arnez]

Well, it fails because it isn't trivial, with_reducible rfl will tell you

Tactic `rfl` failed: The left-hand side
  @id (PUnit ⊕ X)
is not definitionally equal to the right-hand side
  @id (Opt X)

Internally, simp uses something like a with_reducible rfl (which means to only unfold abbrevs). Before v4.29.0-rc2, it still unified PUnit ⊕ X and Opt X under normal transparency (being able to unfold basically anything). However, since v4.29.0-rc2, they are only unified under with_reducible_and_instances (being able to only unfold abbrevs and instances and notably not Opt). If you want the old behavior, you can use set_option backward.isDefEq.respectTransparency false.
See also #general > backward.isDefEq.respectTransparency for more effects of this change. Also note that the FRO doesn't recommend updating to v4.29.0 yet:

Kim Morrison schrieb:

However: unlike most months we do not yet advise downstream projects to move to v4.29.0-rc1, which is more of a :construction_zone: release candidate :construction_zone: than usual, and we will certainly be making further release candidates in this series before reaching a stable version.

[IntGrah]

Ah, I see, that makes much more sense now.