From cbda692e7e68e40ed7aed699a96cdc85d91635a7 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Mon, 13 Apr 2026 20:51:45 +0200
Subject: [PATCH] fix: free variable in `do` bind when continuation type
 depends on bvar (#13396)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes #12768, where the new `do` elaborator produced a
"declaration has free variables" kernel error when the bind
continuation's result type was definitionally but not syntactically
independent of the bound variable. The fix moves creation of the result
type metavariable before `withLocalDecl`, so the unifier must reduce
away the dependency.

For example, given `def Quoted (x : Nat) := Nat`, the expression `do let
val ← pure 3; withStuff val do return 3` would fail because `β` was
assigned `Quoted val` rather than `Nat`.
---
 src/Lean/Elab/Do/Basic.lean          |  2 +-
 tests/elab/due_to_metavariables.lean |  2 +-
 tests/elab/issue12768.lean           | 13 +++++++++++++
 tests/elab/newdo.lean                |  6 +++---
 4 files changed, 18 insertions(+), 5 deletions(-)
 create mode 100644 tests/elab/issue12768.lean

diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index ae373d1cd7..891217489b 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -384,6 +384,7 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
   let k := dec.k
   -- The .ofBinderName below is mainly to interpret `__do_lift` binders as implementation details.
   let declKind := .ofBinderName x
+  let kResultTy ← mkFreshResultType `kResultTy
   withLocalDecl x .default eResultTy (kind := declKind) fun xFVar => do
     let body ← k
     let body' := body.consumeMData
@@ -411,7 +412,6 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
         -- else -- would be too aggressive
         --   return ← mapLetDecl (nondep := true) (kind := declKind) x eResultTy eRes fun _ => k ref
 
-    let kResultTy ← mkFreshResultType `kResultTy
     let body ← Term.ensureHasType (← mkMonadicType kResultTy) body
     let k ← mkLambdaFVars #[xFVar] body
     mkBindApp eResultTy kResultTy e k
diff --git a/tests/elab/due_to_metavariables.lean b/tests/elab/due_to_metavariables.lean
index a7828b9aef..8cac6008e4 100644
--- a/tests/elab/due_to_metavariables.lean
+++ b/tests/elab/due_to_metavariables.lean
@@ -101,7 +101,7 @@ would also work here.
 error: Application type mismatch: The argument
   isDigitEven? n
 has type
-  ?m.2 Bool
+  ?m.3 Bool
 but is expected to have type
   Prop
 in the application
diff --git a/tests/elab/issue12768.lean b/tests/elab/issue12768.lean
new file mode 100644
index 0000000000..f7a9f91fb7
--- /dev/null
+++ b/tests/elab/issue12768.lean
@@ -0,0 +1,13 @@
+module
+
+set_option backward.do.legacy false
+
+set_option linter.unusedVariables.funArgs false in
+def Quoted (x : Nat) := Nat
+
+def withStuff (x : Nat) (f : IO (Quoted x)) : IO (Quoted x) := f
+
+def myFunc : IO Nat := do
+  let val : Nat ← pure 3
+  withStuff val do
+    return (3 : Nat)
diff --git a/tests/elab/newdo.lean b/tests/elab/newdo.lean
index 50dd974bce..3a7ab15a46 100644
--- a/tests/elab/newdo.lean
+++ b/tests/elab/newdo.lean
@@ -108,7 +108,7 @@ Hint: Adding type annotations and supplying implicit arguments to functions can
 example := do return 42
 /--
 error: typeclass instance problem is stuck
-  Bind ?m.23
+  Bind ?m.22
 
 Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Bind` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
 
@@ -211,8 +211,8 @@ trace: [Elab.do] let x := 42;
               else
                 let x := x + i;
                 pure (ForInStep.yield (none, x))
-    let __r : Option ?m.182 := __s.fst
-    let x : ?m.182 := __s.snd
+    let __r : Option ?m.185 := __s.fst
+    let x : ?m.185 := __s.snd
     match __r with
       | some r => pure r
       | none =>