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