feat: linear-size BEq instance (#10268)

This PR adds an alternative implementation of `DerivingBEq` based on
comparing `.ctorIdx` and using a dedicated matcher for comparing same
constructors (added in #10152), to avoid the quadratic overhead of the
default match implementation. The new option
`deriving.beq.linear_construction_threshold` sets the constructor count
threshold (10 by default) for using the new construction. Such instances
also allow `deriving ReflBEq, LawfulBeq`, although these proofs for
these properties are still quadratic.

src/Init/LawfulBEqTactics.lean

@@ -21,7 +21,7 @@ macro "deriving_ReflEq_tactic" : tactic => `(tactic|(
   intro x
   induction x
   all_goals
-    simp only [ BEq.refl, ↓reduceDIte, Bool.and_true, *, reduceBEq ]
+    simp only [ BEq.refl, ↓reduceDIte, Bool.and_true, *, reduceBEq ,reduceCtorIdx]
 ))
 
 theorem and_true_curry {a b : Bool} {P : Prop}
@@ -99,6 +99,6 @@ macro "deriving_LawfulEq_tactic" : tactic => `(tactic|(
     intro y
     cases y
     all_goals
-      simp only [reduceBEq]
+      simp only [reduceBEq, reduceCtorIdx]
       repeat deriving_LawfulEq_tactic_step
 ))

src/Lean/Elab/Deriving/BEq.lean

@@ -10,17 +10,27 @@ public import Lean.Data.Options
 import Lean.Meta.Transform
 import Lean.Elab.Deriving.Basic
 import Lean.Elab.Deriving.Util
-import Lean.Meta.Eqns
+import Lean.Meta.Constructions.CtorIdx
+import Lean.Meta.Constructions.CasesOnSameCtor
 import Lean.Meta.SameCtorUtils
 
 namespace Lean.Elab.Deriving.BEq
 open Lean.Parser.Term
 open Meta
 
+
+register_builtin_option deriving.beq.linear_construction_threshold : Nat := {
+  defValue := 10
+  descr := "If the inductive data type has this many or more constructors, use a different \
+    implementation for implementing `BEq` that avoids the quadratic code size produced by the \
+    default implementation.\n\n\
+    The alternative construction compiles to less efficient code in some cases, so by default \
+    it is only used for inductive types with 10 or more constructors." }
+
 def mkBEqHeader (indVal : InductiveVal) : TermElabM Header := do
   mkHeader `BEq 2 indVal
 
-def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do
+def mkMatchOld (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do
   let discrs ← mkDiscrs header indVal
   let alts ← mkAlts
   `(match $[$discrs],* with $alts:matchAlt*)
@@ -99,6 +109,77 @@ where
     alts := alts.push (← mkElseAlt)
     return alts
 
+def mkMatchNew (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do
+  assert! header.targetNames.size == 2
+
+  let x1 := mkIdent header.targetNames[0]!
+  let x2 := mkIdent header.targetNames[1]!
+  let ctorIdxName := mkCtorIdxName indVal.name
+  -- NB: the getMatcherInfo? assumes all matchers are called `match_`
+  let casesOnSameCtorName ← mkFreshUserName (indVal.name ++ `match_on_same_ctor)
+  mkCasesOnSameCtor casesOnSameCtorName indVal.name
+  let alts ← Array.ofFnM (n := indVal.numCtors) fun ⟨ctorIdx, _⟩ => do
+    let ctorName := indVal.ctors[ctorIdx]!
+    let ctorInfo ← getConstInfoCtor ctorName
+    forallTelescopeReducing ctorInfo.type fun xs type => do
+      let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
+      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 resulting type depends on this field, we don't need to compare
+          -- and the casesOnSameCtor only has a parameter for it once
+          ctorArgs1 := ctorArgs1.push (← `(_))
+        else
+          let userName ← x.fvarId!.getUserName
+          let a := mkIdent (← mkFreshUserName userName)
+          let b := mkIdent (← mkFreshUserName (userName.appendAfter "'"))
+          ctorArgs1 := ctorArgs1.push a
+          ctorArgs2 := ctorArgs2.push b
+          let xType ← inferType x
+          if (← isProp xType) then
+            continue
+          if xType.isAppOf indVal.name then
+            if rhs_empty then
+              rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident)
+              rhs_empty := false
+            else
+              rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident && $rhs)
+          /- If `x` appears in the type of another field, use `eq_of_beq` to
+              unify the types of the subsequent variables -/
+          else if ← xs[(pos+1)...*].anyM
+              (fun fvar => (Expr.containsFVar · x.fvarId!) <$> (inferType fvar)) then
+            rhs ← `(if h : $a:ident == $b:ident then by
+                      cases (eq_of_beq h)
+                      exact $rhs
+                    else false)
+            rhs_empty := false
+          else
+            if rhs_empty then
+              rhs ← `($a:ident == $b:ident)
+              rhs_empty := false
+            else
+              rhs ← `($a:ident == $b:ident && $rhs)
+      `(@fun $ctorArgs1.reverse:term* $ctorArgs2.reverse:term* =>$rhs:term)
+  if indVal.numCtors == 1 then
+    `( $(mkCIdent casesOnSameCtorName) $x1:term $x2:term rfl $alts:term* )
+  else
+    `( match decEq ($(mkCIdent ctorIdxName) $x1:ident) ($(mkCIdent ctorIdxName) $x2:ident) with
+      | .isTrue h => $(mkCIdent casesOnSameCtorName) $x1:term $x2:term h $alts:term*
+      | .isFalse _ => false)
+
+def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do
+  if indVal.numCtors ≥ deriving.beq.linear_construction_threshold.get (← getOptions) then
+    mkMatchNew header indVal auxFunName
+  else
+    mkMatchOld header indVal auxFunName
+
+
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
   let auxFunName := ctx.auxFunNames[i]!
   let indVal     := ctx.typeInfos[i]!

src/Lean/Elab/Deriving/DecEq.lean

@@ -13,7 +13,6 @@ import Lean.Elab.Deriving.Basic
 import Lean.Elab.Deriving.Util
 import Lean.Meta.NatTable
 import Lean.Meta.Constructions.CtorIdx
-import Lean.Meta.Constructions.CtorElim
 import Lean.Meta.Constructions.CasesOnSameCtor
 import Lean.Meta.SameCtorUtils
 

src/Lean/Meta/Constructions/CasesOnSameCtor.lean

@@ -220,13 +220,6 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit :=
         Match.addMatcherInfo declName matcherInfo
         setInlineAttribute declName
 
-        -- Pragmatic hack:
-        -- Normally a matcher is not marked as an aux recursor. We still do that here
-        -- because this makes the elaborator unfold it more eagerily, it seems,
-        -- and this works around issues with the structural recursion equation generator
-        -- (see #10195).
-        modifyEnv fun env => markAuxRecursor env declName
-
         enableRealizationsForConst declName
         compileDecl decl
 

src/Lean/Meta/MethodSpecs.lean

@@ -163,7 +163,8 @@ def rewriteThm (ctx : Simp.Context) (simprocs : Simprocs)
   let thmInfo ← getConstVal eqThmName
   let (result, _) ← simp thmInfo.type ctx (simprocs := #[simprocs])
   trace[Meta.MethodSpecs] "type for {destThmName}:{indentExpr result.expr}"
-  let value ← result.mkEqMPR <| mkConst eqThmName (thmInfo.levelParams.map mkLevelParam)
+  let eqThmApp := mkConst eqThmName (thmInfo.levelParams.map mkLevelParam)
+  let value := mkAppN (mkConst ``Eq.mp [0]) #[thmInfo.type, result.expr, ← result.getProof, eqThmApp]
   addDecl <| Declaration.thmDecl {
     name          := destThmName
     levelParams   := thmInfo.levelParams
@@ -186,7 +187,7 @@ where
       let ctx ← Simp.mkContext
         (simpTheorems  := #[s])
         (congrTheorems := (← getSimpCongrTheorems))
-        (config        := { } ) -- Simp.neutralConfig with dsimp := true, letToHave := false })
+        (config        := { } )
       let simprocs ← Simp.getSimprocs
 
       let env ← getEnv

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -559,6 +559,13 @@ def Result.mkEqMPR (r : Simp.Result) (e : Expr) : MetaM Expr := do
   else
     Meta.mkEqMPR (← r.getProof) e
 
+/-- Construct the `Expr` `h.mp e`, from a `Simp.Result` with proof `h`. -/
+def Result.mkEqMP (r : Simp.Result) (e : Expr) : MetaM Expr := do
+  if r.proof?.isNone && r.expr == e then
+    pure e
+  else
+    Meta.mkEqMP (← r.getProof) e
+
 def mkCongrFun (r : Result) (a : Expr) : MetaM Result :=
   match r.proof? with
   | none   => return { expr := mkApp r.expr a, proof? := none }

tests/lean/run/decEqNonInjIndex.lean

@@ -6,18 +6,9 @@ non-injective indices, and just how bad the error messages are.
 opaque f : Nat → Nat
 
 set_option deriving.decEq.linear_construction_threshold 0
+set_option deriving.beq.linear_construction_threshold 0
 
 /--
-error: Tactic `cases` failed with a nested error:
-Dependent elimination failed: Failed to solve equation
-  f n✝¹ = f n✝
-at case `T.mk1` after processing
-  _, (T.mk1 _ _), _
-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
----
 error: Dependent elimination failed: Failed to solve equation
   f n✝ = f n
 -/
@@ -29,6 +20,7 @@ deriving BEq, DecidableEq
 
 
 set_option deriving.decEq.linear_construction_threshold 10000
+set_option deriving.beq.linear_construction_threshold 10000
 
 /--
 error: Tactic `cases` failed with a nested error:

tests/lean/run/derivingBEq.lean

@@ -1,11 +1,17 @@
 module
 
+set_option deriving.beq.linear_construction_threshold 1000
+
 public section
 
 inductive Foo
   | mk1 | mk2 | mk3
   deriving @[expose] BEq
 
+/-- info: instBEqFoo.beq_spec (x✝ y✝ : Foo) : (x✝ == y✝) = (x✝.ctorIdx == y✝.ctorIdx) -/
+#guard_msgs in
+#check instBEqFoo.beq_spec
+
 namespace Foo
 theorem ex1 : (mk1 == mk2) = false :=
   rfl
@@ -19,17 +25,68 @@ theorem ex5 : (mk2 == mk3) = false :=
   rfl
 end Foo
 
+inductive L (α : Type u) : Type u
+  | nil  : L α
+  | cons : α → L α → L α
+  deriving @[expose] BEq
+
+/--
+info: instBEqL.beq_spec.{u_1} {α✝ : Type u_1} [BEq α✝] (x✝ x✝¹ : L α✝) :
+  (x✝ == x✝¹) =
+    match x✝, x✝¹ with
+    | L.nil, L.nil => true
+    | L.cons a a_1, L.cons b b_1 => a == b && a_1 == b_1
+    | x, x_1 => false
+-/
+#guard_msgs in
+#check instBEqL.beq_spec
+
+namespace L
+theorem ex1 : (L.cons 10 L.nil == L.cons 20 L.nil) = false := rfl
+theorem ex2 : (L.cons 10 L.nil == L.nil) = false := rfl
+end L
+
+namespace InNamespace
+inductive L' (α : Type u) : Type u
+  | nil  : L' α
+  | cons : α → L' α → L' α
+  deriving @[expose] BEq
+
+end InNamespace
+/--
+info: @[expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α)
+-/
+#guard_msgs in #print sig InNamespace.instBEqL'
+/--
+info: theorem InNamespace.instBEqL'.beq_spec.{u_1} : ∀ {α : Type u_1} [inst : BEq α] (x x_1 : InNamespace.L' α),
+  (x == x_1) =
+    match x, x_1 with
+    | InNamespace.L'.nil, InNamespace.L'.nil => true
+    | InNamespace.L'.cons a a_1, InNamespace.L'.cons b b_1 => a == b && a_1 == b_1
+    | x, x_2 => false
+-/
+#guard_msgs in #print sig InNamespace.instBEqL'.beq_spec
+
 inductive Vec (α : Type u) : Nat → Type u
   | nil  : Vec α 0
   | cons : α → {n : Nat} → Vec α n → Vec α (n+1)
   deriving @[expose] BEq
 
-namespace Vec
-theorem ex1 : (cons 10 Vec.nil == cons 20 Vec.nil) = false :=
-  rfl
+/--
+info: instBEqVec.beq_spec.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] (x✝ x✝¹ : Vec α✝ a✝) :
+  (x✝ == x✝¹) =
+    match a✝, x✝, x✝¹ with
+    | .(0), Vec.nil, Vec.nil => true
+    | .(a_1 + 1), Vec.cons a a_2, Vec.cons b b_1 => a == b && a_2 == b_1
+    | x, x_1, x_2 => false
+-/
+#guard_msgs in
+#check instBEqVec.beq_spec
 
-theorem ex2 : (cons 10 Vec.nil == cons 10 Vec.nil) = true :=
-  rfl
+namespace Vec
+theorem ex1 : (cons 10 Vec.nil == cons 20 Vec.nil) = false := rfl
+
+theorem ex2 : (cons 10 Vec.nil == cons 10 Vec.nil) = true := rfl
 
 theorem ex3 : (cons 20 (cons 11 Vec.nil) == cons 20 (cons 10 Vec.nil)) = false :=
   rfl
@@ -101,6 +158,24 @@ deriving BEq
 #with_exporting
 #reduce fun (a : PrivField) => a == a
 
+private structure PrivStruct where
+  a : Nat
+deriving BEq
+
+-- Instance and spec should be private
+/-- info: private def instBEqPrivStruct : BEq PrivStruct -/
+#guard_msgs in
+#print sig instBEqPrivStruct
+
+/-- info: private def instBEqPrivStruct.beq : PrivStruct → PrivStruct → Bool -/
+#guard_msgs in
+#print sig instBEqPrivStruct.beq
+/--
+info: private theorem instBEqPrivStruct.beq_spec : ∀ (x x_1 : PrivStruct), (x == x_1) = (x.a == x_1.a)
+-/
+#guard_msgs in
+#print sig instBEqPrivStruct.beq_spec
+
 end
 
 -- Try again without `public section`

tests/lean/run/derivingBEqLinear.lean

@@ -0,0 +1,177 @@
+module
+
+set_option deriving.beq.linear_construction_threshold 0
+
+public section
+
+inductive Foo
+  | mk1 | mk2 | mk3
+  deriving @[expose] BEq
+
+/-- info: instBEqFoo.beq_spec (x✝ y✝ : Foo) : (x✝ == y✝) = (x✝.ctorIdx == y✝.ctorIdx) -/
+#guard_msgs in
+#check instBEqFoo.beq_spec
+
+namespace Foo
+theorem ex1 : (mk1 == mk2) = false :=
+  rfl
+theorem ex2 : (mk1 == mk1) = true :=
+  rfl
+theorem ex3 : (mk2 == mk2) = true :=
+  rfl
+theorem ex4 : (mk3 == mk3) = true :=
+  rfl
+theorem ex5 : (mk2 == mk3) = false :=
+  rfl
+end Foo
+
+inductive L (α : Type u) : Type u
+  | nil  : L α
+  | cons : α → L α → L α
+  deriving @[expose] BEq
+
+/--
+info: instBEqL.beq_spec.{u_1} {α✝ : Type u_1} [BEq α✝] (x✝ x✝¹ : L α✝) :
+  (x✝ == x✝¹) =
+    match decEq x✝.ctorIdx x✝¹.ctorIdx with
+    | isTrue h =>
+      match x✝, x✝¹, h with
+      | L.nil, L.nil, ⋯ => true
+      | L.cons a a_1, L.cons a' a'_1, ⋯ => a == a' && a_1 == a'_1
+    | isFalse h => false
+-/
+#guard_msgs in #check instBEqL.beq_spec
+
+/-- error: Unknown identifier `instBEqL.beq_spec_2` -/
+#guard_msgs in #check instBEqL.beq_spec_2
+
+namespace L
+theorem ex1 : (L.cons 10 L.nil == L.cons 20 L.nil) = false := rfl
+theorem ex2 : (L.cons 10 L.nil == L.nil) = false := rfl
+end L
+
+namespace InNamespace
+inductive L' (α : Type u) : Type u
+  | nil  : L' α
+  | cons : α → L' α → L' α
+  deriving @[expose] BEq
+
+end InNamespace
+/--
+info: @[expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α)
+-/
+#guard_msgs in #print sig InNamespace.instBEqL'
+/--
+info: theorem InNamespace.instBEqL'.beq_spec.{u_1} : ∀ {α : Type u_1} [inst : BEq α] (x x_1 : InNamespace.L' α),
+  (x == x_1) =
+    match decEq x.ctorIdx x_1.ctorIdx with
+    | isTrue h =>
+      match x, x_1, h with
+      | InNamespace.L'.nil, InNamespace.L'.nil, ⋯ => true
+      | InNamespace.L'.cons a a_1, InNamespace.L'.cons a' a'_1, ⋯ => a == a' && a_1 == a'_1
+    | isFalse h => false
+-/
+#guard_msgs in #print sig InNamespace.instBEqL'.beq_spec
+
+inductive Vec (α : Type u) : Nat → Type u
+  | nil  : Vec α 0
+  | cons : α → {n : Nat} → Vec α n → Vec α (n+1)
+  deriving @[expose] BEq
+
+/--
+info: instBEqVec.beq_spec.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] (x✝ x✝¹ : Vec α✝ a✝) :
+  (x✝ == x✝¹) =
+    match decEq x✝.ctorIdx x✝¹.ctorIdx with
+    | isTrue h =>
+      match a✝, x✝, x✝¹ with
+      | 0, Vec.nil, Vec.nil, ⋯ => true
+      | x + 1, Vec.cons a a_1, Vec.cons a' a'_1, ⋯ => a == a' && a_1 == a'_1
+    | isFalse h => false
+-/
+#guard_msgs in
+#check instBEqVec.beq_spec
+
+namespace Vec
+theorem ex1 : (cons 10 Vec.nil == cons 20 Vec.nil) = false := rfl
+
+theorem ex2 : (cons 10 Vec.nil == cons 10 Vec.nil) = true := rfl
+
+theorem ex3 : (cons 20 (cons 11 Vec.nil) == cons 20 (cons 10 Vec.nil)) = false :=
+  rfl
+
+theorem ex4 : (cons 20 (cons 11 Vec.nil) == cons 20 (cons 11 Vec.nil)) = true :=
+  rfl
+end Vec
+
+inductive Bla (α : Type u) where
+  | node : List (Bla α) → Bla α
+  | leaf : α → Bla α
+  deriving BEq
+
+namespace Bla
+
+#guard node [] != leaf 10
+#guard node [leaf 10] == node [leaf 10]
+#guard node [leaf 10] != node [leaf 10, leaf 20]
+
+end Bla
+
+mutual
+inductive Tree (α : Type u) where
+  | node : TreeList α → Tree α
+  | leaf : α → Tree α
+  deriving BEq
+
+inductive TreeList (α : Type u) where
+  | nil : TreeList α
+  | cons : Tree α → TreeList α → TreeList α
+  deriving BEq
+end
+
+def ex1 [BEq α] : BEq (Tree α) :=
+  inferInstance
+
+def ex2 [BEq α] : BEq (TreeList α) :=
+  inferInstance
+
+/-! Private fields should yield public, no-expose instances. -/
+
+structure PrivField where
+  private a : Nat
+deriving BEq
+
+/-- info: fun a => instBEqPrivField.beq a a -/
+#guard_msgs in
+#with_exporting
+#reduce fun (a : PrivField) => a == a
+
+private structure PrivStruct where
+  a : Nat
+deriving BEq
+
+-- Instance and spec should be private
+/-- info: private def instBEqPrivStruct : BEq PrivStruct -/
+#guard_msgs in
+#print sig instBEqPrivStruct
+
+/-- info: private def instBEqPrivStruct.beq : PrivStruct → PrivStruct → Bool -/
+#guard_msgs in
+#print sig instBEqPrivStruct.beq
+/--
+info: private theorem instBEqPrivStruct.beq_spec : ∀ (x x_1 : PrivStruct), (x == x_1) = (x.a == x_1.a)
+-/
+#guard_msgs in
+#print sig instBEqPrivStruct.beq_spec
+
+end
+
+-- Try again without `public section`
+
+public structure PrivField2 where
+  private a : Nat
+deriving BEq
+
+/-- info: fun a => instBEqPrivField2.beq a a -/
+#guard_msgs in
+#with_exporting
+#reduce fun (a : PrivField2) => a == a

tests/lean/run/derivingReflBEq.lean

@@ -1,3 +1,6 @@
+namespace RegularBEq
+set_option deriving.beq.linear_construction_threshold 1000
+
 -- set_option trace.Elab.Deriving.lawfulBEq true
 
 inductive L (α : Type u) where
@@ -5,7 +8,9 @@ inductive L (α : Type u) where
   | cons : α → L α → L α
 deriving BEq, ReflBEq, LawfulBEq
 
-/-- info: theorem instReflBEqL.{u_1} : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α], ReflBEq (L α) -/
+/--
+info: theorem RegularBEq.instReflBEqL.{u_1} : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α], ReflBEq (L α)
+-/
 #guard_msgs in
 #print sig instReflBEqL
 
@@ -15,7 +20,7 @@ inductive Vec (α : Type u) : Nat → Type u where
 deriving BEq, ReflBEq, LawfulBEq
 
 /--
-info: theorem instReflBEqVec.{u_1} : ∀ {α : Type u_1} {a : Nat} [inst : BEq α] [ReflBEq α], ReflBEq (Vec α a)
+info: theorem RegularBEq.instReflBEqVec.{u_1} : ∀ {α : Type u_1} {a : Nat} [inst : BEq α] [ReflBEq α], ReflBEq (Vec α a)
 -/
 #guard_msgs in
 #print sig instReflBEqVec
@@ -25,7 +30,7 @@ inductive Enum
   | mk1 | mk2 | mk3
 deriving BEq, ReflBEq, LawfulBEq
 
-/-- info: theorem instReflBEqEnum : ReflBEq Enum -/
+/-- info: theorem RegularBEq.instReflBEqEnum : ReflBEq Enum -/
 #guard_msgs in
 #print sig instReflBEqEnum
 
@@ -38,13 +43,13 @@ inductive WithHEq (α : Type u) : Nat → Type u where
 deriving BEq, ReflBEq, LawfulBEq
 
 /--
-info: instReflBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [ReflBEq α✝] : ReflBEq (WithHEq α✝ a✝)
+info: RegularBEq.instReflBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [ReflBEq α✝] : ReflBEq (WithHEq α✝ a✝)
 -/
 #guard_msgs in
 #check instReflBEqWithHEq
 
 /--
-info: instLawfulBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [LawfulBEq α✝] : LawfulBEq (WithHEq α✝ a✝)
+info: RegularBEq.instLawfulBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [LawfulBEq α✝] : LawfulBEq (WithHEq α✝ a✝)
 -/
 #guard_msgs in
 #check instLawfulBEqWithHEq
@@ -91,3 +96,106 @@ inductive TreeList (α : Type u) where
   | cons : Tree α → TreeList α → TreeList α
   deriving BEq
 end
+
+end RegularBEq
+
+namespace LinearBEq
+set_option deriving.beq.linear_construction_threshold 0
+
+-- set_option trace.Elab.Deriving.lawfulBEq true
+
+inductive L (α : Type u) where
+  | nil  : L α
+  | cons : α → L α → L α
+deriving BEq, ReflBEq, LawfulBEq
+
+/--
+info: theorem LinearBEq.instReflBEqL.{u_1} : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α], ReflBEq (L α)
+-/
+#guard_msgs in
+#print sig instReflBEqL
+
+inductive Vec (α : Type u) : Nat → Type u where
+  | nil  : Vec α 0
+  | cons : ∀ {n}, α → Vec α n → Vec α (n+1)
+deriving BEq, ReflBEq, LawfulBEq
+
+/--
+info: theorem LinearBEq.instReflBEqVec.{u_1} : ∀ {α : Type u_1} {a : Nat} [inst : BEq α] [ReflBEq α], ReflBEq (Vec α a)
+-/
+#guard_msgs in
+#print sig instReflBEqVec
+
+
+inductive Enum
+  | mk1 | mk2 | mk3
+deriving BEq, ReflBEq, LawfulBEq
+
+/-- info: theorem LinearBEq.instReflBEqEnum : ReflBEq Enum -/
+#guard_msgs in
+#print sig instReflBEqEnum
+
+-- The following type has `Eq.rec`’s in its `BEq` implementation,
+-- but `simp` seems to handle that just fine
+
+inductive WithHEq (α : Type u) : Nat → Type u where
+  | nil  : WithHEq α 0
+  | cons : ∀ {n m} , α → WithHEq α n → WithHEq α m → WithHEq α (n+1)
+deriving BEq, ReflBEq, LawfulBEq
+
+/--
+info: LinearBEq.instReflBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [ReflBEq α✝] : ReflBEq (WithHEq α✝ a✝)
+-/
+#guard_msgs in
+#check instReflBEqWithHEq
+
+/--
+info: LinearBEq.instLawfulBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq α✝] [LawfulBEq α✝] : LawfulBEq (WithHEq α✝ a✝)
+-/
+#guard_msgs in
+#check instLawfulBEqWithHEq
+
+
+-- No `BEq` derived? Not a great error message yet, but the error location helps, so good enough.
+
+/--
+error: failed to synthesize
+  BEq Foo
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+structure Foo where
+  deriving ReflBEq
+
+-- No `ReflBEq` but `LawfulBEq`? ot a great error message yet.
+
+/--
+@ +2:16...25
+error: failed to synthesize
+  ReflBEq Bar
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs (positions := true) in
+structure Bar where
+  deriving BEq, LawfulBEq
+
+/--
+@ +5:16...23
+error: Deriving `ReflBEq` for mutual inductives is not supported
+-/
+#guard_msgs (positions := true) in
+mutual
+inductive Tree (α : Type u) where
+  | node : TreeList α → Tree α
+  | leaf : α → Tree α
+  deriving BEq, ReflBEq, LawfulBEq
+
+inductive TreeList (α : Type u) where
+  | nil : TreeList α
+  | cons : Tree α → TreeList α → TreeList α
+  deriving BEq
+end
+
+end LinearBEq

tests/lean/run/methodSpecsDeriving.lean

@@ -1,3 +1,5 @@
+set_option deriving.beq.linear_construction_threshold 1000
+
 inductive L (α : Type) where
   | nil  : L α
   | cons : α → L α → L α

tests/lean/run/reduceBEqSimproc.lean

@@ -2,6 +2,8 @@ module
 -- set_option trace.Elab.Deriving.lawfulBEq true
 -- set_option trace.Meta.MethodSpecs true
 
+set_option deriving.beq.linear_construction_threshold 1000
+
 inductive L (α : Type u) where
   | nil  : L α
   | cons : α → L α → L α
@@ -12,6 +14,41 @@ example {n m : Nat} (h : n = m) :
   simp [reduceBEq]
   assumption
 
+-- Linear construction
+
+namespace Linear
+
+set_option deriving.beq.linear_construction_threshold 0
+
+inductive L (α : Type u) where
+  | nil  : L α
+  | cons : α → L α → L α
+deriving BEq
+
+-- This should still split the equations
+
+/--
+info: Linear.instBEqL.beq.eq_1.{u_1} {α✝ : Type u_1} [BEq α✝] (x✝ x✝¹ : L α✝) :
+  instBEqL.beq x✝ x✝¹ =
+    match decEq x✝.ctorIdx x✝¹.ctorIdx with
+    | isTrue h =>
+      match x✝, x✝¹, h with
+      | L.nil, L.nil, ⋯ => true
+      | L.cons a a_1, L.cons a' a'_1, ⋯ => a == a' && instBEqL.beq a_1 a'_1
+    | isFalse h => false
+-/
+#guard_msgs in
+#check instBEqL.beq.eq_1
+
+-- And this should work without L.ctorIdx
+
+example {n m : Nat} (h : n = m) :
+    (L.cons n (L.nil : L Nat) == L.cons m (L.nil : L Nat)) = true := by
+  simp [reduceBEq, reduceCtorIdx]
+  assumption
+
+end Linear
+
 -- Module system interactions
 
 namespace A