How can I elaborate with unfolding_all enabled?

Stream: lean4

[Joachim Breitner]

I want to enter terms that may only typecheck with transparency .all. Is there a way to do that? Why does definition n3 here not work:

import Lean.Elab.Command

def T := Nat → Nat
def x : T := fun n => n + 1

set_option smartUnfolding false

open Lean Meta

def n1 : Nat := x 1
attribute [irreducible] T

/--
error: function expected at
  x
term has type
  T
-/
#guard_msgs in
def n2 : Nat := x 1

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

It does seem to do something, because the error message is different, it seems. Maybe it did pass the elaborator, and is failing later in meta code now…

[Joachim Breitner]

Ok, looks like an issue elsewhere; with

diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 753ca06b52..a5cf21bc6f 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -191,7 +191,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.

it works. Fix at https://github.com/leanprover/lean4/pull/5563.