From 0e122870beca37a34293278c388c26605b0bbfa3 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 19 Sep 2025 12:51:17 +0200
Subject: [PATCH] perf: mkNoConfusionCtors: cheaper `inferType` (#10455)

This PR changes `mkNoConfusionCtors` so that its use of `inferType` does
not have to reduce `noConfusionType`, to make #10315 really effective.
---
 src/Lean/Meta/Constructions/NoConfusion.lean | 3 ++-
 tests/bench/big_beq.lean                     | 2 +-
 tests/lean/run/noConfusionCtors.lean         | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/Constructions/NoConfusion.lean b/src/Lean/Meta/Constructions/NoConfusion.lean
index 167f9067e2..02c2583ab3 100644
--- a/src/Lean/Meta/Constructions/NoConfusion.lean
+++ b/src/Lean/Meta/Constructions/NoConfusion.lean
@@ -243,9 +243,10 @@ def mkNoConfusionCtors (declName : Name) : MetaM Unit := do
               -- computation that `noConfusionType h` is equal to `$kType → P`
               let kType ← mkNoConfusionCtorArg ctor P
               let kType := kType.beta (xs ++ fields1 ++ fields2)
-              withLocalDeclD `k kType fun k =>
+              withLocalDeclD `k kType fun k => do
                 let e := mkConst noConfusionName (v :: us)
                 let e := mkAppN e (xs ++ indices ++ #[P, ctor1, ctor2, h, k])
+                let e ← mkExpectedTypeHint e P
                 mkLambdaFVars (xs ++ #[P] ++ ys ++ #[h, k]) e
       let name := ctor.str "noConfusion"
       addDecl (.defnDecl (← mkDefinitionValInferringUnsafe
diff --git a/tests/bench/big_beq.lean b/tests/bench/big_beq.lean
index fc61b808a7..2da165f636 100644
--- a/tests/bench/big_beq.lean
+++ b/tests/bench/big_beq.lean
@@ -33,7 +33,7 @@ def testGenImpl: CommandElab := fun stx => do
       -- Create constant case definitions
       `(inductive $t:ident (α : Type) : Type where
         $cons:ctor*
-        deriving BEq
+        deriving instance BEq for $t:ident
       )
     elabCommand idecl
   | _ =>
diff --git a/tests/lean/run/noConfusionCtors.lean b/tests/lean/run/noConfusionCtors.lean
index 0eb94585b3..26535aa173 100644
--- a/tests/lean/run/noConfusionCtors.lean
+++ b/tests/lean/run/noConfusionCtors.lean
@@ -82,7 +82,7 @@ info: @[reducible] def Tmₛ.app.noConfusion.{u_1, u} : (P : Sort u_1) →
     {A : T → Tyₛ} →
       (a : Tmₛ (Tyₛ.SPi T A)) →
         (arg : T) → (a' : Tmₛ (Tyₛ.SPi T A)) → a.app arg = a'.app arg → (T = T → A ≍ A → a ≍ a' → arg ≍ arg → P) → P :=
-fun P {T} {A} a arg a' h k => Tmₛ.noConfusion h k
+fun P {T} {A} a arg a' h k => id (Tmₛ.noConfusion h k)
 -/
 #guard_msgs in #print Tmₛ.app.noConfusion