diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index c5cc39145b4c..e7688d6979c2 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -82,6 +82,46 @@ register_builtin_option backward.isDefEq.implicitBump : Bool := {
   not just instance-implicit ones"
 }
 
+/--
+Controls how a failing comparison of two applications invokes `isDefEqOnFailure`.
+
+**Original behavior (`true`):** once before `isDefEqProjInst`, `isDefEqStringLit` and
+`isDefEqUnitLike`, and once again after them, querying the unification hint discrimination tree
+four times instead of two. A stuck abort raised by the first invocation escapes immediately, so
+the three heuristics in between never run.
+
+**New behavior (`false`, the default):** once, before those heuristics. A stuck abort is deferred
+until they have had their chance, and re-raised if they all decline.
+-/
+register_builtin_option backward.isDefEq.appOnFailure : Bool := {
+  defValue := false
+  descr    := "if true, run the stuck-metavariable and unification-hint pass both before and \
+  after the remaining `isExprDefEqExpensive` heuristics, instead of only before them"
+}
+
+/--
+Controls whether assignments to instance-typed metavariables (see
+`MetavarContext.instanceTypedMVars`) are restricted so that the final value of a
+metavariable created for an instance-implicit argument has the type the metavariable was
+created with, up to `TransparencyMode.instances`. This prevents unification from committing
+to an instance for a type that is different at instance-resolution time. See issue #9077.
+
+With `true`, the value must be one instance synthesis could have produced: either the candidate
+value already is such a value — its type matches at `.instances` transparency and the
+metavariables in its type-determining (spine) positions are themselves instance-typed or not
+assignable by `isDefEq` — or the instance is synthesized directly and the candidate must be
+definitionally equal to the result. If synthesis fails, the assignment, and with it the current
+unification attempt, fails.
+
+With `false`, there is no restriction (the behavior before the fix for issue #9077).
+-/
+register_builtin_option backward.isDefEq.instanceTypes : Bool := {
+  defValue := true
+  descr    := "if true, restrict assignments to instance metavariables to values instance \
+  synthesis could have produced, preserving the metavariable's type up to `.instances` \
+  transparency"
+}
+
 register_builtin_option trace.Meta.isDefEq.printTransparency : Bool := {
   defValue := false
   descr    := "if true, prefix `Meta.isDefEq` `=?=` trace messages with the current transparency level"
@@ -285,6 +325,23 @@ inductive DefEqArgsFirstPassResult where
   -/
   | ok (postponedImplicit : Array Nat) (postponedHO : Array Nat)
 
+/--
+Ensure `MetaM` configuration is strong enough for checking definitional equality of
+implicit and instance-implict arguments as well as assigned mvar types. Bumps transparency to at
+least `.implicit`, so both `[instance_reducible]` and `[implicit_reducible]` unfold.
+-/
+@[inline] def withImplicitConfig (x : MetaM α) : MetaM α := do
+  let old ← getTransparency
+  if old.lt .implicit then
+    trace[Meta.isDefEq.transparency]
+      "raising transparency {toString old} → implicit"
+  withAtLeastTransparency .implicit do
+    let cfg ← getConfig
+    if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaHave && cfg.zetaDelta && cfg.proj == .yesWithDelta then
+      x
+    else
+      withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaHave := true, zetaDelta := true, proj := .yesWithDelta }) x
+
 /--
   First pass for `isDefEqArgs`. We unify explicit arguments, *and* easy cases
   Here, we say a case is easy if it is of the form
@@ -318,6 +375,9 @@ inductive DefEqArgsFirstPassResult where
 -/
 private def isDefEqArgsFirstPass
     (paramInfo : Array ParamInfo) (args₁ args₂ : Array Expr) : MetaM DefEqArgsFirstPassResult := do
+  let opts ← getOptions
+  let respectTransparency := backward.isDefEq.respectTransparency.get opts
+  let implicitBump := backward.isDefEq.implicitBump.get opts
   let mut postponedImplicit := #[]
   let mut postponedHO := #[]
   for h : i in *...paramInfo.size do
@@ -338,8 +398,17 @@ private def isDefEqArgsFirstPass
       unless (← Meta.isExprDefEqAux a₁ a₂) do
         return .failed
     else if (← isEtaUnassignedMVar a₁ <||> isEtaUnassignedMVar a₂) then
-      unless (← Meta.isExprDefEqAux a₁ a₂) do
-        return .failed
+      /- Easy cases are still argument unifications at an implicit position, so they get the same
+         transparency bump as the second pass: whether an argument is checked at `.implicit`
+         should not depend on which side happens to be an unassigned metavariable. In particular,
+         the assignment triggered here — including the type check and `instanceTypes` fallbacks
+         run by `checkTypesAndAssign` — sees the bumped ambient transparency. -/
+      if respectTransparency && (info.binderInfo.isInstImplicit || implicitBump) then
+        unless (← withImplicitConfig <| Meta.isExprDefEqAux a₁ a₂) do
+          return .failed
+      else
+        unless (← Meta.isExprDefEqAux a₁ a₂) do
+          return .failed
     else
       if info.isProp then
         unless ← isAbstractedUnassignedMVar a₁ <||> isAbstractedUnassignedMVar a₂ do
@@ -352,16 +421,12 @@ private def isDefEqArgsFirstPass
   return .ok postponedImplicit postponedHO
 
 /--
-Ensure `MetaM` configuration is strong enough for checking definitional equality of
-implicit and instance-implict arguments as well as assigned mvar types. Bumps transparency to at
-least `.implicit`, so both `[instance_reducible]` and `[implicit_reducible]` unfold.
+Like `withImplicitConfig`, but sets transparency to exactly `.instances`: instance-typed
+metavariable assignments must preserve the type at `.instances` even when the ambient
+transparency is higher.
 -/
-@[inline] def withImplicitConfig (x : MetaM α) : MetaM α := do
-  let old ← getTransparency
-  if old.lt .implicit then
-    trace[Meta.isDefEq.transparency]
-      "raising transparency {toString old} → implicit"
-  withAtLeastTransparency .implicit do
+@[inline] def withInstancesConfig (x : MetaM α) : MetaM α := do
+  withTransparency .instances do
     let cfg ← getConfig
     if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaHave && cfg.zetaDelta && cfg.proj == .yesWithDelta then
       x
@@ -489,11 +554,107 @@ abbrev respectTransparencyAtTypes : CoreM Bool := do
   let opts ← getOptions
   return backward.isDefEq.respectTransparency.types.get opts && backward.isDefEq.respectTransparency.get opts
 
+/--
+Return `true` if all metavariables in type-determining (spine) positions of `e` are
+admissible in a value assigned to an instance-typed metavariable under
+`backward.isDefEq.instanceTypes` (see `MetavarContext.instanceTypedMVars`). Admissible are:
+- instance-typed metavariables: their own assignments are subject to the same restriction;
+- metavariables `isDefEq` cannot assign (from an outer `MetavarContext` depth, or synthetic
+  opaque): the current instance search cannot commit them to a wrong-typed value, and their
+  eventual assignment is governed by whoever created them (e.g. the elaborator's pending
+  instance metavariables, which are synthesized against their recorded type).
+
+Only spine positions matter: `inferType` consults the type of a subterm only there (the head
+of an application, the body of a lambda or `let`, the structure of a projection). A
+metavariable in argument position enters the inferred type only by substitution, so
+instantiating it changes the value's type and its occurrences in the already-checked
+expected type in the same way.
+
+A delayed-assigned spine metavariable need not be admissible itself — it will never be
+assigned directly — but the spine of its pending metavariable is checked instead.
+-/
+partial def spineMVarsAdmissible (e : Expr) : MetaM Bool := go e
+where
+  go (e : Expr) : MetaM Bool := do
+    unless e.hasExprMVar do return true
+    match e with
+    | .mvar mvarId =>
+      if let some d ← getDelayedMVarAssignment? mvarId then
+        go (mkMVar d.mvarIdPending)
+      else
+        mvarId.isInstanceTyped <||> mvarId.isReadOnlyOrSyntheticOpaque
+    | .app f _ => go f
+    | .lam _ _ b _ => go b
+    | .letE _ _ v b _ => go v <&&> go b
+    | .proj _ _ s => go s
+    | .mdata _ b => go b
+    | _ => return true
+
+/--
+Type check for assignments to instance-typed metavariables: the value's type must agree with
+the metavariable's type at `.instances` transparency.
+
+The check is *eta-tolerant*: when the types are function types whose binder domains agree
+only above `.instances` (e.g. across a semireducible synonym like Mathlib's `OrderDual`), we
+accept the value as long as the codomain — where instance selection actually happens —
+agrees at `.instances` for the metavariable type's own binders. Without this, acceptance
+would depend on which eta-representative of the value the unifier happened to build
+(`tryResolve` eta-reduces answers, so `fun i : Dual ι => inst i` becomes the bare `inst`,
+whose inferred type has the `ι` binder). The full types must still agree at the ordinary
+transparency, ensuring the assignment remains type-correct.
+-/
+private def checkInstanceTypedTypes (mvarType vType v : Expr) : MetaM Bool := do
+  if (← withInstancesConfig <| Meta.isExprDefEqAux mvarType vType) then
+    return true
+  unless mvarType.isForall do return false
+  let oldOk ← if (← respectTransparencyAtTypes) then
+    withImplicitConfig <| Meta.isExprDefEqAux mvarType vType
+  else
+    withInferTypeConfig <| Meta.isExprDefEqAux mvarType vType
+  unless oldOk do return false
+  forallTelescope mvarType fun xs body => do
+    withInstancesConfig <| Meta.isExprDefEqAux body (← inferType (mkAppN v xs))
+
+/--
+Fallback for assignments to instance-typed metavariables under
+`backward.isDefEq.instanceTypes` when the candidate value `v` is not directly acceptable:
+synthesize the instance for the metavariable's type, assign it, and require `v` to be
+definitionally equal to the synthesized instance. This mirrors the elaboration order in
+which instance arguments were synthesized first and only then unified. Fails without
+modifying the state if synthesis fails or if `v` does not match the synthesized instance.
+-/
+private def synthInstanceTypedMVarAndUnify (mvar v : Expr) : MetaM Bool := do
+  checkpointDefEq do
+    unless (← Meta.synthPending mvar.mvarId!) do
+      if (← isDiagnosticsEnabled) then
+        trace[diagnostics] "failure when assigning instance metavariable with type{indentExpr (← inferType mvar)}\nthe candidate value{indentExpr v}\nwas rejected and the instance could not be synthesized directly.\nWorkaround: `set_option backward.isDefEq.instanceTypes false`"
+      return false
+    let inst ← instantiateMVars mvar
+    if (← Meta.isExprDefEqAux v inst) then
+      return true
+    else
+      if (← isDiagnosticsEnabled) then
+        trace[diagnostics] "failure when assigning instance metavariable with type{indentExpr (← inferType mvar)}\nthe rejected candidate value{indentExpr v}\nis not definitionally equal to the synthesized instance{indentExpr inst}\nWorkaround: `set_option backward.isDefEq.instanceTypes false`"
+      return false
+
 private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
   withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (fun _ => return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do
     if !mvar.isMVar then
       trace[Meta.isDefEq.assign.checkTypes] "metavariable expected"
       return false
+    if (← mvar.mvarId!.isInstanceTyped) && backward.isDefEq.instanceTypes.get (← getOptions) then
+      /- The value of an instance metavariable must be determined by instance synthesis, up
+         to defeq at `.instances` transparency: either the candidate value already is such a
+         value — with only admissible metavariables in its spine — and has the right type, or
+         we synthesize the instance now and require the candidate to be defeq to the result. -/
+      let v ← instantiateMVars v
+      if (← spineMVarsAdmissible v) then
+        let mvarType ← inferType mvar
+        let vType ← inferType v
+        if (← checkInstanceTypedTypes mvarType vType v) then
+          mvar.mvarId!.assign v
+          return true
+      synthInstanceTypedMVarAndUnify mvar v
     else
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
@@ -2161,21 +2322,17 @@ where
 
 /--
   Given applications `t` and `s` that are in WHNF (modulo the current transparency setting),
-  check whether they are definitionally equal or not.
+  check whether they are definitionally equal or not by comparing functions and arguments.
+  On failure, the caller is responsible for invoking `isDefEqAppFallback`.
 -/
 private def isDefEqApp (t s : Expr) : MetaM Bool := do
   let tFn := t.getAppFn
   let sFn := s.getAppFn
   if tFn.isConst && sFn.isConst && tFn.constName! == sFn.constName! then
     /- See comment at `tryHeuristic` explaining why we process arguments before universe levels. -/
-    if (← checkpointDefEq (isDefEqArgs tFn t.getAppArgs s.getAppArgs <&&> isListLevelDefEqAux tFn.constLevels! sFn.constLevels!)) then
-      return true
-    else
-      isDefEqOnFailure t s
-  else if (← checkpointDefEq (Meta.isExprDefEqAux tFn s.getAppFn <&&> isDefEqArgs tFn t.getAppArgs s.getAppArgs)) then
-    return true
+    checkpointDefEq (isDefEqArgs tFn t.getAppArgs s.getAppArgs <&&> isListLevelDefEqAux tFn.constLevels! sFn.constLevels!)
   else
-    isDefEqOnFailure t s
+    checkpointDefEq (Meta.isExprDefEqAux tFn s.getAppFn <&&> isDefEqArgs tFn t.getAppArgs s.getAppArgs)
 
 /-- Return `true` if the type of the given expression is an inductive datatype with a single constructor with no fields. -/
 private def isDefEqUnitLike (t : Expr) (s : Expr) : MetaM Bool := do
@@ -2202,6 +2359,48 @@ private def isDefEqProjInst (t : Expr) (s : Expr) : MetaM LBool := do
   else
     return .undef
 
+/--
+The special cases tried *after* the main `isExprDefEqExpensive` machinery has failed, as opposed
+to the early ones (`isDefEqNative`, `isDefEqNat`, `isDefEqOffset`).
+
+`.false` means one of them decided the terms are *not* definitionally equal, and must not be read
+as "declined". `.undef` means they all declined — note that `isDefEqUnitLike` returning `false`
+is a decline (the rule does not apply), not a negative verdict, hence `.undef`.
+-/
+private def isDefEqLateSpecialCases (t s : Expr) : MetaM LBool := do
+  match (← isDefEqProjInst t s) with
+  | .undef =>
+    match (← isDefEqStringLit t s) with
+    | .undef => return if (← isDefEqUnitLike t s) then .true else .undef
+    | r      => return r
+  | r => return r
+
+/--
+Fallback for a failing comparison of two applications; see `backward.isDefEq.appOnFailure`
+for the two behaviors.
+
+In the new behavior, `isDefEqOnFailure` runs before `isDefEqLateSpecialCases` because those
+unfold the class projections that `getStuckMVar?` needs to see an unsynthesized instance in an
+argument position. A stuck abort is not authoritative here — one of the late special cases may
+still close the goal — so it is deferred and re-raised only if they all decline.
+-/
+private def isDefEqAppFallback (t : Expr) (s : Expr) : MetaM Bool := do
+  if backward.isDefEq.appOnFailure.get (← getOptions) then
+    if (← isDefEqOnFailure t s) then return true
+    whenUndefDo (isDefEqLateSpecialCases t s) do
+    isDefEqOnFailure t s
+  else
+    let saved ← saveState
+    -- `none` records a deferred `isDefEqStuck`
+    let r? ← catchInternalId isDefEqStuckExceptionId (some <$> isDefEqOnFailure t s) fun _ => do
+      saved.restore
+      return none
+    if r? == some true then return true
+    if (← isDefEqLateSpecialCases t s) matches .true then return true
+    if r?.isNone then
+      Meta.throwIsDefEqStuck
+    return false
+
 private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
   whenUndefDo (isDefEqEta t s) do
   whenUndefDo (isDefEqEta s t) do
@@ -2223,12 +2422,11 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
       return true
     if t.isConst && s.isConst then
       if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
-    else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
-      return true
+    else if (← pure t.isApp <&&> pure s.isApp) then
+      if (← isDefEqApp t s) then return true
+      isDefEqAppFallback t s
     else
-      whenUndefDo (isDefEqProjInst t s) do
-      whenUndefDo (isDefEqStringLit t s) do
-      if (← isDefEqUnitLike t s) then return true else
+      whenUndefDo (isDefEqLateSpecialCases t s) do
       isDefEqOnFailure t s
 
 inductive DefEqCacheKind where
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 450d8edb60c6..652a6ebb5c22 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -352,6 +352,10 @@ def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext 
   let localInsts ← getLocalInstances
   forallTelescopeReducing mvarType fun xs mvarTypeBody => do
     let { subgoals, instVal, instTypeBody } ← getSubgoals lctx localInsts xs inst
+    -- Mark the instance-argument metavariables before unifying with the goal type, so that a
+    -- would-be assignment by unification must preserve the type at `.instances` transparency.
+    -- See `MetavarContext.instanceTypedMVars` and issue #9077.
+    subgoals.forM fun subgoal => subgoal.mvarId!.markInstanceTyped
     withTraceNode `Meta.synthInstance.tryResolve (fun _ => do withMCtx (← getMCtx) do
         return m!"{← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
     if (← isDefEq mvarTypeBody instTypeBody) then
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 3ad97d82016c..1fb6e098b6d7 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -370,6 +370,17 @@ structure MetavarContext where
   /-- Assignment table for delayed abstraction metavariables.
   For more information about delayed abstraction, see the docstring for `DelayedMetavarAssignment`. -/
   dAssignment    : PersistentHashMap MVarId DelayedMetavarAssignment := {}
+  /--
+  Metavariables whose assignments must preserve the type up to `TransparencyMode.instances`.
+
+  Metavariables created for the instance-implicit arguments of an instance during typeclass
+  resolution are added to this set, and membership is propagated to the metavariables in
+  type-determining (spine) positions of values assigned to members. This maintains the
+  invariant that the final instantiation of such a metavariable has a type that agrees with
+  the metavariable's type at `.instances` transparency, so unification cannot commit to an
+  instance for a type that is different at instance-resolution time. See issue #9077.
+  -/
+  instanceTypedMVars : PersistentHashMap MVarId Unit := {}
 
 instance : Inhabited MetavarContext := ⟨{}⟩
 
@@ -448,6 +459,20 @@ def _root_.Lean.MVarId.isAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m
 def _root_.Lean.MVarId.isDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool :=
   return (← getMCtx).dAssignment.contains mvarId
 
+/--
+Mark `mvarId` so that assignments to it must preserve its type up to
+`TransparencyMode.instances`. See `MetavarContext.instanceTypedMVars`.
+-/
+def _root_.Lean.MVarId.markInstanceTyped [MonadMCtx m] (mvarId : MVarId) : m Unit :=
+  modifyMCtx fun mctx => { mctx with instanceTypedMVars := mctx.instanceTypedMVars.insert mvarId () }
+
+/--
+Return `true` if assignments to `mvarId` must preserve its type up to
+`TransparencyMode.instances`. See `MetavarContext.instanceTypedMVars`.
+-/
+def _root_.Lean.MVarId.isInstanceTyped [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool :=
+  return (← getMCtx).instanceTypedMVars.contains mvarId
+
 /--
 Check whether a metavariable is assigned or delayed-assigned. A
 delayed-assigned metavariable is already 'solved' but the solution cannot be
diff --git a/tests/elab/9077.lean b/tests/elab/9077.lean
new file mode 100644
index 000000000000..25259fa7a2e9
--- /dev/null
+++ b/tests/elab/9077.lean
@@ -0,0 +1,127 @@
+/-!
+Regression test for #9077: instance synthesis must not commit to an instance for a type
+that is different at instance-resolution time (e.g. across a semireducible type synonym),
+which used to happen when unification assigned an instance metavariable a value of the
+wrong type.
+
+Tests both settings of `backward.isDefEq.instanceTypes`:
+- `false`: no restriction (the buggy pre-#9077-fix behavior),
+- `true`: reject wrong-typed assignments, falling back to synthesizing the instance and
+  unifying the candidate value with the result.
+-/
+
+class P (α : Type) where p : Nat
+class Q (α : Type) extends P α where
+structure H (α : Type) {p : P α} [p' : P α] (h : p = p') where
+class N (β : Type) where
+instance inst (α : Type) [q : Q α] : N (H α (p := q.toP) rfl) where
+
+def Copy (α : Type) := α
+
+set_option backward.isDefEq.respectTransparency false
+
+instance pCopy [P E] : P (Copy E) := (inferInstance : P E)
+
+/-!
+Scenario 1 (the original repro shape): `inst : N (H (Copy E) rfl)` needs `Q (Copy E)`, but
+we only have `iQ : Q E`, and these types are not instance-reducibly equal. With `false`,
+after `synthPending` fails to synthesize `?q : Q (Copy E)`, unification assigns it anyway:
+`pCopy (inst := iQ.toP) =?= ?q.toP` unfolds `pCopy`, giving `iQ.toP =?= ?q.toP` and finally
+`(?q : Q (Copy E)) := (iQ : Q E)`. With `true` this assignment is rejected, and since no
+`Q (Copy E)` instance exists, the synthesis fallback fails too.
+-/
+
+/-- info: inst (Copy E) -/
+#guard_msgs in
+set_option backward.isDefEq.instanceTypes false in
+variable (E : Type) [iQ : Q E] in
+#synth N (H (Copy E) rfl)
+
+/--
+error: failed to synthesize
+  N (H (Copy E) ⋯)
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+set_option backward.isDefEq.instanceTypes true in
+variable (E : Type) [iQ : Q E] in
+#synth N (H (Copy E) rfl)
+
+/-!
+Scenario 2: unification directly proposes `(?q : Q (Copy E)) := (iQ : Q E)` because the
+instance value occurs in the goal type. Without a `Q (Copy E)` instance, `false` exhibits
+the bug and `true` fails.
+-/
+
+structure G (α : Type) (q : Q α) where
+class M (β : Type) where
+instance instG (α : Type) [q : Q α] : M (G α q) where
+
+/-- info: instG (Copy E) -/
+#guard_msgs in
+set_option backward.isDefEq.instanceTypes false in
+variable (E : Type) [iQ : Q E] in
+#synth M (G (Copy E) iQ)
+
+/--
+error: failed to synthesize
+  M (G (Copy E) iQ)
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+set_option backward.isDefEq.instanceTypes true in
+variable (E : Type) [iQ : Q E] in
+#synth M (G (Copy E) iQ)
+
+/-!
+Scenario 3: like scenario 2, but the correct instance `qCopy : Q (Copy E)` exists and is
+definitionally equal to the rejected candidate `iQ`. Merely rejecting the assignment would
+fail here — this is the brittleness the synthesis fallback addresses: `true` synthesizes
+`qCopy`, unifies it with the candidate, and succeeds.
+-/
+
+instance qCopy [Q E] : Q (Copy E) := ‹Q E›
+
+/-- info: instG (Copy E) -/
+#guard_msgs in
+set_option backward.isDefEq.instanceTypes false in
+variable (E : Type) [iQ : Q E] in
+#synth M (G (Copy E) iQ)
+
+/-- info: instG (Copy E) -/
+#guard_msgs in
+set_option backward.isDefEq.instanceTypes true in
+variable (E : Type) [iQ : Q E] in
+#synth M (G (Copy E) iQ)
+
+/-!
+Scenario 4 (minimized from `let x : Std.HashSet _ := ∅` in Mathlib): the goal type contains
+the *caller's* pending instance metavariables (created for the instance-implicit arguments
+of `Box` while its type argument is still undetermined), and unification assigns them to the
+search's subgoal metavariables. These caller metavariables are not assignable during the
+search, so `true` accepts them in the spine rather than demanding an mvar-free value it
+could not synthesize; the elaborator synthesizes them later, once `useBox x` determines the
+type argument.
+-/
+
+class R (α : Type) where
+structure Box (α : Type) [R α] where mk' ::
+class Init (γ : Type) where init : γ
+instance instR : R Nat := ⟨⟩
+instance instInitBox (α : Type) [R α] : Init (Box α) := ⟨⟨⟩⟩
+
+def useBox (_b : Box Nat) : Nat := 0
+
+#guard_msgs in
+set_option backward.isDefEq.instanceTypes false in
+example : Nat :=
+  let x : Box _ := Init.init
+  useBox x
+
+#guard_msgs in
+set_option backward.isDefEq.instanceTypes true in
+example : Nat :=
+  let x : Box _ := Init.init
+  useBox x
diff --git a/tests/elab/isDefEqArgsFirstPassBump.lean b/tests/elab/isDefEqArgsFirstPassBump.lean
new file mode 100644
index 000000000000..f9e03e4b13a7
--- /dev/null
+++ b/tests/elab/isDefEqArgsFirstPassBump.lean
@@ -0,0 +1,41 @@
+/-!
+The first pass of `isDefEqArgs` must apply the `.implicit` transparency bump too.
+
+Reduced from `CategoryTheory.Abelian.subobjectIsoSubobjectOp` in Mathlib's
+`CategoryTheory/Abelian/Subobject.lean` — the order isomorphism
+`Subobject X ≃o (Subobject (op X))ᵒᵈ` — whose proof stops elaborating without the bump,
+failing to synthesize `Mono (kernel.ι (cokernel.π f))`.
+
+`isDefEqArgsFirstPass` unifies an argument pair eagerly when one side is an unassigned
+metavariable, instead of postponing it to the second pass. Such a pair is still an argument
+unification at an implicit position, so it gets the same transparency bump as the second pass:
+whether an argument is checked at `.implicit` must not depend on which side happens to be an
+unassigned metavariable.
+
+Below, synthesizing `Mono (limitPi f)` applies `limitPiMono`, whose conclusion is
+`Mono (limitPi ?f ?inst)`. The instance-implicit `?inst` is unassigned, so the first pass takes
+the eager branch and assigns it `h`. Checking that assignment compares `HasLimit f` against
+`HasLimit (ofOpp (toOpp f))`, which fails at `.instances` because `ofOpp` and `toOpp` are
+`implicit_reducible`. The `backward.isDefEq.instanceTypes` fallback then synthesizes `HasLimit f`
+via `hasLimitAll` and compares `h` against the result — and *that* comparison runs at the ambient
+transparency. Bumped to `.implicit` it reduces `ofOpp (toOpp f)` to `f` and the two proofs match;
+at `.instances` it does not, and synthesis fails with `failed to synthesize Mono (limitPi f)`.
+
+There the assignment reads
+`(?m : HasEqualizer (cokernel.π f) 0) := (h : HasKernel (cokernel.π f).op.unop)`, and the
+`implicit_reducible` definitions are `Quiver.Hom.op` and `Quiver.Hom.unop`.
+-/
+
+@[implicit_reducible] def toOpp (a : Nat) : Nat := a
+@[implicit_reducible] def ofOpp (a : Nat) : Nat := a
+
+class HasLimit (f : Nat) : Prop where
+instance hasLimitAll (f : Nat) : HasLimit f := ⟨⟩
+
+opaque limitObj : Nat → Nat
+def limitPi (f : Nat) [HasLimit f] : Nat := limitObj f
+
+class Mono (g : Nat) : Prop where
+instance limitPiMono (f : Nat) [HasLimit f] : Mono (limitPi f) := ⟨⟩
+
+example (f : Nat) (h : HasLimit (ofOpp (toOpp f))) : Mono (@limitPi f h) := inferInstance
diff --git a/tests/elab/isDefEqCheckAssignmentBug.lean.out.expected b/tests/elab/isDefEqCheckAssignmentBug.lean.out.expected
index cfa49dc07175..91a3389d137b 100644
--- a/tests/elab/isDefEqCheckAssignmentBug.lean.out.expected
+++ b/tests/elab/isDefEqCheckAssignmentBug.lean.out.expected
@@ -28,10 +28,6 @@
         [Meta.isDefEq.onFailure] ❌️ ReaderT Elab.Command.Context
               (StateRefT' IO.RealWorld Elab.Command.State
                 (EIO Exception)) =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM)
-        [Meta.isDefEq.onFailure] ❌️ ReaderT Elab.Command.Context
-              (StateRefT' IO.RealWorld Elab.Command.State
-                (EIO Exception)) =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM)
-  [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM Elab.Command.CommandElabM =?= MonadEvalT ?m ?m
   [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM Elab.Command.CommandElabM =?= MonadEvalT ?m ?m
 [Meta.isDefEq] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM =?= MonadEvalT ?m ?m
   [Meta.isDefEq] ✅️ MetaM =?= ?m
@@ -56,10 +52,10 @@
   [Meta.isDefEq] ✅️ Elab.Command.CommandElabM =?= Elab.Command.CommandElabM
 [Meta.isDefEq] ✅️ ?m =?= Elab.Command.instMonadEvalTermElabMCommandElabM
   [Meta.isDefEq] ?m [assignable] =?= Elab.Command.instMonadEvalTermElabMCommandElabM [nonassignable]
-  [Meta.isDefEq.transparency] raising transparency instances → implicit
   [Meta.isDefEq] ✅️ MonadEval ?m Elab.Command.CommandElabM =?= MonadEval Elab.TermElabM Elab.Command.CommandElabM
     [Meta.isDefEq] ✅️ ?m =?= Elab.TermElabM
       [Meta.isDefEq] ?m [assignable] =?= Elab.TermElabM [nonassignable]
+      [Meta.isDefEq.transparency] raising transparency instances → implicit
       [Meta.isDefEq] ✅️ Type → Type ?u =?= Type → Type
         [Meta.isDefEq] ✅️ Type =?= Type
         [Meta.isDefEq] ✅️ Type ?u =?= Type
@@ -78,9 +74,6 @@
         [Meta.isDefEq] ❌️ Elab.Term.Context =?= Context
         [Meta.isDefEq.onFailure] ❌️ ReaderT Elab.Term.Context
               (StateRefT' IO.RealWorld Elab.Term.State MetaM) =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM)
-        [Meta.isDefEq.onFailure] ❌️ ReaderT Elab.Term.Context
-              (StateRefT' IO.RealWorld Elab.Term.State MetaM) =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM)
-  [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM Elab.TermElabM =?= MonadEvalT ?m ?m
   [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM Elab.TermElabM =?= MonadEvalT ?m ?m
 [Meta.isDefEq] ✅️ MonadEvalT MetaM Elab.TermElabM =?= MonadEvalT ?m ?m
   [Meta.isDefEq] ✅️ MetaM =?= ?m
@@ -110,7 +103,6 @@
       [Meta.isDefEq] ✅️ Type ?u =?= Type
 [Meta.isDefEq] ✅️ ?m =?= instMonadEvalOfMonadLift
   [Meta.isDefEq] ?m [assignable] =?= instMonadEvalOfMonadLift [nonassignable]
-  [Meta.isDefEq.transparency] raising transparency instances → implicit
   [Meta.isDefEq] ✅️ MonadEval ?m Elab.TermElabM =?= MonadEval ?m Elab.TermElabM
     [Meta.isDefEq] ✅️ ?m =?= ?m
     [Meta.isDefEq] ✅️ Elab.TermElabM =?= Elab.TermElabM
@@ -135,12 +127,12 @@
           [Meta.isDefEq] ✅️ Type ?u =?= Type
 [Meta.isDefEq] ✅️ ?m =?= ReaderT.instMonadLift
   [Meta.isDefEq] ?m [assignable] =?= ReaderT.instMonadLift [nonassignable]
-  [Meta.isDefEq.transparency] raising transparency instances → implicit
   [Meta.isDefEq] ✅️ MonadLift ?m
         Elab.TermElabM =?= MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
         (ReaderT Elab.Term.Context (StateRefT' IO.RealWorld Elab.Term.State MetaM))
     [Meta.isDefEq] ✅️ ?m =?= StateRefT' IO.RealWorld Elab.Term.State MetaM
       [Meta.isDefEq] ?m [assignable] =?= StateRefT' IO.RealWorld Elab.Term.State MetaM [nonassignable]
+      [Meta.isDefEq.transparency] raising transparency instances → implicit
       [Meta.isDefEq] ✅️ Type → Type ?u =?= Type → Type
         [Meta.isDefEq] ✅️ Type =?= Type
         [Meta.isDefEq] ✅️ Type ?u =?= Type
@@ -150,11 +142,11 @@
               MetaM) =?= ReaderT Elab.Term.Context (StateRefT' IO.RealWorld Elab.Term.State MetaM)
 [Meta.isDefEq] ✅️ ?m =?= instMonadEvalOfMonadLift
   [Meta.isDefEq] ?m [assignable] =?= instMonadEvalOfMonadLift [nonassignable]
-  [Meta.isDefEq.transparency] raising transparency instances → implicit
   [Meta.isDefEq] ✅️ MonadEval ?m
         Elab.TermElabM =?= MonadEval (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
     [Meta.isDefEq] ✅️ ?m =?= StateRefT' IO.RealWorld Elab.Term.State MetaM
       [Meta.isDefEq] ?m [assignable] =?= StateRefT' IO.RealWorld Elab.Term.State MetaM [nonassignable]
+      [Meta.isDefEq.transparency] raising transparency instances → implicit
       [Meta.isDefEq] ✅️ Type → Type ?u =?= Type → Type
         [Meta.isDefEq] ✅️ Type =?= Type
         [Meta.isDefEq] ✅️ Type ?u =?= Type
@@ -183,10 +175,6 @@
                 [Meta.isDefEq.onFailure] ❌️ ST.Ref IO.RealWorld Elab.Term.State =?= Context
               [Meta.isDefEq.onFailure] ❌️ ReaderT (ST.Ref IO.RealWorld Elab.Term.State) MetaM
                     α =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) α
-              [Meta.isDefEq.onFailure] ❌️ ReaderT (ST.Ref IO.RealWorld Elab.Term.State) MetaM
-                    α =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) α
-  [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM
-        (StateRefT' IO.RealWorld Elab.Term.State MetaM) =?= MonadEvalT ?m ?m
   [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM
         (StateRefT' IO.RealWorld Elab.Term.State MetaM) =?= MonadEvalT ?m ?m
 [Meta.isDefEq] ✅️ MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM) =?= MonadEvalT ?m ?m
@@ -217,7 +205,6 @@
       [Meta.isDefEq] ✅️ Type ?u =?= Type
 [Meta.isDefEq] ✅️ ?m =?= instMonadEvalOfMonadLift
   [Meta.isDefEq] ?m [assignable] =?= instMonadEvalOfMonadLift [nonassignable]
-  [Meta.isDefEq.transparency] raising transparency instances → implicit
   [Meta.isDefEq] ✅️ MonadEval ?m
         (StateRefT' IO.RealWorld Elab.Term.State
           MetaM) =?= MonadEval ?m (StateRefT' IO.RealWorld Elab.Term.State MetaM)
@@ -246,24 +233,24 @@
       [Meta.isDefEq] ✅️ Type → Type =?= Type → Type
 [Meta.isDefEq] ✅️ ?m =?= StateRefT'.instMonadLift
   [Meta.isDefEq] ?m [assignable] =?= StateRefT'.instMonadLift [nonassignable]
-  [Meta.isDefEq.transparency] raising transparency instances → implicit
   [Meta.isDefEq] ✅️ MonadLift ?m
         (StateRefT' IO.RealWorld Elab.Term.State
           MetaM) =?= MonadLift MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.isDefEq] ✅️ ?m =?= MetaM
       [Meta.isDefEq] ?m [assignable] =?= MetaM [nonassignable]
+      [Meta.isDefEq.transparency] raising transparency instances → implicit
       [Meta.isDefEq] ✅️ Type → Type ?u =?= Type → Type
         [Meta.isDefEq] ✅️ Type =?= Type
         [Meta.isDefEq] ✅️ Type ?u =?= Type
     [Meta.isDefEq] ✅️ StateRefT' IO.RealWorld Elab.Term.State MetaM =?= StateRefT' IO.RealWorld Elab.Term.State MetaM
 [Meta.isDefEq] ✅️ ?m =?= instMonadEvalOfMonadLift
   [Meta.isDefEq] ?m [assignable] =?= instMonadEvalOfMonadLift [nonassignable]
-  [Meta.isDefEq.transparency] raising transparency instances → implicit
   [Meta.isDefEq] ✅️ MonadEval ?m
         (StateRefT' IO.RealWorld Elab.Term.State
           MetaM) =?= MonadEval MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.isDefEq] ✅️ ?m =?= MetaM
       [Meta.isDefEq] ?m [assignable] =?= MetaM [nonassignable]
+      [Meta.isDefEq.transparency] raising transparency instances → implicit
       [Meta.isDefEq] ✅️ Type → Type ?u =?= Type → Type
         [Meta.isDefEq] ✅️ Type =?= Type
         [Meta.isDefEq] ✅️ Type ?u =?= Type
@@ -278,14 +265,12 @@
   [Meta.isDefEq] ✅️ MetaM =?= MetaM
 [Meta.isDefEq] ✅️ ?m =?= instMonadEvalT MetaM
   [Meta.isDefEq] ?m [assignable] =?= instMonadEvalT MetaM [nonassignable]
-  [Meta.isDefEq.transparency] raising transparency instances → implicit
   [Meta.isDefEq] ✅️ MonadEvalT MetaM MetaM =?= MonadEvalT MetaM MetaM
     [Meta.isDefEq] ✅️ MetaM =?= MetaM
     [Meta.isDefEq] ✅️ MetaM =?= MetaM
 [Meta.isDefEq] ✅️ ?m =?= instMonadEvalTOfMonadEval MetaM MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
   [Meta.isDefEq] ?m [assignable] =?= instMonadEvalTOfMonadEval MetaM MetaM
         (StateRefT' IO.RealWorld Elab.Term.State MetaM) [nonassignable]
-  [Meta.isDefEq.transparency] raising transparency instances → implicit
   [Meta.isDefEq] ✅️ MonadEvalT MetaM
         (StateRefT' IO.RealWorld Elab.Term.State
           MetaM) =?= MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
@@ -295,7 +280,6 @@
       Elab.TermElabM
   [Meta.isDefEq] ?m [assignable] =?= instMonadEvalTOfMonadEval MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
         Elab.TermElabM [nonassignable]
-  [Meta.isDefEq.transparency] raising transparency instances → implicit
   [Meta.isDefEq] ✅️ MonadEvalT MetaM Elab.TermElabM =?= MonadEvalT MetaM Elab.TermElabM
     [Meta.isDefEq] ✅️ MetaM =?= MetaM
     [Meta.isDefEq] ✅️ Elab.TermElabM =?= Elab.TermElabM
diff --git a/tests/elab/isDefEqProjInstHardFalse.lean b/tests/elab/isDefEqProjInstHardFalse.lean
new file mode 100644
index 000000000000..0b21f476a4d9
--- /dev/null
+++ b/tests/elab/isDefEqProjInstHardFalse.lean
@@ -0,0 +1,47 @@
+import Lean
+
+/-!
+`isDefEqProjInst` must report a failed comparison as `.false`, not `.undef`.
+
+It decides `k =?= C.op instA ?m` by unfolding the instance projection and running a full
+comparison on the result. Reporting `.false` short-circuits the remaining heuristics in
+`isExprDefEqExpensive`. Were it to report `.undef` instead — as a "soft" variant that declines
+whenever either side contains a metavariable would — `isDefEqOnFailure` would run again on the
+original, un-unfolded pair, redoing stuck-metavariable synthesis and unification-hint lookups
+for a comparison that has already been decided. That cost compounds: the enclosing comparison is
+retried at every unfolding stage, so it grows with the nesting depth of the projections.
+
+That variant was measured against Mathlib: `RingTheory/Regular/RegularSequence.lean` went from
+8159 to 98939 `isDefEqOnFailure` invocations (12x) and stopped compiling, exhausting the
+heartbeat budget around `IsWeaklyRegular.prototype_perm` — still timing out at 20x the default
+limit.
+
+This test pins that cost rather than a particular implementation. `k` is opaque, so none of the
+200 comparisons below can succeed; the only question is how much work is spent failing. Cost is
+linear in the iteration count with no measurable fixed overhead, so the margins are set by the
+depth: the budget is roughly 3x what the `.false` version needs, while the declining variant needs
+about 12x. It therefore fails here with a deterministic timeout instead of a silent slowdown.
+-/
+
+open Lean Meta
+
+class C (α : Type) where
+  op : α → α
+
+instance instA : C Nat := ⟨fun n => n + 1⟩
+
+opaque k : Nat
+
+/-- `C.op instA (C.op instA (... e))`, `depth` applications deep. -/
+def nest : Nat → Expr → Expr
+  | 0,   e => e
+  | n+1, e => mkApp3 (mkConst ``C.op) (mkConst ``Nat) (mkConst ``instA) (nest n e)
+
+def tst (depth iters : Nat) : MetaM Unit :=
+  withTransparency .instances do
+    for _ in [0:iters] do
+      let m ← mkFreshExprMVar (mkConst ``Nat)
+      discard <| isDefEq (mkConst ``k) (nest depth m)
+
+set_option maxHeartbeats 1200 in
+run_meta tst 400 200
diff --git a/tests/elab/isDefEqProjInstWithMVar.lean b/tests/elab/isDefEqProjInstWithMVar.lean
new file mode 100644
index 000000000000..c4def255c982
--- /dev/null
+++ b/tests/elab/isDefEqProjInstWithMVar.lean
@@ -0,0 +1,52 @@
+/-!
+MWE: `isDefEqApp` calls `isDefEqOnFailure` itself, so a stuck outer-level instance
+metavariable throws before `isExprDefEqExpensive` ever reaches `isDefEqProjInst`.
+-/
+
+/-- like `CommSemiring` -/
+class K (α : Type) extends Mul α where
+
+class Op (α : Type) where
+  f : α → α → α
+
+/-- Two definitionally equal spellings of the same `Op α`, as in the `Module R R` diamond. -/
+@[reducible] def opStar (α : Type) [K α] : Op α := ⟨fun x y => x * y⟩
+@[reducible] def opMul  (α : Type) [K α] : Op α := ⟨fun x y => Mul.mul x y⟩
+
+/-- Carries an `Op α` instance argument, like `M ⊗[R] N` carries `Module R R`. -/
+structure T (α : Type) (k : K α) [Op α] where
+  val : α
+
+class Sem (X : Type)
+instance instSem (α : Type) (k : K α) : Sem (@T α k (@opMul α k)) := ⟨⟩
+
+structure Box (α : Type) (k : K α)
+structure Hom (α : Type) (k : K α) where run : Box α k → Nat
+
+instance instCoeFunHom (α : Type) (k : K α) [Sem (@T α k (@opStar α k))] :
+    CoeFun (Hom α k) (fun _ => Box α k → Nat) := ⟨Hom.run⟩
+
+def h {α : Type} {k : K α} : Hom α k := ⟨fun _ => 0⟩
+
+@[reducible] def kNat : K Nat where
+  mul a _ := a
+
+/-!
+The error previously was:
+---
+error: Function expected at
+  h
+but this term has type
+  Hom ?m.1 ?m.2
+
+Note: Expected a function because this term is being applied to the argument
+  b
+---
+Reason: `[implicit] HMul.hmul x y =?= Mul.mul x y`, involving a `Mul` mvar, fails.
+`isDefEqApp` calls `isDefEqOnFailure`, which finds the mvar and throws a stuck exception.
+Lean can't synthesize the mvar though, so we fail hard before trying `isDefEqProjInst`.
+
+This was fixed by deferring the stuck exception until `isDefEqProjInst` was tried.
+-/
+
+example (b : Box Nat kNat) : Nat := h b