From c7762d07c13c35f17c6f6d74973c2bc246d79c8d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Jul 2018 15:52:47 -0700
Subject: [PATCH] feat(library/init/control/lift): add comment

---
 library/init/control/lift.lean | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/library/init/control/lift.lean b/library/init/control/lift.lean
index bc9d17baac..41440aa41a 100644
--- a/library/init/control/lift.lean
+++ b/library/init/control/lift.lean
@@ -46,27 +46,30 @@ instance has_monad_lift_t_refl (m) : has_monad_lift_t m m :=
 /-- A functor in the control 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). -/
+    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
+    gadgets such as `monad_state_adapter` and `monad_reader_adapter`. -/
 class monad_functor (m m' : Type u → Type v) (n n' : Type u → Type w) :=
-(monad_map {} {α : Type u} : (∀ {α}, m α → m' α) → n α → n' α)
+(monad_map {} {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
 
 /-- The reflexive-transitive closure of `monad_functor`.
     `monad_map` is used to transitively lift monad morphisms such as `state_t.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 monad_functor_t (m m' : Type u → Type v) (n n' : Type u → Type w) :=
-(monad_map {} {α : Type u} : (∀ {α}, m α → m' α) → n α → n' α)
+(monad_map {} {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
 
 export monad_functor_t (monad_map)
 
 instance monad_functor_t_trans (m m' n n' o o') [monad_functor n n' o o'] [monad_functor_t m m' n n'] :
   monad_functor_t m m' o o' :=
-⟨λ α f, monad_functor.monad_map (λ α, (monad_map @f : n α → n' α))⟩
+⟨λ α f, monad_functor.monad_map (λ β, (monad_map @f : n β → n' β))⟩
 
 instance monad_functor_t_refl (m m') : monad_functor_t m m' m m' :=
 ⟨λ α f, f⟩
 
-@[simp] lemma monad_map_refl {m m' : Type u → Type v} (f : ∀ {α}, m α → m' α) {α} : (monad_map @f : m α → m' α) = f := rfl
-
+@[simp] lemma monad_map_refl {m m' : Type u → Type v} (f : ∀ {β}, m β → m' β) {α} : (monad_map @f : m α → m' α) = f := rfl
 
 /-- Run a monad stack to completion.
     `run` should be the composition of the transformers' individual `run` functions.