fix: we should not use implicit targets when creating the key for the CustomEliminator map

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -111,11 +111,23 @@ def mkCustomEliminator (declName : Name) : MetaM CustomEliminator := do
   let elimInfo ← getElimInfo declName
   forallTelescopeReducing info.type fun xs _ => do
     let mut typeNames := #[]
-    for targetPos in elimInfo.targetsPos do
+    for i in [:elimInfo.targetsPos.size] do
+      let targetPos := elimInfo.targetsPos[i]
       let x := xs[targetPos]
-      let xType ← inferType x
-      let .const typeName .. := xType.getAppFn | throwError "unexpected eliminator target type{indentExpr xType}"
-      typeNames := typeNames.push typeName
+      /- Return true if there is another target that depends on `x`. -/
+      let isImplicitTarget : MetaM Bool := do
+        for j in [i+1:elimInfo.targetsPos.size] do
+          let y := xs[elimInfo.targetsPos[j]]
+          let yType ← inferType y
+          if (← dependsOn yType x.fvarId!) then
+            return true
+        return false
+      /- We should only use explicit targets when creating the key for the `CustomEliminators` map.
+         See test `tests/lean/run/eliminatorImplicitTargets.lean`. -/
+      unless (← isImplicitTarget) do
+        let xType ← inferType x
+        let .const typeName .. := xType.getAppFn | throwError "unexpected eliminator target type{indentExpr xType}"
+        typeNames := typeNames.push typeName
     return { typeNames, elimInfo }
 
 def addCustomEliminator (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do

tests/lean/run/eliminatorImplicitTargets.lean

@@ -0,0 +1,13 @@
+inductive Equality {α : Type u} : α → α → Type u
+| refl {a : α} : Equality a a
+
+open Equality
+
+@[eliminator]
+def ind {α : Type u} (motive : ∀ (a b : α) (p : Equality a b), Sort v)
+  {a : α} (πrefl : motive a a refl) {b : α} (p : Equality a b) : motive a b p :=
+@Equality.casesOn α a (λ b p => motive a a refl → motive a b p) b p
+  (λ (ε : motive a a refl) => ε) πrefl
+
+def symm {α : Type u} {a b : α} (p : Equality a b) : Equality b a :=
+by { induction p; apply refl }