Update

This PR shares common functionality relate to equalities between same
constructors, and when these are type-correct. In particular it uses the
more compelte logic from `mkInjectivityThm` also in other places, such
as `CasesOnSameCtor` and the deriving code for `BEq`, `DecidableEq`,
`Ord`, for more consistency and better error messages.

src/Lean/Elab/Deriving/BEq.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Transform
 public import Lean.Elab.Deriving.Basic
 public import Lean.Elab.Deriving.Util
+import Lean.Meta.SameCtorUtils
 
 public section
 
@@ -44,17 +45,20 @@ where
         -- add `_` pattern for indices
         for _ in *...indVal.numIndices do
           patterns := patterns.push (← `(_))
-        let mut ctorArgs1 := #[]
-        let mut ctorArgs2 := #[]
+        let mut ctorArgs1 : Array Term := #[]
+        let mut ctorArgs2 : Array Term := #[]
         let mut rhs ← `(true)
         let mut rhs_empty := true
         for i in *...ctorInfo.numFields do
           let pos := indVal.numParams + ctorInfo.numFields - i - 1
           let x := xs[pos]!
-          if type.containsFVar x.fvarId! then
+          if occursOrInType (← getLCtx) x type then
             -- If resulting type depends on this field, we don't need to compare
-            ctorArgs1 := ctorArgs1.push (← `(_))
-            ctorArgs2 := ctorArgs2.push (← `(_))
+            -- but use inaccessible patterns fail during pattern match compilation if their
+            -- equality does not actually follow from the equality between their types
+            let a := mkIdent (← mkFreshUserName `a)
+            ctorArgs1 := ctorArgs1.push a
+            ctorArgs2 := ctorArgs2.push (← `(term|.( $a:ident )))
           else
             let a := mkIdent (← mkFreshUserName `a)
             let b := mkIdent (← mkFreshUserName `b)

src/Lean/Elab/Deriving/DecEq.lean

@@ -15,6 +15,7 @@ import Lean.Meta.NatTable
 import Lean.Meta.Constructions.CtorIdx
 import Lean.Meta.Constructions.CtorElim
 import Lean.Meta.Constructions.CasesOnSameCtor
+import Lean.Meta.SameCtorUtils
 
 namespace Lean.Elab.Deriving.DecEq
 open Lean.Parser.Term
@@ -75,10 +76,13 @@ where
             let mut todo := #[]
             for i in *...ctorInfo.numFields do
               let x := xs[indVal.numParams + i]!
-              if type.containsFVar x.fvarId! then
+              if occursOrInType (← getLCtx) x type then
                 -- If resulting type depends on this field, we don't need to compare
-                ctorArgs1 := ctorArgs1.push (← `(_))
-                ctorArgs2 := ctorArgs2.push (← `(_))
+                -- but use inaccessible patterns fail during pattern match compilation if their
+                -- equality does not actually follow from the equality between their types
+                let a := mkIdent (← mkFreshUserName `a)
+                ctorArgs1 := ctorArgs1.push a
+                ctorArgs2 := ctorArgs2.push (← `(term|.( $a:ident )))
               else
                 let a := mkIdent (← mkFreshUserName `a)
                 let b := mkIdent (← mkFreshUserName `b)

src/Lean/Elab/Deriving/Ord.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Transform
 public import Lean.Elab.Deriving.Basic
 public import Lean.Elab.Deriving.Util
+import Lean.Meta.SameCtorUtils
 
 public section
 
@@ -44,10 +45,17 @@ where
           ctorArgs2 := ctorArgs2.push (← `(_))
         for i in *...ctorInfo.numFields do
           let x := xs[indVal.numParams + i]!
-          if type.containsFVar x.fvarId! || (←isProp (←inferType x)) then
+          if (← isProof x) then
             -- If resulting type depends on this field or is a proof, we don't need to compare
             ctorArgs1 := ctorArgs1.push (← `(_))
             ctorArgs2 := ctorArgs2.push (← `(_))
+          else if occursOrInType (← getLCtx) x type then
+            -- If resulting type depends on this field, we don't need to compare
+            -- but use inaccessible patterns fail during pattern match compilation if their
+            -- equality does not actually follow from the equality between their types
+            let a := mkIdent (← mkFreshUserName `a)
+            ctorArgs1 := ctorArgs1.push a
+            ctorArgs2 := ctorArgs2.push (← `(term|.( $a:ident )))
           else
             let a := mkIdent (← mkFreshUserName `a)
             let b := mkIdent (← mkFreshUserName `b)

src/Lean/Meta/Constructions/CasesOnSameCtor.lean

@@ -14,6 +14,7 @@ import Lean.Meta.CompletionName
 import Lean.Meta.Constructions.CtorIdx
 import Lean.Meta.Constructions.CtorElim
 import Lean.Elab.App
+import Lean.Meta.SameCtorUtils
 
 /-!
 See `mkCasesOnSameCtor` below.
@@ -109,23 +110,6 @@ public def mkCasesOnSameCtorHet (declName : Name) (indName : Name) : MetaM Unit
   Elab.Term.elabAsElim.setTag declName
   setReducibleAttribute declName
 
-def withSharedIndices (ctor : Expr) (k : Array Expr → Expr → Expr → MetaM α) : MetaM α := do
-  let ctorType ← inferType ctor
-  forallTelescopeReducing ctorType fun zs ctorRet => do
-    let ctor1 := mkAppN ctor zs
-    let rec go ctor2 todo acc := do
-      match todo with
-      | [] => k acc ctor1 ctor2
-      | z::todo' =>
-        if ctorRet.containsFVar z.fvarId! then
-          go (mkApp ctor2 z) todo' acc
-        else
-          let t ← whnfForall (← inferType ctor2)
-          assert! t.isForall
-          withLocalDeclD t.bindingName! t.bindingDomain! fun z' => do
-            go (mkApp ctor2 z') todo' (acc.push z')
-    go ctor zs.toList zs
-
 /--
 This constructs a matcher for a match statement that matches on the constructors of
 a data type in parallel. So if `h : x1.ctorIdx = x2.ctorIdx`, then it implements
@@ -173,9 +157,9 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit :=
 
       let altTypes ← info.ctors.toArray.mapIdxM fun i ctorName => do
         let ctor := mkAppN (mkConst ctorName us) params
-        withSharedIndices ctor fun zs12 ctorApp1 ctorApp2 => do
-          let ctorRet1 ← whnf (← inferType ctorApp1)
-          let is : Array Expr := ctorRet1.getAppArgs[info.numParams:]
+        withSharedCtorIndices ctor fun zs12 is fields1 fields2 => do
+          let ctorApp1 := mkAppN ctor fields1
+          let ctorApp2 := mkAppN ctor fields2
           let e := mkAppN motive (is ++ #[ctorApp1, ctorApp2, (← mkEqRefl (mkNatLit i))])
           let e ← mkForallFVars zs12 e
           let name := match ctorName with

src/Lean/Meta/Injective.lean

@@ -6,14 +6,16 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.Transform
-public import Lean.Meta.Tactic.Injection
-public import Lean.Meta.Tactic.Apply
-public import Lean.Meta.Tactic.Refl
-public import Lean.Meta.Tactic.Cases
-public import Lean.Meta.Tactic.Subst
-public import Lean.Meta.Tactic.Assumption
+public import Lean.Meta.Basic
+import Lean.Meta.Transform
+import Lean.Meta.Tactic.Injection
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Refl
+import Lean.Meta.Tactic.Cases
+import Lean.Meta.Tactic.Subst
+import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Simp.Main
+import Lean.Meta.SameCtorUtils
 
 public section
 
@@ -35,35 +37,6 @@ def elimOptParam (type : Expr) : CoreM Expr := do
     else
       return .continue
 
-
-/-- Returns true if `e` occurs either in `t`, or in the type of a sub-expression of `t`.
-  Consider the following example:
-  ```lean
-  inductive Tyₛ : Type (u+1)
-  | SPi : (T : Type u) -> (T -> Tyₛ) -> Tyₛ
-
-  inductive Tmₛ.{u} :  Tyₛ.{u} -> Type (u+1)
-  | app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)```
-  ```
-  When looking for fixed arguments in `Tmₛ.app`, if we only consider occurrences in the term `Tmₛ (A arg)`,
-  `T` is considered non-fixed despite the fact that `A : T -> Tyₛ`.
-  This leads to an ill-typed injectivity theorem signature:
-  ```lean
-  theorem Tmₛ.app.inj {T : Type u} {A : T → Tyₛ} {a : Tmₛ (Tyₛ.SPi T A)} {arg : T} {T_1 : Type u} {a_1 : Tmₛ (Tyₛ.SPi T_1 A)} :
-  Tmₛ.app a arg = Tmₛ.app a_1 arg →
-    T = T_1 ∧ a ≍ a_1 := fun x => Tmₛ.noConfusion x fun T_eq A_eq a_eq arg_eq => eq_of_heq a_eq
-  ```
-  Instead of checking the type of every subterm, we only need to check the type of free variables, since free variables introduced in
-  the constructor may only appear in the type of other free variables introduced after them.
--/
-def occursOrInType (lctx : LocalContext) (e : Expr) (t : Expr) : Bool :=
-  t.find? go |>.isSome
-where
-  go s := Id.run do
-    let .fvar fvarId := s | s == e
-    let some decl := lctx.find? fvarId | s == e
-    return s == e || e.occurs decl.type
-
 private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
   let us := ctorVal.levelParams.map mkLevelParam
   let type ← elimOptParam ctorVal.type

src/Lean/Meta/SameCtorUtils.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+module
+prelude
+public import Lean.Meta.Basic
+import Lean.Meta.Transform
+
+/-!
+This module contains utilities for dealing with equalities between constructor applications,
+in particular about which fields must be the same a-priori for the equality to type check.
+
+Users include (or will include) the injectivity theorems, the per-constructor no-confusion
+construction and deriving type classes lik `BEq`, `DecidableEq` or `Ord`.
+-/
+
+namespace Lean.Meta
+
+/--
+Returns true if `e` occurs either in `t`, or in the type of a sub-expression of `t`.
+
+Consider the following example:
+```lean
+inductive Tyₛ : Type (u+1)
+| SPi : (T : Type u) -> (T -> Tyₛ) -> Tyₛ
+
+inductive Tmₛ.{u} :  Tyₛ.{u} -> Type (u+1)
+| app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)```
+```
+When looking for fixed arguments in `Tmₛ.app`, if we only consider occurrences in the term `Tmₛ (A arg)`,
+`T` is considered non-fixed despite the fact that `A : T -> Tyₛ`.
+This leads to an ill-typed injectivity theorem signature:
+```lean
+theorem Tmₛ.app.inj {T : Type u} {A : T → Tyₛ} {a : Tmₛ (Tyₛ.SPi T A)} {arg : T} {T_1 : Type u} {a_1 : Tmₛ (Tyₛ.SPi T_1 A)} :
+Tmₛ.app a arg = Tmₛ.app a_1 arg →
+  T = T_1 ∧ a ≍ a_1 := fun x => Tmₛ.noConfusion x fun T_eq A_eq a_eq arg_eq => eq_of_heq a_eq
+```
+Instead of checking the type of every subterm, we only need to check the type of free variables, since free variables introduced in
+the constructor may only appear in the type of other free variables introduced after them.
+-/
+public def occursOrInType (lctx : LocalContext) (e : Expr) (t : Expr) : Bool :=
+  t.find? go |>.isSome
+where
+  go s := Id.run do
+    let .fvar fvarId := s | s == e
+    let some decl := lctx.find? fvarId | s == e
+    return s == e || e.occurs decl.type
+
+/--
+Given a constructor, returns a mask of its fields, where `true` means that this field
+occurs in the result type of the constructor.
+-/
+public def occursInCtorTypeMask (ctorName : Name) : MetaM (Array Bool) := do
+  let ctorInfo ← getConstInfoCtor ctorName
+  forallBoundedTelescope ctorInfo.type (some ctorInfo.numParams) fun _ ctorRet => do
+    forallBoundedTelescope ctorRet (some ctorInfo.numFields) fun ys ctorRet => do
+      let ctorRet ← whnf ctorRet
+      let ctorRet ← Core.betaReduce ctorRet -- we 'beta-reduce' to eliminate "artificial" dependencies
+      let lctx ← getLCtx
+      return ys.map (occursOrInType lctx · ctorRet)
+
+/--
+Given a constructor (applied to the parameters already), brings its fields into scope twice,
+but uses the same variable for fields that appear in the result type, so that the resulting
+constructor applications have the same type.
+
+Passes to `k`
+* the new variables
+* the indices to the type class
+* the fields of the first constructor application
+* the fields of the second constructor application
+-/
+public def withSharedCtorIndices (ctor : Expr)
+    (k : Array Expr → Array Expr → Array Expr → Array Expr → MetaM α) : MetaM α := do
+  let ctorType ← inferType ctor
+  forallTelescopeReducing ctorType fun zs ctorRet => do
+    let ctorRet ← whnf ctorRet
+    let ctorRet ← Core.betaReduce ctorRet -- we 'beta-reduce' to eliminate "artificial" dependencies
+    let indInfo ← getConstInfoInduct ctorRet.getAppFn.constName!
+    let indices := ctorRet.getAppArgsN indInfo.numIndices
+
+    let rec go zs2 mask todo acc := do
+      match mask, todo with
+      | true::mask', z::todo' =>
+        go (zs2.push z) mask' todo' acc
+      | false::mask', _::todo' =>
+        let t ← whnfForall (← inferType (mkAppN ctor zs2))
+        assert! t.isForall
+        withLocalDeclD (t.bindingName!.appendAfter "'") t.bindingDomain! fun z' => do
+          go (zs2.push z') mask' todo' (acc.push z')
+      | _, _ =>
+        k acc indices zs zs2
+
+    let mask ← occursInCtorTypeMask ctor.getAppFn.constName!
+    go #[] mask.toList zs.toList zs

src/Lean/Util/Recognizers.lean

@@ -68,6 +68,7 @@ namespace Expr
 @[inline] def and? (p : Expr) : Option (Expr × Expr) :=
   p.app2? ``And
 
+/-- Recognizes `x1 ≍ x2`, returns `some (α1, x1, α2, x2)`.  -/
 @[inline] def heq? (p : Expr) : Option (Expr × Expr × Expr × Expr) :=
   p.app4? ``HEq
 

tests/lean/run/3386.lean

@@ -5,5 +5,20 @@
 inductive Tyₛ : Type (u+1)
 | SPi : (T : Type u) -> (T -> Tyₛ) -> Tyₛ
 
+set_option deriving.decEq.linear_construction_threshold 0
 inductive Tmₛ.{u} :  Tyₛ.{u} -> Type (u+1)
 | app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)
+
+/--
+info: Tmₛ.app.injEq.{u} {T : Type u} {A : T → Tyₛ} (a✝ : Tmₛ (Tyₛ.SPi T A)) (arg : T) (a✝¹ : Tmₛ (Tyₛ.SPi T A)) :
+  (a✝.app arg = a✝¹.app arg) = (a✝ = a✝¹)
+-/
+#guard_msgs in
+#check Tmₛ.app.injEq
+
+/--
+info: Tmₛ.app.inj.{u} {T : Type u} {A : T → Tyₛ} {a✝ : Tmₛ (Tyₛ.SPi T A)} {arg : T} {a✝¹ : Tmₛ (Tyₛ.SPi T A)} :
+  a✝.app arg = a✝¹.app arg → a✝ = a✝¹
+-/
+#guard_msgs in
+#check Tmₛ.app.inj

tests/lean/run/casesOnSameCtor.lean

@@ -28,7 +28,7 @@ info: Vec.match_on_same_ctor.het.{u_1, u} {α : Type u} {motive : {a : Nat} →
 info: Vec.match_on_same_ctor.{u_1, u} {α : Type u}
   {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} {a✝ : Nat} (t t✝ : Vec α a✝)
   (h : t.ctorIdx = t✝.ctorIdx) (nil : motive nil nil ⋯)
-  (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a_2 : α) → (a_3 : Vec α n) → motive (cons a a_1) (cons a_2 a_3) ⋯) :
+  (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
   motive t t✝ h
 -/
 #guard_msgs in
@@ -39,7 +39,7 @@ info: Vec.match_on_same_ctor.{u_1, u} {α : Type u}
 info: Vec.match_on_same_ctor.splitter.{u_1, u} {α : Type u}
   {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} {a✝ : Nat} (t t✝ : Vec α a✝)
   (h : t.ctorIdx = t✝.ctorIdx) (h_1 : motive nil nil ⋯)
-  (h_2 : (a : α) → (n : Nat) → (a_1 : Vec α n) → (a_2 : α) → (a_3 : Vec α n) → motive (cons a a_1) (cons a_2 a_3) ⋯) :
+  (h_2 : (a : α) → (n : Nat) → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
   motive t t✝ h
 -/
 #guard_msgs in
@@ -52,12 +52,12 @@ example : @Vec.match_on_same_ctor = @Vec.match_on_same_ctor.splitter := by rfl
 /--
 info: Vec.match_on_same_ctor.eq_2.{u_1, u} {α : Type u}
   {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} (a✝ : α) (n : Nat) (a✝¹ : Vec α n)
-  (a✝² : α) (a✝³ : Vec α n) (nil : motive nil nil ⋯)
-  (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a_2 : α) → (a_3 : Vec α n) → motive (cons a a_1) (cons a_2 a_3) ⋯) :
-  (match n + 1, Vec.cons a✝ a✝¹, Vec.cons a✝² a✝³ with
+  (a'✝ : α) (a'✝¹ : Vec α n) (nil : motive nil nil ⋯)
+  (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
+  (match n + 1, Vec.cons a✝ a✝¹, Vec.cons a'✝ a'✝¹ with
     | 0, Vec.nil, Vec.nil, ⋯ => nil
-    | n + 1, Vec.cons a a_1, Vec.cons a_2 a_3, ⋯ => cons a a_1 a_2 a_3) =
-    cons a✝ a✝¹ a✝² a✝³
+    | n + 1, Vec.cons a a_1, Vec.cons a' a'_1, ⋯ => cons a a_1 a' a'_1) =
+    cons a✝ a✝¹ a'✝ a'✝¹
 -/
 #guard_msgs in
 #check Vec.match_on_same_ctor.eq_2
@@ -136,8 +136,7 @@ run_meta mkCasesOnSameCtor `List.match_on_same_ctor ``List
 /--
 info: List.match_on_same_ctor.{u_1, u} {α : Type u} {motive : (t t_1 : List α) → t.ctorIdx = t_1.ctorIdx → Sort u_1}
   (t t✝ : List α) (h : t.ctorIdx = t✝.ctorIdx) (nil : motive [] [] ⋯)
-  (cons :
-    (head : α) → (tail : List α) → (head_1 : α) → (tail_1 : List α) → motive (head :: tail) (head_1 :: tail_1) ⋯) :
+  (cons : (head : α) → (tail : List α) → (head' : α) → (tail' : List α) → motive (head :: tail) (head' :: tail') ⋯) :
   motive t t✝ h
 -/
 #guard_msgs in

tests/lean/run/derivingBEq.lean

@@ -69,6 +69,27 @@ def ex1 [BEq α] : BEq (Tree α) :=
 def ex2 [BEq α] : BEq (TreeList α) :=
   inferInstance
 
+-- The tricky inductive from issue #3386
+
+inductive Tyₛ : Type (u+1)
+| SPi : (T : Type u) -> (T -> Tyₛ) -> Tyₛ
+
+/--
+error: Tactic `cases` failed with a nested error:
+Dependent elimination failed: Failed to solve equation
+  A✝¹ arg✝¹ = A✝ arg✝
+at case `Tmₛ.app` after processing
+  _, (Tmₛ.app _ _ _ _), _
+the dependent pattern matcher can solve the following kinds of equations
+- <var> = <term> and <term> = <var>
+- <term> = <term> where the terms are definitionally equal
+- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
+-/
+#guard_msgs(pass trace, all) in
+inductive Tmₛ.{u} :  Tyₛ.{u} -> Type (u+1)
+| app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)
+deriving BEq
+
 /-! Private fields should yield public, no-expose instances. -/
 
 structure PrivField where

tests/lean/run/derivingDecidableEq.lean

@@ -56,6 +56,29 @@ def ex1 [DecidableEq α] : DecidableEq (Tree α) :=
 def ex2 [DecidableEq α] : DecidableEq (TreeList α) :=
   inferInstance
 
+-- The tricky inductive from issue #3386
+
+inductive Tyₛ : Type (u+1)
+| SPi : (T : Type u) -> (T -> Tyₛ) -> Tyₛ
+
+/--
+error: Tactic `cases` failed with a nested error:
+Dependent elimination failed: Failed to solve equation
+  A✝¹ arg✝¹ = A✝ arg✝
+at case `Tmₛ.app` after processing
+  _, (Tmₛ.app _ _ _ _), _
+the dependent pattern matcher can solve the following kinds of equations
+- <var> = <term> and <term> = <var>
+- <term> = <term> where the terms are definitionally equal
+- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
+---
+warning: unused `termination_by`, function is not recursive
+-/
+#guard_msgs(pass trace, all) in
+inductive Tmₛ.{u} :  Tyₛ.{u} -> Type (u+1)
+| app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)
+deriving DecidableEq
+
 /-! Private fields should yield public, no-expose instances. -/
 
 structure PrivField where

tests/lean/run/derivingDecidableEqLinear.lean

@@ -56,6 +56,20 @@ def ex1 [DecidableEq α] : DecidableEq (Tree α) :=
 def ex2 [DecidableEq α] : DecidableEq (TreeList α) :=
   inferInstance
 
+
+inductive Tyₛ : Type (u+1)
+| SPi : (T : Type u) -> (T -> Tyₛ) -> Tyₛ
+
+/--
+error: Dependent elimination failed: Failed to solve equation
+  A✝ arg✝ = A arg
+-/
+#guard_msgs in
+inductive Tmₛ.{u} :  Tyₛ.{u} -> Type (u+1)
+| app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)
+deriving DecidableEq
+
+
 /-! Private fields should yield public, no-expose instances. -/
 
 structure PrivField where