refactor: remove MonadRun

src/Init/Control.lean

@@ -10,7 +10,6 @@ import Init.Control.Alternative
 import Init.Control.Monad
 import Init.Control.MonadLift
 import Init.Control.MonadFunctor
-import Init.Control.MonadRun
 import Init.Control.MonadControl
 import Init.Control.State
 import Init.Control.StateRef

src/Init/Control/Except.lean

@@ -11,7 +11,6 @@ import Init.Control.Alternative
 import Init.Control.MonadControl
 import Init.Control.Id
 import Init.Control.MonadFunctor
-import Init.Control.MonadRun
 
 universes u v w u'
 
@@ -200,9 +199,6 @@ instance [Monad m] : MonadExceptAdapter ε ε' (ExceptT ε m) (ExceptT ε' m) :=
 ⟨fun α => ExceptT.adapt⟩
 end
 
-instance (ε m out) [MonadRun out m] : MonadRun (fun α => out (Except ε α)) (ExceptT ε m) :=
-⟨fun α => run⟩
-
 @[inline] def observing {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) : m (Except ε α) :=
 catch (do a ← x; pure (Except.ok a)) (fun ex => pure (Except.error ex))
 

src/Init/Control/Id.lean

@@ -7,7 +7,6 @@ The identity Monad.
 -/
 prelude
 import Init.Control.MonadLift
-import Init.Control.MonadRun
 
 universe u
 
@@ -36,7 +35,4 @@ x
 instance {α} [HasOfNat α] : HasOfNat (Id α) :=
 inferInstanceAs (HasOfNat α)
 
-instance : MonadRun id Id :=
-⟨@Id.run⟩
-
 end Id

src/Init/Control/MonadRun.lean

@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich, Leonardo de Moura
--/
-prelude
-import Init.Control.MonadLift
-
-universes u v
-
-/-- Run a Monad stack to completion.
-    `run` should be the composition of the transformers' individual `run` functions.
-    This class mostly saves some typing when using highly nested Monad stacks:
-    ```
-    @[reducible] def MyMonad := ReaderT myCfg $ StateT myState $ ExceptT myErr id
-    -- def MyMonad.run {α : Type} (x : MyMonad α) (cfg : myCfg) (st : myState) := ((x.run cfg).run st).run
-    def MyMonad.run {α : Type} (x : MyMonad α) := MonadRun.run x
-    ```
-    -/
-class MonadRun (out : outParam $ Type u → Type v) (m : Type u → Type v) :=
-(run {α : Type u} : m α → out α)
-
-export MonadRun (run)

src/Init/Control/Option.lean

@@ -66,6 +66,4 @@ namespace OptionT
   instance : MonadExceptOf Unit (OptionT m) :=
   { throw := fun _ _ => OptionT.fail, catch := @OptionT.catch _ _ }
 
-  instance (m out) [MonadRun out m] : MonadRun (fun α => out (Option α)) (OptionT m) :=
-  ⟨fun α => MonadRun.run⟩
 end OptionT

src/Init/Control/Reader.lean

@@ -147,23 +147,6 @@ instance [Monad m] : MonadReaderAdapterOf ρ ρ' (ReaderT ρ m) (ReaderT ρ' m)
 ⟨fun α => ReaderT.adapt⟩
 end
 
-instance (ρ : Type u) (m out) [MonadRun out m] : MonadRun (fun α => ρ → out α) (ReaderT ρ m) :=
-⟨fun α x => run ∘ x⟩
-
-class MonadReaderRunner (ρ : Type u) (m m' : Type u → Type u) :=
-(runReader {α : Type u} : m α → ρ → m' α)
-export MonadReaderRunner (runReader)
-
-section
-variables {ρ ρ' : Type u} {m m' : Type u → Type u}
-
-instance monadReaderRunnerTrans {n n' : Type u → Type u} [MonadReaderRunner ρ m m'] [MonadFunctor m m' n n'] : MonadReaderRunner ρ n n' :=
-⟨fun α x r => monadMap (fun (α) (y : m α) => (runReader y r : m' α)) x⟩
-
-instance ReaderT.MonadStateRunner [Monad m] : MonadReaderRunner ρ (ReaderT ρ m) m :=
-⟨fun α x r => x r⟩
-end
-
 instance ReaderT.monadControl (ρ : Type u) (m : Type u → Type v) : MonadControl m (ReaderT ρ m) := {
   stM      := fun α       => α,
   liftWith := fun α f ctx => f fun β x => x ctx,

src/Init/Control/State.lean

@@ -199,23 +199,6 @@ instance [Monad m] : MonadStateAdapter σ σ' (StateT σ m) (StateT σ' m) :=
 ⟨fun σ'' α => StateT.adapt⟩
 end
 
-instance (σ : Type u) (m out : Type u → Type v) [MonadRun out m] [Functor m] : MonadRun (fun α => σ → out α) (StateT σ m) :=
-⟨fun α x => run ∘ StateT.run' x⟩
-
-class MonadStateRunner (σ : Type u) (m m' : Type u → Type u) :=
-(runState {α : Type u} : m α → σ → m' α)
-export MonadStateRunner (runState)
-
-section
-variables {σ σ' : Type u} {m m' : Type u → Type u}
-
-instance monadStateRunnerTrans {n n' : Type u → Type u} [MonadStateRunner σ m m'] [MonadFunctor m m' n n'] : MonadStateRunner σ n n' :=
-⟨fun α x s => monadMap (fun (α) (y : m α) => (runState y s : m' α)) x⟩
-
-instance StateT.MonadStateRunner [Monad m] : MonadStateRunner σ (StateT σ m) m :=
-⟨fun α x s => Prod.fst <$> x s⟩
-end
-
 instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (StateT σ m) := {
   stM      := fun α   => α × σ,
   liftWith := fun α f => do s ← get; liftM (f (fun β x => x.run s)),

src/Lean/Hygiene.lean

@@ -31,7 +31,7 @@ instance : MonadQuotation Unhygienic := {
     let fresh ← modifyGet fun n => (n, n + 1)
     withReader (fun _ => fresh) x
 }
-protected def run {α : Type} (x : Unhygienic α) : α := run x firstFrontendMacroScope (firstFrontendMacroScope+1)
+protected def run {α : Type} (x : Unhygienic α) : α := (x firstFrontendMacroScope).run' (firstFrontendMacroScope+1)
 end Unhygienic
 
 private def mkInaccessibleUserNameAux (unicode : Bool) (name : Name) (idx : Nat) : Name :=

tests/lean/repr_issue.lean

@@ -13,5 +13,5 @@ foo
 
 -- The following examples were producing an element of Type `id (Except String Nat)`.
 -- Type class resolution was failing to produce an instance for `HasRepr (id (Except String Nat))` because `id` is not transparent.
-#eval run ex₁ (mkArray 10 1000)
-#eval run ex₂ (mkArray 10 1000)
+#eval ex₁.run' (mkArray 10 1000) $.run
+#eval ex₂.run' (mkArray 10 1000) $.run