refactor: simplify MonadFunctor

src/Init/Control/Except.lean

@@ -118,7 +118,7 @@ ExceptT.mk $ ma >>= fun res => match res with
  | Except.ok a    => pure (Except.ok a)
  | Except.error e => (handle e)
 
-instance (m') [Monad m'] : MonadFunctor m m' (ExceptT ε m) (ExceptT ε m') :=
+instance : MonadFunctor m (ExceptT ε m) :=
 ⟨fun _ f x => f x⟩
 
 instance : Monad (ExceptT ε m) :=

src/Init/Control/MonadFunctor.lean

@@ -11,25 +11,20 @@ universes u v w
 /-- A functor in the category of monads. Can be used to lift monad-transforming functions.
     Based on pipes' [MFunctor](https://hackage.haskell.org/package/pipes-2.4.0/docs/Control-MFunctor.html),
     but not restricted to monad transformers.
-    Alternatively, an implementation of [MonadTransFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadTransFunctor).
-
-
-    Remark: other libraries equate `m` and `m'`, and `n` and `n'`. We need to distinguish them to be able to implement
-    ogadgets such as `MonadStateAdapter` and `MonadReaderAdapter`. -/
-class MonadFunctor (m m' : Type u → Type v) (n n' : Type u → Type w) :=
-(monadMap {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
+    Alternatively, an implementation of [MonadTransFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadTransFunctor). -/
+class MonadFunctor (m : Type u → Type v) (n : Type u → Type w) :=
+(monadMap {α : Type u} : (∀ {β}, m β → m β) → n α → n α)
 
 /-- The reflexive-transitive closure of `MonadFunctor`.
     `monadMap` is used to transitively lift Monad morphisms such as `StateT.zoom`.
     A generalization of [MonadLiftFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadLiftFunctor), which can only lift endomorphisms (i.e. m = m', n = n'). -/
-class MonadFunctorT (m m' : Type u → Type v) (n n' : Type u → Type w) :=
-(monadMap {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
+class MonadFunctorT (m : Type u → Type v) (n : Type u → Type w) :=
+(monadMap {α : Type u} : (∀ {β}, m β → m β) → n α → n α)
 
 export MonadFunctorT (monadMap)
 
-instance monadFunctorTrans (m m' n n' o o') [MonadFunctorT m m' n n'] [MonadFunctor n n' o o'] :
-  MonadFunctorT m m' o o' :=
-⟨fun α f => MonadFunctor.monadMap (fun β => (monadMap @f : n β → n' β))⟩
+instance monadFunctorTrans (m n o) [MonadFunctorT m n] [MonadFunctor n o] : MonadFunctorT m o :=
+⟨fun α f => MonadFunctor.monadMap (fun β => (monadMap @f : n β → n β))⟩
 
-instance monadFunctorRefl (m m') : MonadFunctorT m m' m m' :=
+instance monadFunctorRefl (m) : MonadFunctorT m m :=
 ⟨fun α f => f⟩

src/Init/Control/Option.lean

@@ -56,7 +56,7 @@ namespace OptionT
   @[inline] protected def monadMap {m'} [Monad m'] {α} (f : ∀ {α}, m α → m' α) : OptionT m α → OptionT m' α :=
   fun x => f x
 
-  instance (m') [Monad m'] : MonadFunctor m m' (OptionT m) (OptionT m') :=
+  instance : MonadFunctor m (OptionT m) :=
   ⟨fun α => OptionT.monadMap⟩
 
   @[inline] protected def catch (ma : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α :=

src/Init/Control/Reader.lean

@@ -66,7 +66,7 @@ fun r => f <$> x r
 instance : Monad (ReaderT ρ m) :=
 { pure := @ReaderT.pure _ _ _, bind := @ReaderT.bind _ _ _, map := @ReaderT.map _ _ _ }
 
-instance (ρ m m') [Monad m] [Monad m'] : MonadFunctor m m' (ReaderT ρ m) (ReaderT ρ m') :=
+instance (ρ m) [Monad m] : MonadFunctor m (ReaderT ρ m) :=
 ⟨fun _ f x r => f (x r)⟩
 
 @[inline] protected def adapt {ρ' : Type u} [Monad m] {α : Type u} (f : ρ' → ρ) : ReaderT ρ m α → ReaderT ρ' m α :=
@@ -138,7 +138,7 @@ instance MonadWithReaderOf.isMonadWithReader (ρ : Type u) (m : Type u → Type
 section
 variables {ρ : Type u} {m : Type u → Type v}
 
-instance monadWithReaderOfTrans {n : Type u → Type v} [MonadWithReaderOf ρ m] [MonadFunctor m m n n] : MonadWithReaderOf ρ n :=
+instance monadWithReaderOfTrans {n : Type u → Type v} [MonadWithReaderOf ρ m] [MonadFunctor m n] : MonadWithReaderOf ρ n :=
 ⟨fun α f => monadMap fun β => (withTheReader ρ f : m β → m β)⟩
 
 instance ReaderT.monadWithReaderOf [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) :=

src/Init/Control/State.lean

@@ -70,7 +70,7 @@ fun s => do a ← t; pure (a, s)
 instance : MonadLift m (StateT σ m) :=
 ⟨@StateT.lift σ m _⟩
 
-instance (σ m m') [Monad m] [Monad m'] : MonadFunctor m m' (StateT σ m) (StateT σ m') :=
+instance (σ m) [Monad m] : MonadFunctor m (StateT σ m) :=
 ⟨fun _ f x s => f (x s)⟩
 
 @[inline] protected def adapt {σ σ' σ'' α : Type u} {m : Type u → Type v} [Monad m] (split : σ → σ' × σ'')

src/Init/Control/StateRef.lean

@@ -32,8 +32,8 @@ fun _ => x
 instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
 instance : MonadLift m (StateRefT' ω σ m) := ⟨fun _ => StateRefT'.lift⟩
 instance [Monad m] [MonadIO m] : MonadIO (StateRefT' ω σ m) := inferInstanceAs (MonadIO (ReaderT _ _))
-instance (σ m m') [Monad m] [Monad m'] : MonadFunctor m m' (StateRefT' ω σ m) (StateRefT' ω σ m') :=
-inferInstanceAs (MonadFunctor m m' (ReaderT _ _) (ReaderT _ _))
+instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) :=
+inferInstanceAs (MonadFunctor m (ReaderT _ _))
 
 @[inline] protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
 fun ref => ref.get

src/Init/LeanInit.lean

@@ -474,7 +474,7 @@ instance : MonadQuotation MacroM := {
   withFreshMacroScope := Macro.withFreshMacroScope
 }
 
-instance {m n : Type → Type} [MonadQuotation m] [MonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n := {
+instance {m n : Type → Type} [MonadQuotation m] [MonadLift m n] [MonadFunctorT m n] : MonadQuotation n := {
   getCurrMacroScope   := liftM (m := m) getCurrMacroScope,
   getMainModule       := liftM (m := m) getMainModule,
   withFreshMacroScope := monadMap (m := m) withFreshMacroScope

src/Lean/Exception.lean

@@ -31,7 +31,7 @@ class Ref (m : Type → Type) :=
 
 export Ref (getRef)
 
-instance (m n : Type → Type) [Ref m] [MonadFunctor m m n n] [MonadLift m n] : Ref n := {
+instance (m n : Type → Type) [Ref m] [MonadFunctor m n] [MonadLift m n] : Ref n := {
   getRef  := liftM (getRef : m _),
   withRef := fun ref x => monadMap (m := m) (Ref.withRef ref) x
 }