"failed to synthesize instance" despite local instance

[tom93]

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

I'm working with complex instances, and synthesis fails even when I explicitly create a local instance.

Steps to Reproduce

I couldn't reduce the example further without losing the error. Update: I found a smaller reproducer, see the comment below.

Example

class IsNamedTypeDecl (α : Type) (TypeParam : outParam Type) where
  name : α →  String
  typeParams : α → List TypeParam

abbrev IsNamedTypeDecl.numParams {α TypeParam} [IsNamedTypeDecl α TypeParam] (decl : α) : Nat :=
  (IsNamedTypeDecl.typeParams decl).length

-- We have to use `List` rather than `Vector` due to https://www.github.com/leanprover/lean4/issues/1964.
inductive MyType (TypeParam NamedTypeDecl : Type) [IsNamedTypeDecl NamedTypeDecl TypeParam] where
  | typeParam (_ : TypeParam)
  | namedType (decl : NamedTypeDecl) (typeArgs : List (MyType TypeParam NamedTypeDecl))

abbrev MyType.instantiate {TypeParam NamedTypeDecl} [IsNamedTypeDecl NamedTypeDecl TypeParam]
    (decl : NamedTypeDecl) (typeArgs : Vector (MyType TypeParam NamedTypeDecl) (IsNamedTypeDecl.numParams decl)) :
    MyType TypeParam NamedTypeDecl :=
  .namedType decl typeArgs.toList

instance (TypeParam NamedTypeDecl) [IsNamedTypeDecl NamedTypeDecl TypeParam]
    [DecidableEq TypeParam] [DecidableEq NamedTypeDecl] :
    DecidableEq (MyType TypeParam NamedTypeDecl) :=
  go
where
  go l r := by
    cases l <;> cases r
    any_goals exact .isFalse (fun h => MyType.noConfusion rfl rfl (heq_of_eq rfl) (heq_of_eq h))
    next => rw [MyType.typeParam.injEq]; exact inferInstance
    next declₗ typeArgsₗ declᵣ typeArgsᵣ =>
      let := List_hasDecEq typeArgsₗ typeArgsᵣ
      rw [MyType.namedType.injEq]; exact inferInstance
  termination_by structural l
  List_hasDecEq : (a b : List _) → Decidable (Eq a b)
      | .nil,       .nil       => isTrue rfl
      | .cons _ _,  .nil       => isFalse (fun h => List.noConfusion rfl (heq_of_eq h))
      | .nil,       .cons _ _  => isFalse (fun h => List.noConfusion rfl (heq_of_eq h))
      | .cons a as, .cons b bs =>
        match (go a b) with
        | isTrue hab  =>
          match List_hasDecEq as bs with
          | isTrue habs  => isTrue (hab ▸ habs ▸ rfl)
          | isFalse nabs => isFalse (fun h => List.noConfusion rfl (heq_of_eq h) (fun _ habs => absurd (eq_of_heq habs) nabs))
        | isFalse nab => isFalse (fun h => List.noConfusion rfl (heq_of_eq h) (fun hab _ => absurd (eq_of_heq hab)   nab))

-- Somewhat similar to `Vector.instDecidableExistsVectorSucc`, but for a specific form of `P` to allow the search to be pruned (and supports arbitrary `n`).
instance (priority := high) Vector_instDecidableForallVectorIdx' {n α} (Q : Fin n → α → Prop) (P : (xs : Vector α n) → (∀ (i : Fin n), Q i xs[i]) → Prop)
    [∀ i x, Decidable (Q i x)] [∀ xs hQxs, Decidable (P xs hQxs)] [∀ R, [DecidablePred R] → Decidable (∀ (x : α), R x)] :
    Decidable (∀ xs, (hQxs : ∀ (i : Fin n), Q i xs[i]) → P xs hQxs) := by
  sorry

def Sound {TypeParam NamedTypeDecl} [IsNamedTypeDecl NamedTypeDecl TypeParam]
    (alg : MyType TypeParam NamedTypeDecl → List String)
    (decl : NamedTypeDecl) :
    Prop :=
  ∀ (argsₗ : Vector (MyType ..) (IsNamedTypeDecl.numParams decl))
    (h_argsₗ : ∀ (i : Fin (IsNamedTypeDecl.numParams decl)), alg argsₗ[i] ⊆ alg (.typeParam (IsNamedTypeDecl.typeParams decl)[i]))
    (argsᵤ : Vector (MyType ..) (IsNamedTypeDecl.numParams decl))
    (h_argsᵤ : ∀ (i : Fin (IsNamedTypeDecl.numParams decl)), alg argsᵤ[i] ⊆ alg (.typeParam (IsNamedTypeDecl.typeParams decl)[i]) ∧ (argsᵤ[i] matches .typeParam _ ∨ argsᵤ[i] = argsₗ[i])),
  alg (.instantiate decl argsₗ) ⊆ alg (.instantiate decl argsᵤ)

set_option synthInstance.maxHeartbeats 1000000
set_option synthInstance.maxSize 10000
--set_option trace.Meta.synthInstance true

instance {TypeParam NamedTypeDecl} [IsNamedTypeDecl NamedTypeDecl TypeParam]
    [DecidableEq TypeParam] [DecidableEq NamedTypeDecl]
    [∀ (R : MyType TypeParam NamedTypeDecl → Prop), Decidable (∀ x, R x)]
    (alg : MyType TypeParam NamedTypeDecl → List String)
    (decl : NamedTypeDecl) :
    Decidable (Sound alg decl) := by
  unfold Sound
  let localInstance : -- The type was copied directly from the Lean error message.
      (xs : Vector (MyType TypeParam NamedTypeDecl) (IsNamedTypeDecl.numParams decl)) →
      (hQxs :
          ∀ (i : Fin (IsNamedTypeDecl.numParams decl)),
            alg xs[i] ⊆ alg (MyType.typeParam (IsNamedTypeDecl.typeParams decl)[i])) →
        Decidable
          (∀ (argsᵤ : Vector (MyType TypeParam NamedTypeDecl) (IsNamedTypeDecl.numParams decl)),
            (∀ (i : Fin (IsNamedTypeDecl.numParams decl)),
                alg argsᵤ[i] ⊆ alg (MyType.typeParam (IsNamedTypeDecl.typeParams decl)[i]) ∧
                  ((match argsᵤ[i] with
                      | MyType.typeParam x => true
                      | x => false) =
                      true ∨
                    argsᵤ[i] = xs[i])) →
              alg (MyType.instantiate decl xs) ⊆ alg (MyType.instantiate decl argsᵤ)) :=
    fun xs hQxs => by
      apply Vector_instDecidableForallVectorIdx' (Q := fun i x => alg x ⊆ alg _ ∧ ((x matches .typeParam _ ∨ x = _)))
  apply @Vector_instDecidableForallVectorIdx' _ _
    (Q := fun i x => alg x ⊆ alg (.typeParam (IsNamedTypeDecl.typeParams decl)[i]))
    (P := fun argsₗ h_argsₗ =>
      ∀ (argsᵤ : Vector (MyType TypeParam NamedTypeDecl) (IsNamedTypeDecl.numParams decl))
      (h_argsᵤ :
        ∀ (i : Fin (IsNamedTypeDecl.numParams decl)),
          alg argsᵤ[i] ⊆ alg (MyType.typeParam (IsNamedTypeDecl.typeParams decl)[i]) ∧
            ((match argsᵤ[i] with
                | MyType.typeParam x => true
                | x => false) =
                true ∨
              argsᵤ[i] = argsₗ[i])),
      alg (.instantiate decl argsₗ) ⊆ alg (.instantiate decl argsᵤ))
    _
    _ -- changing this underscore to `localInstance` makes the error go away
    _

Error message: "failed to synthesize instance of type class ..."

Changing the second-to-last underscore to localInstance makes the error go away.

I tried increasing synthInstance.maxHeartbeats and synthInstance.maxSize as shown but it didn't help.

Versions

Nightly 2026-07-18, v4.32.0, 4.28.1.

Additional Information

In my original example (before I minimised it), I saw a very puzzling message from trace.Meta.synthInstance, it said "apply localInstance to ... result type X is not definitionally equal to Y" where X and Y are long but identical. I can post this example if it's useful.

[tom93]

I found a simpler reproducer:

def decideForallVector {α} {n : Nat} (P : Vector α n → Prop)
    [DecidablePred P]
    (h : ∀ (Q : α → Prop), DecidablePred Q → Decidable (∀ x : α, Q x)) :
    Decidable (∀ (xs : Vector α n), P xs) := by
  -- The proof is not important (could be replaced with `sorry`).
  cases n with
  | zero => exact Vector.instDecidableForallVectorZero P
  | succ n =>
    have : Decidable (∀ x xs, P (.push xs x)) := by
      have : ∀ x xs, Decidable (P (Vector.push xs x)) := inferInstance
      have (x : α) : Decidable (∀ (xs : Vector α n), P (xs.push x)) := by
        exact decideForallVector _ h
      apply h
      assumption
    apply Vector.instDecidableForallVectorSucc

instance instDecidableForallVector (α n) (P : Vector α n → Prop)
    [DecidablePred P]
    [h : ∀ (Q : α → Prop), [DecidablePred Q] → Decidable (∀ x : α, Q x)] :
    Decidable (∀ xs, P xs) := by
  -- Likewise can be replaced with `sorry`.
  apply decideForallVector
  exact fun _ _ => h _

example (n : Nat) : Decidable (∀ (xs : Vector (Fin 5) n), (∀ (i : Fin n), xs[i].val % 2 = 0) → (xs.map (·.val)).sum % 2 = 0) := by
  have : (Q : Fin 5 → Prop) → [DecidablePred Q] → Decidable (∀ (x : Fin 5), Q x) := fun Q => inferInstance
  --exact inferInstance -- Fails.
  exact @instDecidableForallVector _ _ _ _ inferInstance -- Fails.
  --exact @instDecidableForallVector _ _ _ _ this -- Succeeds.