From ee2ce2288abc68436dc50a433f678eed3fa7c1a6 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sat, 11 Apr 2026 10:55:10 +0200 Subject: [PATCH 1/3] perf(Tactic/FastInstance): use `whnf` on data fields --- Mathlib/Tactic/FastInstance.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Tactic/FastInstance.lean b/Mathlib/Tactic/FastInstance.lean index 7a2f24d0c68348..7f139c7b2138bb 100644 --- a/Mathlib/Tactic/FastInstance.lean +++ b/Mathlib/Tactic/FastInstance.lean @@ -40,7 +40,7 @@ Many reductions for typeclasses are done with reducible transparency, so the ent is `withReducible` with some exceptions. -/ partial def makeFastInstance (inst expectedType : Expr) (trace : Array Name := #[]) : - MetaM Expr := withReducible do + MetaM Expr := withReducibleAndInstances do withTraceNode `Elab.fast_instance (fun _ => return m!"type: {expectedType}") do let some className ← isClass? expectedType | error trace m!"Can only be used for classes, but type is{indentExpr expectedType}" @@ -61,7 +61,7 @@ partial def makeFastInstance (inst expectedType : Expr) (trace : Array Name := # is not defeq to inferred instance{indentExpr new}" -- Otherwise, try to reduce it to a constructor. else - (← whnfI inst).withApp fun f args => do + (← whnf inst).withApp fun f args => do let error' (m : MessageData) : MetaM Expr := do if isStructure (← getEnv) className then error trace m @@ -102,8 +102,8 @@ partial def makeFastInstance (inst expectedType : Expr) (trace : Array Name := # mvarId.assign (← makeFastInstance arg argExpectedType (trace := trace')) else -- For data fields, make sure that the lambda binders have the right type. - forallTelescopeReducing argExpectedType fun xs _ ↦ do - mvarId.assign <| ← mkLambdaFVars xs (arg.beta xs) + mvarId.assign <| ← forallTelescopeReducing argExpectedType fun xs _ ↦ do + mkLambdaFVars xs (← whnf (mkAppN arg xs)) return mkAppN f (← mvars.mapM instantiateMVars) /-- From e283a6039368eecf557716b97584e258d0a47556 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sat, 11 Apr 2026 11:51:49 +0200 Subject: [PATCH 2/3] fix test --- MathlibTest/InferInstanceAsPercent.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MathlibTest/InferInstanceAsPercent.lean b/MathlibTest/InferInstanceAsPercent.lean index 177ad275bbb621..e86e263fa2b193 100644 --- a/MathlibTest/InferInstanceAsPercent.lean +++ b/MathlibTest/InferInstanceAsPercent.lean @@ -35,7 +35,7 @@ instance myNatInv_fixed : MyInv MyNat := -- The binder type is `MyNat`: /-- info: @[implicit_reducible] def myNatInv_fixed : MyInv MyNat := -{ myInv := fun (a : MyNat) => a + 1 } +{ myInv := fun (a : MyNat) => (Nat.add a 0).succ } -/ #guard_msgs in #print myNatInv_fixed From b6ad48a8addfccadcdd2ef2528c395049f2271b2 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Tue, 28 Apr 2026 18:15:12 +0100 Subject: [PATCH 3/3] don't change the transparency --- Mathlib/Tactic/FastInstance.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Tactic/FastInstance.lean b/Mathlib/Tactic/FastInstance.lean index 7f139c7b2138bb..3af61e032a5ab9 100644 --- a/Mathlib/Tactic/FastInstance.lean +++ b/Mathlib/Tactic/FastInstance.lean @@ -40,7 +40,7 @@ Many reductions for typeclasses are done with reducible transparency, so the ent is `withReducible` with some exceptions. -/ partial def makeFastInstance (inst expectedType : Expr) (trace : Array Name := #[]) : - MetaM Expr := withReducibleAndInstances do + MetaM Expr := withReducible do withTraceNode `Elab.fast_instance (fun _ => return m!"type: {expectedType}") do let some className ← isClass? expectedType | error trace m!"Can only be used for classes, but type is{indentExpr expectedType}" @@ -61,7 +61,7 @@ partial def makeFastInstance (inst expectedType : Expr) (trace : Array Name := # is not defeq to inferred instance{indentExpr new}" -- Otherwise, try to reduce it to a constructor. else - (← whnf inst).withApp fun f args => do + (← whnfI inst).withApp fun f args => do let error' (m : MessageData) : MetaM Expr := do if isStructure (← getEnv) className then error trace m @@ -103,7 +103,7 @@ partial def makeFastInstance (inst expectedType : Expr) (trace : Array Name := # else -- For data fields, make sure that the lambda binders have the right type. mvarId.assign <| ← forallTelescopeReducing argExpectedType fun xs _ ↦ do - mkLambdaFVars xs (← whnf (mkAppN arg xs)) + mkLambdaFVars xs (← whnfI (mkAppN arg xs)) return mkAppN f (← mvars.mapM instantiateMVars) /--