feat: solve typeclass subgoals in reverse order

Some instance arguments may still need to be reversed.

library/Init/Coe.lean

@@ -79,13 +79,13 @@ universes u₁ u₂ u₃
 
 /- Transitive closure for HasLift, HasCoe, HasCoeToFun -/
 
-instance liftTrans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasLift a b] [HasLiftT b c] : HasLiftT a c :=
+instance liftTrans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasLiftT b c] [HasLift a b] : HasLiftT a c :=
 ⟨fun x => liftT (lift x : b)⟩
 
 instance liftRefl {a : Sort u} : HasLiftT a a :=
 ⟨id⟩
 
-instance coeTrans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasCoe a b] [HasCoeT b c] : HasCoeT a c :=
+instance coeTrans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasCoeT b c] [HasCoe a b] : HasCoeT a c :=
 ⟨fun x => coeT (coeB x : b)⟩
 
 instance coeBase {a : Sort u} {b : Sort v} [HasCoe a b] : HasCoeT a b :=
@@ -116,17 +116,17 @@ instance coeOption {a : Type u} : HasCoeT a (Option a) :=
 class HasCoeTAux (a : Sort u) (b : Sort v) :=
 (coe : a → b)
 
-instance coeTransAux {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasCoe a b] [HasCoeTAux b c] : HasCoeTAux a c :=
+instance coeTransAux {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasCoeTAux b c] [HasCoe a b] : HasCoeTAux a c :=
 ⟨fun x => @HasCoeTAux.coe b c _ (coeB x)⟩
 
 instance coeBaseAux {a : Sort u} {b : Sort v} [HasCoe a b] : HasCoeTAux a b :=
 ⟨coeB⟩
 
-instance coeFnTrans {a : Sort u₁} {b : Sort u₂} [HasCoeTAux a b] [HasCoeToFun.{u₂, u₃} b] : HasCoeToFun.{u₁, u₃} a :=
+instance coeFnTrans {a : Sort u₁} {b : Sort u₂} [HasCoeToFun.{u₂, u₃} b] [HasCoeTAux a b] : HasCoeToFun.{u₁, u₃} a :=
 { F   := fun x => @HasCoeToFun.F.{u₂, u₃} b _ (@HasCoeTAux.coe a b _ x),
   coe := fun x => coeFn (@HasCoeTAux.coe a b _ x) }
 
-instance coeSortTrans {a : Sort u₁} {b : Sort u₂} [HasCoeTAux a b] [HasCoeToSort.{u₂, u₃} b] : HasCoeToSort.{u₁, u₃} a :=
+instance coeSortTrans {a : Sort u₁} {b : Sort u₂} [HasCoeToSort.{u₂, u₃} b] [HasCoeTAux a b] : HasCoeToSort.{u₁, u₃} a :=
 { S   := HasCoeToSort.S.{u₂, u₃} b,
   coe := fun x => coeSort (@HasCoeTAux.coe a b _ x) }
 
@@ -160,7 +160,7 @@ universes ua ua₁ ua₂ ub ub₁ ub₂
 
 /- Remark: we can't use [HasLiftT a₂ a₁] since it will produce non-termination whenever a type class resolution
    problem does not have a solution. -/
-instance liftFn {a₁ : Sort ua₁} {a₂ : Sort ua₂} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [HasLift a₂ a₁] [HasLiftT b₁ b₂] : HasLift (a₁ → b₁) (a₂ → b₂) :=
+instance liftFn {a₁ : Sort ua₁} {a₂ : Sort ua₂} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [HasLiftT b₁ b₂] [HasLift a₂ a₁] : HasLift (a₁ → b₁) (a₂ → b₂) :=
 ⟨fun f x => coe (f (coe x))⟩
 
 instance liftFnRange {a : Sort ua} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [HasLiftT b₁ b₂] : HasLift (a → b₁) (a → b₂) :=

library/Init/Control/Lift.lean

@@ -62,7 +62,7 @@ class MonadFunctorT (m m' : Type u → Type v) (n n' : Type u → Type w) :=
 
 export MonadFunctorT (monadMap)
 
-instance monadFunctorTTrans (m m' n n' o o') [MonadFunctor n n' o o'] [MonadFunctorT m m' n n'] :
+instance monadFunctorTTrans (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' β))⟩
 

library/Init/Control/State.lean

@@ -109,7 +109,7 @@ do s ← get; modify f; pure s
 
 -- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
 -- will be picked first
-instance monadStateTrans {n : Type u → Type w} [HasMonadLift m n] [MonadState σ m] : MonadState σ n :=
+instance monadStateTrans {n : Type u → Type w} [MonadState σ m] [HasMonadLift m n] : MonadState σ n :=
 { get := monadLift (MonadState.get : m _),
   set := fun st => monadLift (MonadState.set st : m _),
   modifyGet := fun α f => monadLift (MonadState.modifyGet f : m _) }
@@ -165,14 +165,14 @@ variables {σ σ' : Type u} {m m' : Type u → Type v}
 adaptState (fun st => (toSigma st, PUnit.unit)) (fun st _ => fromSigma st)
 export MonadStateAdapter (adaptState')
 
-instance monadStateAdapterTrans {n n' : Type u → Type v} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
+instance monadStateAdapterTrans {n n' : Type u → Type v} [MonadStateAdapter σ σ' m m'] [MonadFunctor m m' n n'] : MonadStateAdapter σ σ' n n' :=
 ⟨fun σ'' α split join => monadMap (fun α => (adaptState split join : m α → m' α))⟩
 
 instance [Monad m] : MonadStateAdapter σ σ' (StateT σ m) (StateT σ' m) :=
 ⟨fun σ'' α => StateT.adapt⟩
 end
 
-instance (σ : Type u) (m out : Type u → Type v) [Functor m] [MonadRun out m] : MonadRun (fun α => σ → out α) (StateT σ m) :=
+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) :=
@@ -182,7 +182,7 @@ export MonadStateRunner (runState)
 section
 variables {σ σ' : Type u} {m m' : Type u → Type u}
 
-instance monadStateRunnerTrans {n n' : Type u → Type u} [MonadFunctor m m' n n'] [MonadStateRunner σ m m'] : MonadStateRunner σ n n' :=
+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 :=

src/library/type_context.cpp

@@ -3458,10 +3458,8 @@ struct instance_synthesizer {
             r = locals.mk_lambda(r);
             m_ctx.assign(mvar, r);
             // copy new_inst_mvars to stack
-            unsigned i = new_inst_mvars.size();
-            while (i > 0) {
-                --i;
-                m_state.m_stack = cons(stack_entry(new_inst_mvars[i], e.m_depth+1), m_state.m_stack);
+            for (expr const & new_inst_mvar : new_inst_mvars) {
+                m_state.m_stack = cons(stack_entry(new_inst_mvar, e.m_depth+1), m_state.m_stack);
             }
             return true;
         } catch (exception & ex) {

tests/lean/run/coroutine.lean

@@ -139,7 +139,7 @@ instance (α : Type u) (δ : Type v) : monadCoroutine α δ (coroutine α δ) :=
 { yield  := coroutine.yield }
 
 instance monadCoroutineTrans (α : Type u) (δ : Type v) (m : Type w → Type r) (n : Type w → Type s)
-                               [HasMonadLift m n] [monadCoroutine α δ m] : monadCoroutine α δ n :=
+                               [monadCoroutine α δ m] [HasMonadLift m n] : monadCoroutine α δ n :=
 { yield := fun d => monadLift (monadCoroutine.yield d : m _) }
 
 export monadCoroutine (yield)