From 719819bf496c5b1d5494af0661c19bd932439eba Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 9 Jul 2020 16:58:38 +0200
Subject: [PATCH] fix: finally shouldn't call `finalizer` when `finalizer`
 throws

---
 src/Init/Control/Except.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 117492c987..9f39bc2597 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -181,7 +181,8 @@ instance (ε m out) [MonadRun out m] : MonadRun (fun α => out (Except ε α)) (
 ⟨fun α => run⟩
 
 /-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
-@[inline] def finally {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) (finalizer : m PUnit) : m α :=
-catch
-  (do a ← x; finalizer; pure a)
-  (fun e => do finalizer; throw e)
+@[inline] def finally {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) (finalizer : m PUnit) : m α := do
+r ← catch (Except.ok <$> x) (fun ex => @pure m _ _ $ Except.error ex);
+match r with
+| Except.ok a => finalizer *> pure a
+| Except.error e => finalizer *> throw e