diff --git a/src/Lean/Elab/BuiltinDo/For.lean b/src/Lean/Elab/BuiltinDo/For.lean
index a7b171c60d..0f79217198 100644
--- a/src/Lean/Elab/BuiltinDo/For.lean
+++ b/src/Lean/Elab/BuiltinDo/For.lean
@@ -185,7 +185,7 @@ open Lean.Meta
         if info.returnsEarly then
           let ret ← getFVarFromUserName returnVarName
           let ret ← if loopMutVars.isEmpty then mkAppM ``Prod.fst #[ret] else pure ret
-          let motive := mkLambda `_ .default (← inferType ret) (← mkMonadicType γ)
+          let motive := mkLambda `_ .default (← inferType ret) (← mkMonadApp γ)
           let app := mkApp3 (mkConst ``Break.runK.match_1 [mi.u, mi.v.succ]) oldReturnCont.resultType motive ret
           let none := mkSimpleThunk (← dec.continueWithUnit)
           let some ← withLocalDeclD (← mkFreshUserName `r) oldReturnCont.resultType fun r => do
diff --git a/src/Lean/Elab/BuiltinDo/If.lean b/src/Lean/Elab/BuiltinDo/If.lean
index 04e4215fb7..5f6fa8dff9 100644
--- a/src/Lean/Elab/BuiltinDo/If.lean
+++ b/src/Lean/Elab/BuiltinDo/If.lean
@@ -54,7 +54,7 @@ where
     -- elaborator. However, for Lake.Package.mkBuildArchiveFacetConfig, we still need to postpone.
     doElabToSyntax "then branch of if with condition {cond}" (elabDoSeq thenSeq dec) fun then_ => do
     doElabToSyntax "else branch of if with condition {cond}" (elabDoSeq elseSeq dec) fun else_ => do
-    let mγ ← mkMonadicType (← read).doBlockResultType
+    let mγ ← mkMonadApp (← read).doBlockResultType
     Term.elabTermEnsuringType (← `(if $cond then $then_ else $else_)) mγ
 
   elabDite h cond thenSeq elseSeq dec := do
@@ -62,7 +62,7 @@ where
       elabDoSeq (if then_ then thenSeq else elseSeq) dec
     doElabToSyntax "then branch of if with condition {cond}" (elabDiteBranch true) fun then_ => do
     doElabToSyntax "else branch of if with condition {cond}" (elabDiteBranch false) fun else_ => do
-    let mγ ← mkMonadicType (← read).doBlockResultType
+    let mγ ← mkMonadApp (← read).doBlockResultType
     match h with
     | `(_%$tk) => Term.elabTermEnsuringType (← `(if _%$tk : $cond then $then_ else $else_)) mγ
     | `($h:ident) => Term.elabTermEnsuringType (← `(if $h:ident : $cond then $then_ else $else_)) mγ
diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index b8deb6c9c4..8c3fbc7978 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -95,7 +95,7 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
   let dec ← dec.ensureUnitAt tk
   -- Some decl preprocessing on the patterns and expected types:
   let decl ← pushTypeIntoReassignment letOrReassign decl
-  let mγ ← mkMonadicType (← read).doBlockResultType
+  let mγ ← mkMonadApp (← read).doBlockResultType
   match decl with
   | `(letDecl| $decl:letEqnsDecl) =>
     let declNew ← `(letDecl| $(⟨← liftMacroM <| Term.expandLetEqnsDecl decl⟩):letIdDecl)
@@ -221,7 +221,7 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   let `(doLetRec| let%$tk rec $decls:letRecDecls) := stx | throwUnsupportedSyntax
   let dec ← dec.ensureUnitAt tk
   let vars ← getLetRecDeclsVars decls
-  let mγ ← mkMonadicType (← read).doBlockResultType
+  let mγ ← mkMonadApp (← read).doBlockResultType
   doElabToSyntax m!"let rec body of group {vars}" dec.continueWithUnit fun body => do
     -- Let recs may never have nested actions. We expand just for the sake of error messages.
     -- This suppresses error messages for the let body. Not sure if this is a good call, but it was
diff --git a/src/Lean/Elab/BuiltinDo/Match.lean b/src/Lean/Elab/BuiltinDo/Match.lean
index 5b22db885f..5352a43cae 100644
--- a/src/Lean/Elab/BuiltinDo/Match.lean
+++ b/src/Lean/Elab/BuiltinDo/Match.lean
@@ -26,9 +26,9 @@ open Lean.Meta.Match
 private def elabDoSeqWithRefinedType (type : Expr) (doSeq : TSyntax ``doSeq) (dec : DoElemCont) : DoElabM Expr := do
   let newDoBlockResultType ← withNewMCtxDepth do
     let γ ← mkFreshExprMVar (mkSort (← read).monadInfo.u.succ)
-    unless ← isDefEqGuarded type (← mkMonadicType γ) do
+    unless ← isDefEqGuarded type (← mkMonadApp γ) do
       throwError "Could not determine dependently-refined result type of `do` block.\n
-        Expected type {type} was not def eq to {← mkMonadicType γ}"
+        Expected type {type} was not def eq to {← mkMonadApp γ}"
     instantiateMVars γ
   trace[Elab.do.match] "newDoBlockResultType: {newDoBlockResultType}"
   -- The `doBlockResultType` *is* the continuation's return type, since it is duplicable.
@@ -47,7 +47,7 @@ The rest of the code in this file is concerned with providing the default, non-d
 private def expandToTermMatch : DoElab := fun stx dec => do
   let `(doMatch| match $[(dependent := $dep?)]? $[(generalizing := $gen?)]? $[(motive := $motive?)]? $discrs:matchDiscr,* with $alts:matchAlt*) := stx | throwUnsupportedSyntax
   let doBlockResultType := (← read).doBlockResultType
-  let mγ ← mkMonadicType doBlockResultType
+  let mγ ← mkMonadApp doBlockResultType
   -- trace[Elab.do] "expandToTermMatch. mγ: {mγ}, dec.resultType: {dec.resultType}, dec.duplicable: {dec.kind matches .duplicable ..}"
   let info ← inferControlInfoElem stx
   let dependent := dep?.getD ⟨.missing⟩ matches `(trueVal| true)
@@ -183,7 +183,7 @@ private def elabMatchAlt (discrs : Array Term.Discr) (matchType : Expr)
 
 private def elabMatchAlts (discrs : Array Term.Discr) (alts : Array DoMatchAltView) (dec : DoElemCont) : DoElabM (Expr × Array AltLHS × Array Expr) := do
   let alts ← liftMacroM <| Term.expandMacrosInPatterns alts
-  let matchType ← mkDepMatchMotive discrs (← mkMonadicType (← read).doBlockResultType)
+  let matchType ← mkDepMatchMotive discrs (← mkMonadApp (← read).doBlockResultType)
   let (lhss, rhss) ← Array.unzip <$> alts.mapM (elabMatchAlt discrs matchType · dec)
   return (matchType, lhss, rhss)
 
diff --git a/src/Lean/Elab/BuiltinDo/MatchExpr.lean b/src/Lean/Elab/BuiltinDo/MatchExpr.lean
index 223d236fe1..d9cdd0ec15 100644
--- a/src/Lean/Elab/BuiltinDo/MatchExpr.lean
+++ b/src/Lean/Elab/BuiltinDo/MatchExpr.lean
@@ -60,6 +60,6 @@ where elabDoMatchExprNoMeta (info : ControlInfo) (discr : Term) (alts : TSyntax
         doElabToSyntax m!"match_expr else alternative" (ref := elseSeq) (elabDoSeq ⟨elseSeq⟩ dec) fun rhs => do
           let alts : TSyntax ``matchExprAlts := ⟨alts.raw.modifyArg 0 fun node => node.setArgs altsArr⟩
           let alts : TSyntax ``matchExprAlts := ⟨alts.raw.modifyArg 1 (·.setArg 3 rhs)⟩
-          let mγ ← mkMonadicType (← read).doBlockResultType
+          let mγ ← mkMonadApp (← read).doBlockResultType
           Term.elabTerm (← `(match_expr $discr with $alts)) mγ
     elabMatch 0 (alts.raw[0].getArgs.map (⟨·⟩))
diff --git a/src/Lean/Elab/BuiltinDo/Misc.lean b/src/Lean/Elab/BuiltinDo/Misc.lean
index 1985c5cdcb..60d7bfada8 100644
--- a/src/Lean/Elab/BuiltinDo/Misc.lean
+++ b/src/Lean/Elab/BuiltinDo/Misc.lean
@@ -24,7 +24,7 @@ open InternalSyntax in
 
 @[builtin_doElem_elab Lean.Parser.Term.doExpr] def elabDoExpr : DoElab := fun stx dec => do
   let `(doExpr| $e:term) := stx | throwUnsupportedSyntax
-  let mα ← mkMonadicType dec.resultType
+  let mα ← mkMonadApp dec.resultType
   let e ← Term.elabTermEnsuringType e mα
   dec.mkBindUnlessPure e
 
@@ -39,21 +39,21 @@ open InternalSyntax in
 
 @[builtin_doElem_elab Lean.Parser.Term.doDbgTrace] def elabDoDbgTrace : DoElab := fun stx dec => do
   let `(doDbgTrace| dbg_trace%$tk $msg:term) := stx | throwUnsupportedSyntax
-  let mγ ← mkMonadicType (← read).doBlockResultType
+  let mγ ← mkMonadApp (← read).doBlockResultType
   let dec ← dec.ensureUnitAt tk
   doElabToSyntax "dbg_trace body" dec.continueWithUnit fun body => do
   Term.elabTerm (← `(dbg_trace $msg; $body)) mγ
 
 @[builtin_doElem_elab Lean.Parser.Term.doAssert] def elabDoAssert : DoElab := fun stx dec => do
   let `(doAssert| assert!%$tk $cond) := stx | throwUnsupportedSyntax
-  let mγ ← mkMonadicType (← read).doBlockResultType
+  let mγ ← mkMonadApp (← read).doBlockResultType
   let dec ← dec.ensureUnitAt tk
   doElabToSyntax "assert! body" dec.continueWithUnit fun body => do
   Term.elabTerm (← `(assert! $cond; $body)) mγ
 
 @[builtin_doElem_elab Lean.Parser.Term.doDebugAssert] def elabDoDebugAssert : DoElab := fun stx dec => do
   let `(doDebugAssert| debug_assert!%$tk $cond) := stx | throwUnsupportedSyntax
-  let mγ ← mkMonadicType (← read).doBlockResultType
+  let mγ ← mkMonadApp (← read).doBlockResultType
   let dec ← dec.ensureUnitAt tk
   doElabToSyntax "debug_assert! body" dec.continueWithUnit fun body => do
   Term.elabTerm (← `(debug_assert! $cond; $body)) mγ
diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index 16dd038f74..ac8a7d0791 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -225,7 +225,7 @@ unsafe def ContInfoRef.toContInfoImpl (m : ContInfoRef) : ContInfo :=
 opaque ContInfoRef.toContInfo (m : ContInfoRef) : ContInfo
 
 /-- Constructs `m α` from `α`. -/
-def mkMonadicType (resultType : Expr) : DoElabM Expr :=
+def mkMonadApp (resultType : Expr) : DoElabM Expr :=
   return mkApp (← read).monadInfo.m resultType
 
 /-- The cached `PUnit` expression. -/
@@ -469,7 +469,7 @@ the bind if `$(← dec.k)` is `pure $dec.resultName` or `e` is some `pure` compu
 -/
 def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr := do
   -- let eResultTy ← mkFreshResultType
-  -- let e ← Term.ensureHasType (← mkMonadicType eResultTy) e
+  -- let e ← Term.ensureHasType (← mkMonadApp eResultTy) e
   -- let dec ← dec.ensureHasType eResultTy
   let x := dec.resultName
   let k := dec.k
@@ -505,7 +505,7 @@ 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 body ← Term.ensureHasType (← mkMonadicType kResultTy) body
+    let body ← Term.ensureHasType (← mkMonadApp kResultTy) body
     let k ← mkLambdaFVars #[xFVar] body
     mkBindApp eResultTy kResultTy e k
 
@@ -603,7 +603,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
   if nondupDec.kind matches .duplicable .. then
     return ← caller nondupDec
   let γ := (← read).doBlockResultType
-  let mγ ← mkMonadicType γ
+  let mγ ← mkMonadApp γ
   let mutVars := (← read).mutVars |>.filter (callerInfo.reassigns.contains ·.getId)
   let mutVarNames := mutVars.map (·.getId)
   let joinName ← mkFreshUserName `__do_jp
@@ -869,7 +869,7 @@ private def elabDoElemFns (stx : TSyntax `doElem) (cont : DoElemCont)
   match fns with
   | [] => throwError "unexpected `do` element syntax{indentD stx}"
   | elabFn :: elabFns =>
-    let expectedType ← mkMonadicType (← read).doBlockResultType
+    let expectedType ← mkMonadApp (← read).doBlockResultType
     withTermInfoContext' elabFn.declName stx (expectedType := expectedType) do
       try
         elabFn.value stx cont
@@ -897,7 +897,7 @@ partial def elabDoElem (stx : TSyntax `doElem) (cont : DoElemCont) (catchExPostp
   checkSystem "do element elaborator"
   profileitM Exception "do element elaborator" (decl := k) (← getOptions) <|
   withRef stx <| withIncRecDepth <| withFreshMacroScope <| do
-  let mγ ← mkMonadicType (← read).doBlockResultType
+  let mγ ← mkMonadApp (← read).doBlockResultType
   if (← read).deadCode matches .deadSyntactically then
     logWarningAt stx "This `do` element and its control-flow region are dead code. Consider removing it."
     return ← mkFreshExprMVar mγ (userName := `deadCode)
@@ -940,7 +940,7 @@ partial def elabDoSeq (doSeq : TSyntax ``doSeq) (cont : DoElemCont) (catchExPost
     | .internal id _ =>
       if catchExPostpone && id == postponeExceptionId then
         s.restore
-        let expectedType ← mkMonadicType (← read).doBlockResultType
+        let expectedType ← mkMonadApp (← read).doBlockResultType
         doElabToSyntax m!"do sequence {doSeq}" (elabDoSeq doSeq cont) (Term.postponeElabTerm · expectedType)
       else
         throw ex
diff --git a/src/Lean/Elab/Do/Control.lean b/src/Lean/Elab/Do/Control.lean
index d14fb5121f..fd8a6ee27a 100644
--- a/src/Lean/Elab/Do/Control.lean
+++ b/src/Lean/Elab/Do/Control.lean
@@ -89,7 +89,7 @@ def ControlStack.optionT (baseMonadInfo : MonadInfo) (optionTWrapper casesOnWrap
         mkLambdaFVars #[r] (← outerCont)
       let ksuccess ← withLocalDeclD dec.resultName dec.resultType fun r => do
         mkLambdaFVars #[r] (← dec.k)
-      let β ← mkMonadicType (← read).doBlockResultType
+      let β ← mkMonadApp (← read).doBlockResultType
       return mkApp5 (mkConst casesOnWrapper [baseMonadInfo.u, baseMonadInfo.v]) dec.resultType β e kexit ksuccess
     base.restoreCont { resultName, resultType, k }
 where
@@ -150,7 +150,7 @@ def ControlStack.mkBreak (base : ControlStack) (hasContinue : Bool) : DoElabM Ex
   -- When there's an outer `continue` layer as well, we account for that by applying `stM` of
   -- `OptionT` to `α`.
   let α := if hasContinue then mkApp (mkConst ``Option [mi.u]) α else α
-  let mγ ← mkMonadicType (← read).doBlockResultType
+  let mγ ← mkMonadApp (← read).doBlockResultType
   let res ← base.runInBase <| mkApp3 (mkConst ``BreakT.break [mi.u, mi.v]) α mi.m inst
   let ty ← inferType res
   -- Now instantiate `α`
@@ -161,7 +161,7 @@ def ControlStack.mkContinue (base : ControlStack) : DoElabM Expr := do
   let mi := { (← read).monadInfo with m := (← base.m) }
   let inst ← mkInstMonad mi
   let α ← mkFreshResultType `α
-  let mγ ← mkMonadicType (← read).doBlockResultType
+  let mγ ← mkMonadApp (← read).doBlockResultType
   let res ← base.runInBase <| mkApp3 (mkConst ``ContinueT.continue [mi.u, mi.v]) α mi.m inst
   let ty ← inferType res
   -- Now instantiate `α`
@@ -173,7 +173,7 @@ def ControlStack.mkReturn (base : ControlStack) (r : Expr) : DoElabM Expr := do
   let instMonad ← mkInstMonad mi
   let ρ ← inferType r
   let δ ← mkFreshResultType `δ
-  let mγ ← mkMonadicType (← read).doBlockResultType
+  let mγ ← mkMonadApp (← read).doBlockResultType
   let mγ' := mkApp mi.m (mkApp2 (mkConst ``Except [mi.u, mi.v]) ρ δ)
   synthUsingDefEq "early return result type" mγ mγ'
   base.runInBase <| mkApp5 (mkConst ``EarlyReturnT.return [mi.u, mi.v]) ρ mi.m δ instMonad r
diff --git a/src/Lean/Elab/Idbg.lean b/src/Lean/Elab/Idbg.lean
index fa1954f2cd..feb7035623 100644
--- a/src/Lean/Elab/Idbg.lean
+++ b/src/Lean/Elab/Idbg.lean
@@ -365,7 +365,7 @@ def elabIdbgTerm : TermElab := fun stx expectedType? => do
 @[builtin_doElem_elab Lean.Parser.Term.doIdbg]
 def elabDoIdbg : DoElab := fun stx dec => do
   let `(Lean.Parser.Term.doIdbg| idbg%$tk $e) := stx | throwUnsupportedSyntax
-  let mγ ← mkMonadicType (← read).doBlockResultType
+  let mγ ← mkMonadApp (← read).doBlockResultType
   let dec ← dec.ensureUnitAt tk
   doElabToSyntax "idbg body" dec.continueWithUnit fun body => do
     elabIdbgCore (e := e) (body := body) (ref := stx) mγ