From c07ee77d33dd36c5d7dee0af6e645fa44fe8aac4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 1 Jan 2026 19:21:43 -0800
Subject: [PATCH] feat: add `Meta.Context.cacheInferType` (#11869)

This PR adds configuration flag `Meta.Context.cacheInferType`. You can
use it to disable the `inferType` cache at `MetaM`. We use this flag to
implement `SymM` because it has its own cache based on pointer equality.
---
 src/Lean/Meta/Basic.lean         |  5 +++++
 src/Lean/Meta/InferType.lean     |  2 +-
 src/Lean/Meta/Sym/InferType.lean | 12 ++++++++++--
 3 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 5e8cbb8878..db2b9ab21e 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -507,6 +507,11 @@ structure Context where
    This is not a great solution, but a proper solution would require a more sophisticated caching mechanism.
   -/
   inTypeClassResolution : Bool := false
+  /--
+  When `cacheInferType := true`, the `inferType` results are cached if the input term does not contain
+  metavariables
+  -/
+  cacheInferType : Bool := true
 deriving Inhabited
 
 def Context.config (c : Context) : Config := c.keyedConfig.config
diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 35d36d6260..541ecfba88 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -178,7 +178,7 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
   | none   => fvarId.throwUnknown
 
 @[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do
-  if e.hasMVar then
+  if !(← read).cacheInferType || e.hasMVar then
     inferType
   else
     let key ← mkExprConfigCacheKey e
diff --git a/src/Lean/Meta/Sym/InferType.lean b/src/Lean/Meta/Sym/InferType.lean
index e5252ab7d7..493b1d6feb 100644
--- a/src/Lean/Meta/Sym/InferType.lean
+++ b/src/Lean/Meta/Sym/InferType.lean
@@ -8,12 +8,20 @@ prelude
 public import Lean.Meta.Sym.SymM
 namespace Lean.Meta.Sym
 
+def inferTypeWithoutCache (e : Expr) : MetaM Expr :=
+  withReader (fun c => { c with cacheInferType := false }) do
+    Meta.inferType e
+
+def getLevelWithoutCache (type : Expr) : MetaM Level :=
+  withReader (fun c => { c with cacheInferType := false }) do
+    Meta.getLevel type
+
 /-- Returns the type of `e`. -/
 public def inferType (e : Expr) : SymM Expr := do
   if let some type := (← get).inferType.find? { expr := e } then
     return type
   else
-    let type ← Grind.shareCommonInc (← Meta.inferType e)
+    let type ← Grind.shareCommonInc (← inferTypeWithoutCache e)
     modify fun s => { s with inferType := s.inferType.insert { expr := e } type }
     return type
 
@@ -22,7 +30,7 @@ public def getLevel (type : Expr) : SymM Level := do
   if let some u := (← get).getLevel.find? { expr := type } then
     return u
   else
-    let u ← Meta.getLevel type
+    let u ← getLevelWithoutCache type
     modify fun s => { s with getLevel := s.getLevel.insert { expr := type } u }
     return u