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

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

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

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