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

@@ -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

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
   | _ =>

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