From 97ac23113821f2c8376f0d5a06febbbb4dc1f73c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 31 May 2021 16:37:18 -0700
Subject: [PATCH] feat: add missing `OptionT` instance

---
 src/Init/Control/Option.lean | 28 ++++++++++++++++------------
 1 file changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index f78636d030..7cde967b1c 100644
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@@ -21,47 +21,51 @@ def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
 namespace OptionT
 variable {m : Type u → Type v} [Monad m] {α β : Type u}
 
-@[inline] protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := id (α := m (Option β)) do
+protected def mk (x : m (Option α)) : OptionT m α :=
+  x
+
+@[inline] protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := OptionT.mk do
   match (← x) with
   | some a => f a
   | none   => pure none
 
-@[inline] protected def pure (a : α) : OptionT m α := id (α := m (Option α)) do
+@[inline] protected def pure (a : α) : OptionT m α := OptionT.mk do
   pure (some a)
 
-instance : Monad (OptionT m) := {
+instance : Monad (OptionT m) where
   pure := OptionT.pure
   bind := OptionT.bind
-}
 
-@[inline] protected def orElse (x : OptionT m α) (y : OptionT m α) : OptionT m α := id (α := m (Option α)) do
+@[inline] protected def orElse (x : OptionT m α) (y : OptionT m α) : OptionT m α := OptionT.mk do
   match (← x) with
   | some a => pure (some a)
   | _      => y
 
-@[inline] protected def fail : OptionT m α := id (α := m (Option α)) do
+@[inline] protected def fail : OptionT m α := OptionT.mk do
   pure none
 
-instance : Alternative (OptionT m) := {
+instance : Alternative (OptionT m) where
   failure := OptionT.fail
   orElse  := OptionT.orElse
-}
 
-@[inline] protected def lift (x : m α) : OptionT m α := id (α := m (Option α)) do
+@[inline] protected def lift (x : m α) : OptionT m α := OptionT.mk do
   return some (← x)
 
 instance : MonadLift m (OptionT m) := ⟨OptionT.lift⟩
 
 instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
 
-@[inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := id (α := m (Option α)) do
+@[inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := OptionT.mk do
   let some a ← x | handle ()
   pure a
 
-instance : MonadExceptOf Unit (OptionT m) := {
+instance : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
-}
+
+instance (ε : Type u) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
+  throw e           := OptionT.mk <| throwThe ε e
+  tryCatch x handle := OptionT.mk <| tryCatchThe ε x handle
 
 end OptionT