"failed to synthesize instance" despite local instance

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
    _