diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index ca45e9b4db..a551c061bc 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -63,19 +63,19 @@ abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
 abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α β] : β :=
   CoeSort.coe a
 
-instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeTC α β] [Coe β δ] : CoeTC α δ where
+instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [Coe β δ] [CoeTC α β] : CoeTC α δ where
   coe a := coeB (coeTC a : β)
 
 instance coeBase {α : Sort u} {β : Sort v} [Coe α β] : CoeTC α β where
   coe a := coeB a
 
-instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeTC β δ] [CoeTail δ γ] [CoeHead α β] : CoeT α a γ where
+instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeHead α β] [CoeTail δ γ] [CoeTC β δ] : CoeT α a γ where
   coe := coeTail (coeTC (coeHead a : β) : δ)
 
-instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC β δ] [CoeHead α β] : CoeT α a δ  where
+instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeHead α β] [CoeTC β δ] : CoeT α a δ  where
   coe := coeTC (coeHead a : β)
 
-instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α β] [CoeTail β δ] : CoeT α a δ where
+instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTail β δ] [CoeTC α β] : CoeT α a δ where
   coe := coeTail (coeTC a : β)
 
 instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT α a β where
@@ -116,7 +116,7 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α wh
   Remark: one may question why we use `OfNat α` instead of `Coe Nat α`.
   Reason: `OfNat` is for implementing polymorphic numeric literals, and we may
   want to have numberic literals for a type α and **no** coercion from `Nat` to `α`. -/
-instance hasOfNatOfCoe [OfNat α n] [Coe α β] : OfNat β n where
+instance hasOfNatOfCoe [Coe α β] [OfNat α n] : OfNat β n where
   ofNat := coe (OfNat.ofNat n : α)
 
 @[inline] def liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 7f3d120303..b242bbd8df 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -86,7 +86,7 @@ class MonadControlT (m : Type u → Type v) (n : Type u → Type w) where
 
 export MonadControlT (stM liftWith restoreM)
 
-instance (m n o) [MonadControlT m n] [MonadControl n o] : MonadControlT m o where
+instance (m n o) [MonadControl n o] [MonadControlT m n] : MonadControlT m o where
   stM α := stM m n (MonadControl.stM n o α)
   liftWith f := MonadControl.liftWith fun x₂ => liftWith fun x₁ => f (x₁ ∘ x₂)
   restoreM := MonadControl.restoreM ∘ restoreM
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index 0a5e94a006..db60187815 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -18,7 +18,7 @@ namespace ReaderT
 @[inline] protected def failure [Alternative m] : ReaderT ρ m α :=
   fun s => failure
 
-instance [Monad m] [Alternative m] : Alternative (ReaderT ρ m) where
+instance [Alternative m] [Monad m] : Alternative (ReaderT ρ m) where
   failure := ReaderT.failure
   orElse  := ReaderT.orElse
 
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index d07970a6ca..88290d500b 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -135,7 +135,7 @@ def mkFreshId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m Name := d
   setNGen ngen.next
   pure r
 
-instance monadNameGeneratorLift (m n : Type → Type) [MonadNameGenerator m] [MonadLift m n] : MonadNameGenerator n := {
+instance monadNameGeneratorLift (m n : Type → Type) [MonadLift m n] [MonadNameGenerator m] : MonadNameGenerator n := {
   getNGen := liftM (getNGen : m _),
   setNGen := fun ngen => liftM (setNGen ngen : m _)
 }
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index fbcb598ac9..76354368af 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1176,7 +1176,7 @@ export MonadLiftT (monadLift)
 
 abbrev liftM := @monadLift
 
-instance (m n o) [MonadLiftT m n] [MonadLift n o] : MonadLiftT m o where
+instance (m n o) [MonadLift n o] [MonadLiftT m n] : MonadLiftT m o where
   monadLift x := MonadLift.monadLift (m := n) (monadLift x)
 
 instance (m) : MonadLiftT m m where
@@ -1196,7 +1196,7 @@ class MonadFunctorT (m : Type u → Type v) (n : Type u → Type w) where
 
 export MonadFunctorT (monadMap)
 
-instance (m n o) [MonadFunctorT m n] [MonadFunctor n o] : MonadFunctorT m o where
+instance (m n o) [MonadFunctor n o] [MonadFunctorT m n] : MonadFunctorT m o where
   monadMap f := MonadFunctor.monadMap (m := n) (monadMap (m := m) f)
 
 instance monadFunctorRefl (m) : MonadFunctorT m m where
@@ -1324,7 +1324,7 @@ export MonadReader (read)
 instance (ρ : Type u) (m : Type u → Type v) [MonadReaderOf ρ m] : MonadReader ρ m where
   read := readThe ρ
 
-instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadReaderOf ρ m] [MonadLift m n] : MonadReaderOf ρ n where
+instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [MonadReaderOf ρ m] : MonadReaderOf ρ n where
   read := liftM (m := m) read
 
 instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (ReaderT ρ m) where
@@ -1344,7 +1344,7 @@ export MonadWithReader (withReader)
 instance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadWithReader ρ m where
   withReader := withTheReader ρ
 
-instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [MonadWithReaderOf ρ m] [MonadFunctor m n] : MonadWithReaderOf ρ n where
+instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [MonadFunctor m n] [MonadWithReaderOf ρ m] : MonadWithReaderOf ρ n where
   withReader f := monadMap (m := m) (withTheReader ρ f)
 
 instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) where
@@ -1396,7 +1396,7 @@ instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState
 
 -- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
 -- will be picked first
-instance {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadStateOf σ m] [MonadLift m n] : MonadStateOf σ n where
+instance {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [MonadStateOf σ m] : MonadStateOf σ n where
   get       := liftM (m := m) MonadStateOf.get
   set       := fun s => liftM (m := m) (MonadStateOf.set s)
   modifyGet := fun f => monadLift (m := m) (MonadState.modifyGet f)
@@ -1742,7 +1742,7 @@ class MonadRef (m : Type → Type) where
 
 export MonadRef (getRef)
 
-instance (m n : Type → Type) [MonadRef m] [MonadFunctor m n] [MonadLift m n] : MonadRef n where
+instance (m n : Type → Type) [MonadLift m n] [MonadFunctor m n] [MonadRef m] : MonadRef n where
   getRef  := liftM (getRef : m _)
   withRef := fun ref x => monadMap (m := m) (MonadRef.withRef ref) x
 
@@ -1786,7 +1786,7 @@ export MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)
 def MonadRef.mkInfoFromRefPos [Monad m] [MonadRef m] : m SourceInfo := do
   return { pos := (← getRef).getPos }
 
-instance {m n : Type → Type} [MonadQuotation m] [MonadLift m n] [MonadFunctor m n] : MonadQuotation n where
+instance {m n : Type → Type} [MonadFunctor m n] [MonadLift m n] [MonadQuotation m] : MonadQuotation n where
   getCurrMacroScope   := liftM (m := m) getCurrMacroScope
   getMainModule       := liftM (m := m) getMainModule
   withFreshMacroScope := monadMap (m := m) withFreshMacroScope
diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean
index 2e57269872..cad11f39bf 100644
--- a/src/Init/System/ST.lean
+++ b/src/Init/System/ST.lean
@@ -19,7 +19,7 @@ instance (σ : Type) : Monad (ST σ) := inferInstanceAs (Monad (EST _ _))
 -- Auxiliary class for inferring the "state" of `EST` and `ST` monads
 class STWorld (σ : outParam Type) (m : Type → Type)
 
-instance {σ m n} [STWorld σ m] [MonadLift m n] : STWorld σ n := ⟨⟩
+instance {σ m n} [MonadLift m n] [STWorld σ m] : STWorld σ n := ⟨⟩
 instance {ε σ} : STWorld σ (EST ε σ) := ⟨⟩
 
 @[noinline, nospecialize]
diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean
index f7461215b2..59342b335e 100644
--- a/src/Lean/Data/Options.lean
+++ b/src/Lean/Data/Options.lean
@@ -102,8 +102,8 @@ class MonadOptions (m : Type → Type) where
 
 export MonadOptions (getOptions)
 
-instance (m n) [MonadOptions m] [MonadLift m n] : MonadOptions n :=
-  { getOptions := liftM (getOptions : m _) }
+instance (m n) [MonadLift m n] [MonadOptions m] : MonadOptions n where
+  getOptions := liftM (getOptions : m _)
 
 variables {m} [Monad m] [MonadOptions m]
 
diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index da26b37f60..573f91d26e 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -74,7 +74,7 @@ class MonadInfoTree (m : Type → Type)  where
 
 export MonadInfoTree (getInfoState modifyInfoState)
 
-instance (m n) [MonadInfoTree m] [MonadLift m n] : MonadInfoTree n where
+instance (m n) [MonadLift m n] [MonadInfoTree m] : MonadInfoTree n where
   getInfoState      := liftM (getInfoState : m _)
   modifyInfoState f := liftM (modifyInfoState f : m _)
 
diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean
index 5a3288bc58..22345f1dd0 100644
--- a/src/Lean/Elab/Log.lean
+++ b/src/Lean/Elab/Log.lean
@@ -21,12 +21,11 @@ class MonadLog (m : Type → Type) extends MonadFileMap m where
 
 export MonadLog (getFileName logMessage)
 
-instance (m n) [MonadLog m] [MonadLift m n] : MonadLog n := {
-  getRef      := liftM (MonadLog.getRef : m _),
-  getFileMap  := liftM (getFileMap : m _),
-  getFileName := liftM (getFileName : m _),
+instance (m n) [MonadLift m n] [MonadLog m] : MonadLog n where
+  getRef      := liftM (MonadLog.getRef : m _)
+  getFileMap  := liftM (getFileMap : m _)
+  getFileName := liftM (getFileName : m _)
   logMessage  := fun msg => liftM (logMessage msg : m _ )
-}
 
 variables {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m]
 
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 6994b63425..f1e48ed229 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -141,7 +141,7 @@ class MonadMacroAdapter (m : Type → Type) where
   getNextMacroScope                  : m MacroScope
   setNextMacroScope                  : MacroScope → m Unit
 
-instance (m n) [MonadMacroAdapter m] [MonadLift m n] : MonadMacroAdapter n := {
+instance (m n) [MonadLift m n] [MonadMacroAdapter m] : MonadMacroAdapter n := {
   getCurrMacroScope := liftM (MonadMacroAdapter.getCurrMacroScope : m _),
   getNextMacroScope := liftM (MonadMacroAdapter.getNextMacroScope : m _),
   setNextMacroScope := fun s => liftM (MonadMacroAdapter.setNextMacroScope s : m _)
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 2997d4ffa2..9fa22fc296 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -703,9 +703,8 @@ class MonadEnv (m : Type → Type) where
 
 export MonadEnv (getEnv modifyEnv)
 
-instance (m n) [MonadEnv m] [MonadLift m n] : MonadEnv n := {
-  getEnv    := liftM (getEnv : m Environment),
+instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
+  getEnv    := liftM (getEnv : m Environment)
   modifyEnv := fun f => liftM (modifyEnv f : m Unit)
-}
 
 end Lean
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 5f8b43f8df..a3fa426360 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -383,7 +383,7 @@ class MonadLCtx (m : Type → Type) where
 
 export MonadLCtx (getLCtx)
 
-instance (m n) [MonadLCtx m] [MonadLift m n] : MonadLCtx n where
+instance (m n) [MonadLift m n] [MonadLCtx m] : MonadLCtx n where
   getLCtx := liftM (getLCtx : m _)
 
 def replaceFVarIdAtLocalDecl (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 5190505f0c..b970181955 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -215,8 +215,8 @@ class AddMessageContext (m : Type → Type) where
 
 export AddMessageContext (addMessageContext)
 
-instance (m n) [AddMessageContext m] [MonadLift m n] : AddMessageContext n :=
-  { addMessageContext := fun msg => liftM (addMessageContext msg : m _) }
+instance (m n) [MonadLift m n] [AddMessageContext m] : AddMessageContext n where
+  addMessageContext := fun msg => liftM (addMessageContext msg : m _)
 
 def addMessageContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
   let env ← getEnv
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 01980ccf57..5ae7d7a634 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -290,7 +290,7 @@ class MonadMCtx (m : Type → Type) where
 
 export MonadMCtx (getMCtx modifyMCtx)
 
-instance (m n) [MonadMCtx m] [MonadLift m n] : MonadMCtx n where
+instance (m n) [MonadLift m n] [MonadMCtx m] : MonadMCtx n where
   getMCtx    := liftM (getMCtx : m _)
   modifyMCtx := fun f => liftM (modifyMCtx f : m _)
 
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index f9b2ace28a..9528d53b9e 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -151,7 +151,7 @@ class MonadResolveName (m : Type → Type) where
 
 export MonadResolveName (getCurrNamespace getOpenDecls)
 
-instance (m n) [MonadResolveName m] [MonadLift m n] : MonadResolveName n where
+instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where
   getCurrNamespace := liftM (m:=m) getCurrNamespace
   getOpenDecls     := liftM (m:=m) getOpenDecls
 
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index b294c5bfb4..a34d0d9832 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -38,9 +38,9 @@ class MonadTrace (m : Type → Type) where
 
 export MonadTrace (getTraceState modifyTraceState)
 
-instance (m n) [MonadTrace m] [MonadLift m n] : MonadTrace n :=
-  { modifyTraceState := fun f => liftM (modifyTraceState f : m _),
-    getTraceState    := liftM (getTraceState : m _) }
+instance (m n) [MonadLift m n] [MonadTrace m] : MonadTrace n where
+  modifyTraceState := fun f => liftM (modifyTraceState f : m _)
+  getTraceState    := liftM (getTraceState : m _)
 
 variables {α : Type} {m : Type → Type} [Monad m] [MonadTrace m]