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`.
