fix: getFunInfo, inferType to use withAtLeastTransparency, not withTransparency (#5563)

when the transparency mode is `.all`, then one expects `getFunInfo` and
`inferType` to also work with that transparency mode.

Fixes #5562
Fixes #2975 
Fixes #2194

src/Lean/Meta/Basic.lean

@@ -246,12 +246,20 @@ structure DefEqCache where
   all       : PersistentHashMap (Expr × Expr) Bool := {}
   deriving Inhabited
 
+/--
+  A cache for `inferType` at transparency levels `.default` an `.all`.
+-/
+structure InferTypeCaches where
+  default   : InferTypeCache
+  all       : InferTypeCache
+  deriving Inhabited
+
 /--
   Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
 -/
 structure Cache where
-  inferType      : InferTypeCache := {}
-  funInfo        : FunInfoCache   := {}
+  inferType      : InferTypeCaches := ⟨{}, {}⟩
+  funInfo        : FunInfoCache := {}
   synthInstance  : SynthInstanceCache := {}
   whnfDefault    : WhnfCache := {} -- cache for closed terms and `TransparencyMode.default`
   whnfAll        : WhnfCache := {} -- cache for closed terms and `TransparencyMode.all`
@@ -478,8 +486,11 @@ variable [MonadControlT MetaM n] [Monad n]
 @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit :=
   modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed, diag }
 
-@[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
-  modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩
+@[inline] def modifyInferTypeCacheDefault (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
+  modifyCache fun ⟨⟨icd, ica⟩, c1, c2, c3, c4, c5, c6⟩ => ⟨⟨f icd, ica⟩, c1, c2, c3, c4, c5, c6⟩
+
+@[inline] def modifyInferTypeCacheAll (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
+  modifyCache fun ⟨⟨icd, ica⟩, c1, c2, c3, c4, c5, c6⟩ => ⟨⟨icd, f ica⟩, c1, c2, c3, c4, c5, c6⟩
 
 @[inline] def modifyDefEqTransientCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
   modifyCache fun ⟨c1, c2, c3, c4, c5, defeqTrans, c6⟩ => ⟨c1, c2, c3, c4, c5, f defeqTrans, c6⟩

src/Lean/Meta/FunInfo.lean

@@ -55,7 +55,7 @@ private def updateHasFwdDeps (pinfo : Array ParamInfo) (backDeps : Array Nat) :
 private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
   checkFunInfoCache fn maxArgs? do
     let fnType ← inferType fn
-    withTransparency TransparencyMode.default do
+    withAtLeastTransparency TransparencyMode.default do
       forallBoundedTelescope fnType maxArgs? fun fvars type => do
         let mut paramInfo := #[]
         let mut higherOrderOutParams : FVarIdSet := {}

src/Lean/Meta/InferType.lean

@@ -166,13 +166,24 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
   | none   => fvarId.throwUnknown
 
 @[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do
-  match (← get).cache.inferType.find? e with
-  | some type => return type
-  | none =>
-    let type ← inferType
-    unless e.hasMVar || type.hasMVar do
-      modifyInferTypeCache fun c => c.insert e type
-    return type
+  match (← getTransparency) with
+  | .default =>
+    match (← get).cache.inferType.default.find? e with
+    | some type => return type
+    | none =>
+      let type ← inferType
+      unless e.hasMVar || type.hasMVar do
+        modifyInferTypeCacheDefault fun c => c.insert e type
+      return type
+  | .all =>
+    match (← get).cache.inferType.all.find? e with
+    | some type => return type
+    | none =>
+      let type ← inferType
+      unless e.hasMVar || type.hasMVar do
+        modifyInferTypeCacheAll fun c => c.insert e type
+      return type
+  | _ => panic! "checkInferTypeCache: transparency mode not default or all"
 
 @[export lean_infer_type]
 def inferTypeImp (e : Expr) : MetaM Expr :=
@@ -191,7 +202,7 @@ def inferTypeImp (e : Expr) : MetaM Expr :=
     | .forallE ..    => checkInferTypeCache e (inferForallType e)
     | .lam ..        => checkInferTypeCache e (inferLambdaType e)
     | .letE ..       => checkInferTypeCache e (inferLambdaType e)
-  withIncRecDepth <| withTransparency TransparencyMode.default (infer e)
+  withIncRecDepth <| withAtLeastTransparency TransparencyMode.default (infer e)
 
 /--
   Return `LBool.true` if given level is always equivalent to universe level zero.

stage0/src/stdlib_flags.h

@@ -6,7 +6,7 @@ options get_default_options() {
     // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `true` for changing built-in parsers used in quotations
     opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax

tests/lean/run/issue2975.lean

@@ -0,0 +1,19 @@
+import Lean
+open Lean Meta Elab Term
+
+elab "#reduce'" t:term : command => Elab.Command.runTermElabM fun _ => do
+  let e ← withSynthesize <| elabTerm t none
+  let e ← Meta.reduce e
+  withTransparency TransparencyMode.all do
+    logInfo m!"{← inferType e}"
+
+structure S where
+  x : Nat
+
+def S' := S
+def S'.x (s : S') : Nat := S.x s
+
+attribute [irreducible] S'
+
+variable (s : S')
+#reduce' s.x

tests/lean/run/issue5562.lean

@@ -0,0 +1,63 @@
+import Lean
+
+/-!
+This test checks that we can enter, typecheck etc. terms that are only type-correct at
+transparency `all`.
+-/
+
+open Lean Meta
+
+
+def T := Nat → Nat
+def x : T := fun n => n + 1
+
+-- All well:
+def n1 : Nat := x 1
+
+
+-- Now we make `T` irreducible. A bunch of things should break:
+
+attribute [irreducible] T
+
+/--
+error: function expected at
+  x
+term has type
+  T
+-/
+#guard_msgs in
+def n2 : Nat := x 1
+
+
+-- NB: Checking does not break! Always done at transparency `all`.
+run_meta do
+  Meta.check (.app (mkConst ``x) (mkNatLit 1))
+
+-- Type inference fails:
+
+/--
+error: function expected
+  x 1
+-/
+#guard_msgs in
+run_meta do
+  let _ ← Meta.inferType (.app (mkConst ``x) (mkNatLit 1))
+
+-- But succeeds at transparency .all
+
+run_meta do
+  withTransparency .all do
+    let _ ← Meta.inferType (.app (mkConst ``x) (mkNatLit 1))
+
+-- An elaborator that sets transparency to .all:
+
+elab "with_unfolding_all" t:term : term <= expectedType? =>
+  withTransparency .all <|
+    Elab.Term.elabTerm t expectedType?
+
+/--
+error: function expected
+  x 1
+-/
+#guard_msgs in
+def n3 : Nat := with_unfolding_all x 1