Regression in apply at nonstandard transparency

[hrmacbeth]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

There is an apparent regression in with_reducible_and_instances apply on current nightly (4.15.0-nightly-2024-11-30), compared to 4.14.0-rc3.

Context

This is isolated from a failure of the mathlib tactic gcongr which turned up in one of the "nightly testing" bumps, leanprover-community/mathlib4#19314.

Zulip discussion:

• https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/.2319314.20adaptations.20for.20nightly-2024-11-20
• https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Minimization.20request

Steps to Reproduce

class Inv (α : Type) where
  inv : α → α

postfix:max "⁻¹" => Inv.inv

class DivInvMonoid (G : Type) extends Inhabited G, Inv G where
  zpow : Int → G → G

class InvOneClass (G : Type) extends Inv G
class DivInvOneMonoid (G : Type) extends DivInvMonoid G, InvOneClass G
class DivisionMonoid (G : Type) extends DivInvMonoid G
class DivisionCommMonoid (G : Type) extends DivisionMonoid G
class GroupWithZero (G : Type) extends Inhabited G, DivInvMonoid G
class CommGroupWithZero (G : Type) extends Inhabited G, GroupWithZero G

theorem inv_anti₀ [GroupWithZero M] {a : M} (P : M → Prop) (hba : P a) : P (a⁻¹) := sorry

instance (priority := 100) DivisionMonoid.toDivInvOneMonoid {α : Type} [DivisionMonoid α] :
    DivInvOneMonoid α :=
  { DivisionMonoid.toDivInvMonoid with }

instance (priority := 100) CommGroupWithZero.toDivisionCommMonoid {G : Type} [CommGroupWithZero G] :
    DivisionCommMonoid G :=
  { ‹CommGroupWithZero G› with }

/-! ## Algebraic structure on the nonnegative elements of a type -/

namespace Nonneg
variable {α : Type} [CommGroupWithZero α] (P : α → Prop)

instance one : Inhabited (Subtype P) where default := ⟨default, sorry⟩
instance inv : Inv (Subtype P) where inv x := ⟨x⁻¹, sorry⟩

instance groupWithZero : GroupWithZero (Subtype P) :=
  { zpow := fun n x => ⟨DivInvMonoid.zpow n x, sorry⟩ }

instance commGroupWithZero : CommGroupWithZero (Subtype P) :=
  { Nonneg.groupWithZero P with }

end Nonneg


/-! ## Main issue -/

axiom Real : Type
notation "ℝ" => Real
@[instance] axiom Real.commGroupWithZero : CommGroupWithZero ℝ

axiom P : ℝ → Prop

def NNReal := Subtype P
notation "ℝ≥0" => NNReal
noncomputable instance : CommGroupWithZero ℝ≥0 := Nonneg.commGroupWithZero P


-- test 1
example {p : ℝ≥0} (P : ℝ≥0 → Prop) : P (p⁻¹) := by
  apply inv_anti₀ -- works
  sorry

-- test 2
example {p : ℝ≥0} (P : ℝ≥0 → Prop) : P (p⁻¹) := by
  with_reducible_and_instances apply inv_anti₀
  sorry

Expected behavior: Both Test 1 and Test 2 succeed.

Actual behavior: Test 2 fails with the error "tactic 'apply' failed, failed to assign synthesized instance".

Versions

4.15.0-nightly-2024-11-30

(Both tests work on 4.14.0-rc3.)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[hrmacbeth]

I bisected, this seems to appear for the first time in nightly-2024-11-12. Maybe it is caused by #5920? (cc @kmill)