diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index af1dac4aa5..f78636d030 100644
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@@ -64,3 +64,8 @@ instance : MonadExceptOf Unit (OptionT m) := {
 }
 
 end OptionT
+
+abbrev OptionM (α : Type u) := OptionT Id α
+
+abbrev OptionM.run (x : OptionM α) : Option α :=
+  x
diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean
index a70a3fbbdd..28e2338aab 100644
--- a/src/Init/Data/ToString/Basic.lean
+++ b/src/Init/Data/ToString/Basic.lean
@@ -11,6 +11,7 @@ import Init.Data.Repr
 import Init.Data.Int.Basic
 import Init.Data.Format.Basic
 import Init.Control.Id
+import Init.Control.Option
 open Sum Subtype Nat
 
 open Std
@@ -120,11 +121,12 @@ instance {α : Type u} {p : α → Prop} [ToString α] : ToString (Subtype p) :=
   toString (val s)⟩
 
 def String.toInt? (s : String) : Option Int :=
-  if s.get 0 = '-' then do
-    let v ← (s.toSubstring.drop 1).toNat?;
-    pure <| - Int.ofNat v
-  else
-   Int.ofNat <$> s.toNat?
+  OptionM.run do
+    if s.get 0 = '-' then do
+      let v ← (s.toSubstring.drop 1).toNat?;
+      pure <| - Int.ofNat v
+    else
+     Int.ofNat <$> s.toNat?
 
 def String.isInt (s : String) : Bool :=
   if s.get 0 = '-' then
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 2f6cc62738..d7673fd02b 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -501,40 +501,42 @@ def toNat (stx : Syntax) : Nat :=
   | some val => val
   | none     => 0
 
-def decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) := do
-  let c := s.get i
-  let i := s.next i
-  if c == '\\' then pure ('\\', i)
-  else if c = '\"' then pure ('\"', i)
-  else if c = '\'' then pure ('\'', i)
-  else if c = 'r'  then pure ('\r', i)
-  else if c = 'n'  then pure ('\n', i)
-  else if c = 't'  then pure ('\t', i)
-  else if c = 'x'  then
-    let (d₁, i) ← decodeHexDigit s i
-    let (d₂, i) ← decodeHexDigit s i
-    pure (Char.ofNat (16*d₁ + d₂), i)
-  else if c = 'u'  then do
-    let (d₁, i) ← decodeHexDigit s i
-    let (d₂, i) ← decodeHexDigit s i
-    let (d₃, i) ← decodeHexDigit s i
-    let (d₄, i) ← decodeHexDigit s i
-    pure (Char.ofNat (16*(16*(16*d₁ + d₂) + d₃) + d₄), i)
-  else
-    none
+def decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) :=
+  OptionM.run do
+    let c := s.get i
+    let i := s.next i
+    if c == '\\' then pure ('\\', i)
+    else if c = '\"' then pure ('\"', i)
+    else if c = '\'' then pure ('\'', i)
+    else if c = 'r'  then pure ('\r', i)
+    else if c = 'n'  then pure ('\n', i)
+    else if c = 't'  then pure ('\t', i)
+    else if c = 'x'  then
+      let (d₁, i) ← decodeHexDigit s i
+      let (d₂, i) ← decodeHexDigit s i
+      pure (Char.ofNat (16*d₁ + d₂), i)
+    else if c = 'u'  then do
+      let (d₁, i) ← decodeHexDigit s i
+      let (d₂, i) ← decodeHexDigit s i
+      let (d₃, i) ← decodeHexDigit s i
+      let (d₄, i) ← decodeHexDigit s i
+      pure (Char.ofNat (16*(16*(16*d₁ + d₂) + d₃) + d₄), i)
+    else
+      none
 
-partial def decodeStrLitAux (s : String) (i : String.Pos) (acc : String) : Option String := do
-  let c := s.get i
-  let i := s.next i
-  if c == '\"' then
-    pure acc
-  else if s.atEnd i then
-    none
-  else if c == '\\' then do
-    let (c, i) ← decodeQuotedChar s i
-    decodeStrLitAux s i (acc.push c)
-  else
-    decodeStrLitAux s i (acc.push c)
+partial def decodeStrLitAux (s : String) (i : String.Pos) (acc : String) : Option String :=
+  OptionM.run do
+    let c := s.get i
+    let i := s.next i
+    if c == '\"' then
+      pure acc
+    else if s.atEnd i then
+      none
+    else if c == '\\' then do
+      let (c, i) ← decodeQuotedChar s i
+      decodeStrLitAux s i (acc.push c)
+    else
+      decodeStrLitAux s i (acc.push c)
 
 def decodeStrLit (s : String) : Option String :=
   decodeStrLitAux s 1 ""
@@ -545,38 +547,40 @@ def isStrLit? (stx : Syntax) : Option String :=
   | _        => none
 
 def decodeCharLit (s : String) : Option Char :=
-  let c := s.get 1
-  if c == '\\' then do
-    let (c, _) ← decodeQuotedChar s 2
-    pure c
-  else
-    pure c
+  OptionM.run do
+    let c := s.get 1
+    if c == '\\' then do
+      let (c, _) ← decodeQuotedChar s 2
+      pure c
+    else
+      pure c
 
 def isCharLit? (stx : Syntax) : Option Char :=
   match isLit? charLitKind stx with
   | some val => decodeCharLit val
   | _        => none
 
-private partial def decodeNameLitAux (s : String) (i : Nat) (r : Name) : Option Name := do
-  let continue? (i : Nat) (r : Name) : Option Name :=
-    if s.get i == '.' then
-       decodeNameLitAux s (s.next i) r
-    else if s.atEnd i then
-       pure r
+private partial def decodeNameLitAux (s : String) (i : Nat) (r : Name) : Option Name :=
+  OptionM.run do
+    let continue? (i : Nat) (r : Name) : OptionM Name :=
+      if s.get i == '.' then
+         decodeNameLitAux s (s.next i) r
+      else if s.atEnd i then
+         pure r
+      else
+         none
+    let curr := s.get i
+    if isIdBeginEscape curr then
+      let startPart := s.next i
+      let stopPart  := s.nextUntil isIdEndEscape startPart
+      if !isIdEndEscape (s.get stopPart) then none
+      else continue? (s.next stopPart) (Name.mkStr r (s.extract startPart stopPart))
+    else if isIdFirst curr then
+      let startPart := i
+      let stopPart  := s.nextWhile isIdRest startPart
+      continue? stopPart (Name.mkStr r (s.extract startPart stopPart))
     else
-       none
-  let curr := s.get i
-  if isIdBeginEscape curr then
-    let startPart := s.next i
-    let stopPart  := s.nextUntil isIdEndEscape startPart
-    if !isIdEndEscape (s.get stopPart) then none
-    else continue? (s.next stopPart) (Name.mkStr r (s.extract startPart stopPart))
-  else if isIdFirst curr then
-    let startPart := i
-    let stopPart  := s.nextWhile isIdRest startPart
-    continue? stopPart (Name.mkStr r (s.extract startPart stopPart))
-  else
-    none
+      none
 
 def decodeNameLit (s : String) : Option Name :=
   if s.get 0 == '`' then
@@ -791,16 +795,17 @@ abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α
 namespace Lean.Syntax
 
 private def decodeInterpStrQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) :=
-  match decodeQuotedChar s i with
-  | some r => some r
-  | none   =>
-    let c := s.get i
-    let i := s.next i
-    if c == '{' then pure ('{', i)
-    else none
+  OptionM.run do
+    match decodeQuotedChar s i with
+    | some r => some r
+    | none   =>
+      let c := s.get i
+      let i := s.next i
+      if c == '{' then pure ('{', i)
+      else none
 
 private partial def decodeInterpStrLit (s : String) : Option String :=
-  let rec loop (i : String.Pos) (acc : String) :=
+  let rec loop (i : String.Pos) (acc : String) : OptionM String :=
     let c := s.get i
     let i := s.next i
     if c == '\"' || c == '{' then
diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index ddd56a08c4..d3a5f0a6ec 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -45,7 +44,7 @@ def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
       let jsonFields := fields.map (Prod.snd ∘ mkJsonField)
       let fields := fields.map mkIdent
       let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:explicitBinder* (j : Json)
-        : Option $(← mkInductiveApp ctx.typeInfos[0] header.argNames) := do
+        : Option $(← mkInductiveApp ctx.typeInfos[0] header.argNames) := OptionM.run do
         $[let $fields:ident ← getObjValAs? j _ $jsonFields]*
         return { $[$fields:ident := $(id fields)]* })
       return #[cmd] ++ (← mkInstanceCmds ctx ``FromJson declNames)
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 93b195350f..4148889bd0 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -321,11 +321,11 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
           let contents := if contents.size == 1
             then contents[0]
             else mkNullNode contents
-          `(match ($(discrs).sequenceMap fun
-              | `($contents) => some $tuple
-              | _            => none) with
-            | some $resId => $yes
-            | none => $no)
+          `(match OptionM.run ($(discrs).sequenceMap fun
+                | `($contents) => some $tuple
+                | _            => none) with
+              | some $resId => $yes
+              | none => $no)
     }
     else if let some idx := quoted.getArgs.findIdx? (fun arg => isAntiquotSuffixSplice arg || isAntiquotSplice arg) then do
       /-