Unification sees through type synonyms when checking instances' types

Prerequisites

• 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

Unification of (?inst).toMyClass =?= i.toMyClass assigns ?inst := i whenever ?inst : A and i : B have the same type at implicit transparency, not instance transparency. In particular, i : B might not be the instance expected for an instance-implicit argument of type A.

Context

This problem occurred in Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/LeviCivita.lean.

Steps to Reproduce

Mathlib-free reproducer:

class Topo (α : Type) where nhd : α → α → Prop
class Nrm (α : Type) extends Topo α where norm : α → Nat
structure Total {B : Type} (E : B → Type) where
  base : B
  fib  : E base

class Fib {B : Type} (E : B → Type) [∀ b, Topo (E b)] where chart : B → B

instance totalTopo {B : Type} [Topo B] {E : B → Type} [∀ b, Topo (E b)] [Fib E] :
    Topo (Total E) := ⟨fun _ _ => True⟩

def Diff {M N : Type} [Topo M] [Topo N] (_f : M → N) : Prop := True

theorem inner_bundle {B : Type} [Topo B] {E : B → Type}
    [nE : ∀ b, Nrm (E b)] [Fib E] {f g : ∀ b, E b}
    (_hf : Diff fun b => (⟨b, f b⟩ : Total E))
    (_hg : Diff fun b => (⟨b, g b⟩ : Total E)) :
    ∀ b, (nE b).norm (f b) = (nE b).norm (g b) := sorry

def Tan (E : Type) (B : Type) (_b : B) : Type := E

instance tanTopo (E : Type) [nE : Nrm E] (B : Type) (b : B) : Topo (Tan E B b) := nE.toTopo
instance tanFib (E : Type) [Nrm E] (B : Type) : Fib (Tan E B) := ⟨id⟩

class RB {B : Type} (E : B → Type) [∀ b, Topo (E b)] where g : ∀ b, E b → Nat

instance rbNrm {B : Type} {E : B → Type} [tE : ∀ b, Topo (E b)] [rb : RB E] (b : B) : Nrm (E b) where
  toTopo := tE b
  norm := rb.g b

section
variable (E : Type) [Nrm E] (B : Type) [Topo B] [RB (Tan E B)] (f g : ∀ b, Tan E B b)

/--
error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  fun b => rbNrm b
inferred
  fun b => inst✝²
-/
#guard_msgs in
example (hf : Diff fun b => (⟨b, f b⟩ : Total (Tan E B)))
        (hg : Diff fun b => (⟨b, g b⟩ : Total (Tan E B))) :=
  inner_bundle hf hg

-- works with an explicit expected type, which enforces the expected instance
example (hf : Diff fun b => (⟨b, f b⟩ : Total (Tan E B)))
        (hg : Diff fun b => (⟨b, g b⟩ : Total (Tan E B))) :
    ∀ b, (rbNrm b).norm (f b) = (rbNrm b).norm (g b) :=
  inner_bundle hf hg

end

Reproducer closer to Mathlib:

module

public import Mathlib.Analysis.InnerProductSpace.Dual
public import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
public import Mathlib.Geometry.Manifold.Riemannian.Basic
public import Mathlib.Geometry.Manifold.VectorField.LieBracket
meta import Lean.PostprocessTraces
open Lean.PostprocessTraces

open Bundle FiberBundle Function NormedSpace VectorField

open scoped Manifold ContDiff Bundle
variable
  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  {M : Type*} [EMetricSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
  [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
  [IsContMDiffRiemannianBundle I ∞ E (fun (x : M) ↦ TangentSpace I x)]
  [IsRiemannianManifold I M]
  {X Y Z : Π x : M, TangentSpace I x}

local notation "⟪" X ", " Y "⟫" => fun x ↦ inner ℝ (X x) (Y x)

lemma _root_.MDifferentiableAt.inner_bundle' {x : M} {X Y : Π x : M, TangentSpace I x}
    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) :
    MDiffAt ⟪X, Y⟫ x :=
  MDifferentiableAt.inner_bundle hX hY


variable {x : M} (hY : MDiffAt (T% Y) x)  (hZ : MDiffAt (T% Z) x)

postprocess_traces
  filterSubtrees (ofClass `Meta.isDefEq.assign.checkTypes)
  >=> exposeSubtrees (fun x => ofClass `Meta.isDefEq.assign.checkTypes x <&&> containsString "NormedAddCommGroup (TangentSpace I x)" x)
in
set_option trace.Meta.isDefEq.assign.checkTypes true in
set_option trace.Meta.isDefEq.printTransparency true in
set_option trace.Meta.isDefEq true in
set_option trace.Meta.synthInstance true in
#check hY.inner_bundle hZ

Expected behavior:

• Lean's errors should be easy to understand and fix.
• Possibly: Lean should not assign instances of the wrong type (at instance transparency) to an instance-implicit metavariable during unification.
• Lean should not assign instances during unification that it will reject at a later point.

Actual behavior:

From the Mathlib reproducer's trace:

``lean
[] ❌️ [default] (instNormedAddCommGroupOfRiemannianBundleOfIsTopologicalAddGroupOfContinuousConstSMulReal
b).toMetricSpace =?= inst✝⁸.toMetricSpace ▶
[] ✅️ [default] NormedAddCommGroup.toMetricSpace.1 =?= inst✝⁸.toMetricSpace.1 ▼
[] ✅️ [default] TangentSpace I b =?= E ▶
[synthInstance] ✅️ (x : M) → NormedAddCommGroup (TangentSpace I x) ▶
[] ❌️ [default] instNormedAddCommGroupOfRiemannianBundleOfIsTopologicalAddGroupOfContinuousConstSMulReal b =?= inst✝⁸ ▶
[] ✅️ [default] (?m.114 b).3 =?= inst✝⁸.3 ▼
[] ?m.114 b [assignable] =?= inst✝⁸ [nonassignable]
[assign.checkTypes] ✅️ (?m.114 : (x : M) → NormedAddCommGroup (TangentSpace I x)) := (fun b => inst✝⁸ : M → NormedAddCommGroup E) ▼

Confronted with the unification problem `(someInstanceDerivedFrom ?i).toMetricSpace =?= (someInstanceDerivedFrom j).toMetricSpace` and speculatively tries `?i =?= j`. The assignment succeeds. Later, the term elaborator checks whether `?i`'s assigned instance matches the synthesized instance, which it doesn't, and it fails. The instance assigned by unification is an unexpected, wrong, instance.

This does *not* happen during instance search, in contrast to issue #9077.

### Versions

Lean 4.35.0-nightly-2026-08-27
Target: x86_64-unknown-linux-gnu Linux

### Additional Information

I'm already working on finding a fix for this issue and opened this for documentation purposes.

### Impact

Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others are impacted by this issue, please ask them to add :+1: to it.