feat: set priority in monadic class instances

doc/examples/widgets.lean

@@ -141,7 +141,7 @@ def getType (params : GetTypeParams) : RequestM (RequestTask CodeWithInfos) :=
     runTermElabM snap do
       let name ← resolveGlobalConstNoOverloadCore params.name
       let c ← try getConstInfo name
-        catch _ => throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩
+        catch _ : Exception => throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩
       Widget.ppExprTagged c.type
 
 /-!

src/Init/Control/Except.lean

@@ -136,7 +136,7 @@ instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [MonadExceptO
   tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle
 
 @[always_inline]
-instance (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) where
+instance (priority := high) (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) where
   throw e := ExceptT.mk <| pure (Except.error e)
   tryCatch := ExceptT.tryCatch
 

src/Init/Control/ExceptCps.lean

@@ -36,7 +36,7 @@ instance : Monad (ExceptCpsT ε m) where
 instance : LawfulMonad (ExceptCpsT σ m) := by
   refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
 
-instance : MonadExceptOf ε (ExceptCpsT ε m) where
+instance (priority := high) : MonadExceptOf ε (ExceptCpsT ε m) where
   throw e  := fun _ _ k => k e
   tryCatch x handle := fun _ k₁ k₂ => x _ k₁ (fun e => handle e _ k₁ k₂)
 

src/Init/Control/Option.lean

@@ -63,7 +63,7 @@ instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
   let some a ← x | handle ()
   pure a
 
-instance : MonadExceptOf Unit (OptionT m) where
+instance (priority := low) : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 

src/Init/Control/State.lean

@@ -113,7 +113,7 @@ def ForM.forIn [Monad m] [ForM (StateT β (ExceptT β m)) ρ α]
 section
 variable {σ : Type u} {m : Type u → Type v}
 
-instance [Monad m] : MonadStateOf σ (StateT σ m) where
+instance (priority := high) [Monad m] : MonadStateOf σ (StateT σ m) where
   get       := StateT.get
   set       := StateT.set
   modifyGet := StateT.modifyGet

src/Init/Prelude.lean

@@ -2997,7 +2997,8 @@ variable {ε : Type u} {m : Type v → Type w}
 @[inline] protected def orElse [MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : Unit → m α) : m α :=
   tryCatch t₁ fun _ => t₂ ()
 
-instance [MonadExcept ε m] {α : Type v} : OrElse (m α) where
+/- (priority := low) -/
+instance (priority := 100) [MonadExcept ε m] {α : Type v} : OrElse (m α) where
   orElse := MonadExcept.orElse
 
 end MonadExcept
@@ -3027,7 +3028,7 @@ namespace ReaderT
 section
 variable {ρ : Type u} {m : Type u → Type v} {α : Type u}
 
-instance  : MonadLift m (ReaderT ρ m) where
+instance : MonadLift m (ReaderT ρ m) where
   monadLift x := fun _ => x
 
 @[always_inline]
@@ -3123,7 +3124,8 @@ instance (ρ : Type u) (m : Type u → Type v) [MonadReaderOf ρ m] : MonadReade
 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
+/- (priority := high) -/
+instance (priority := 10000) {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (ReaderT ρ m) where
   read := ReaderT.read
 
 /--
@@ -3160,7 +3162,8 @@ instance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadW
 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} : MonadWithReaderOf ρ (ReaderT ρ m) where
+/- (priority := high) -/
+instance (priority := 10000) {ρ : Type u} {m : Type u → Type v} : MonadWithReaderOf ρ (ReaderT ρ m) where
   withReader f x := fun ctx => x (f ctx)
 
 /--
@@ -3246,8 +3249,6 @@ of the state. It is equivalent to `get <* modify f` but may be more efficient.
 def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m σ :=
   modifyGet fun s => (s, f s)
 
--- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
--- will be picked first
 @[always_inline]
 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

src/Lean/Elab/Match.lean

@@ -165,7 +165,7 @@ open Lean.Elab.Term.Quotation in
     for (pats, rhs) in patss.zip rhss do
       let vars ← try
         getPatternsVars pats
-      catch | _ => return  -- can happen in case of pattern antiquotations
+      catch _ => return  -- can happen in case of pattern antiquotations
       Quotation.withNewLocals (getPatternVarNames vars) <| precheck rhs
   | _ => throwUnsupportedSyntax
 
@@ -346,9 +346,9 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
               | some path =>
                 restoreState s
                 -- Wrap the type mismatch exception for the "discriminant refinement" feature.
-                throwThe PatternElabException { ex := ex, patternIdx := idx, pathToIndex := path }
-              | none => restoreState s; throw ex
-            | none => throw ex
+                throw { ex := ex, patternIdx := idx, pathToIndex := path }
+              | none => restoreState s; throwThe Exception ex
+            | none => throwThe Exception ex
         matchType := b.instantiate1 pattern
         patterns  := patterns.push pattern
       | _ => throwError "unexpected match type"

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -222,7 +222,7 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
         let args := e.getAppArgs
         for discr in args[info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
           if (← Meta.isConstructorApp discr) then
-            throwThe Unit ()
+            throw ()
   return (← (find e).run) matches .error _
 
 partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do

src/lake/Lake/Util/Cycle.lean

@@ -58,14 +58,14 @@ instance inhabitedOfMonadCycle [MonadCycle κ m] : Inhabited (m α) := ⟨throwC
 /-- A transformer that equips a monad with a `CallStack`. -/
 abbrev CallStackT κ m := ReaderT (CallStack κ) m
 
-instance [Monad m] : MonadCallStackOf κ (CallStackT κ m) where
+instance (priority := high) [Monad m] : MonadCallStackOf κ (CallStackT κ m) where
   getCallStack := read
   withCallStack s x := x s
 
 /-- A transformer that equips a monad with a `CallStack` to detect cycles. -/
 abbrev CycleT κ m := CallStackT κ <| ExceptT (Cycle κ) m
 
-instance [Monad m] : MonadCycleOf κ (CycleT κ m) where
+instance (priority := high) [Monad m] : MonadCycleOf κ (CycleT κ m) where
   throwCycle := throw
 
 /--

src/lake/Lake/Util/EStateT.lean

@@ -185,7 +185,7 @@ protected def get [Pure m] : EStateT ε σ m σ := fun s =>
 protected def modifyGet [Pure m] (f : σ → Prod α σ) : EStateT ε σ m α := fun s =>
   match f s with | (a, s) => pure <| .ok a s
 
-instance [Pure m] : MonadStateOf σ (EStateT ε σ m) where
+instance (priority := high) [Pure m] : MonadStateOf σ (EStateT ε σ m) where
   set       := EStateT.set
   get       := EStateT.get
   modifyGet := EStateT.modifyGet
@@ -201,7 +201,7 @@ protected def tryCatch [Monad m] (x : EStateT ε σ m α) (handle : ε → EStat
   | .error e s => handle e s
   | ok         => pure ok
 
-instance [Monad m] : MonadExceptOf ε (EStateT ε σ m) where
+instance (priority := high) [Monad m] : MonadExceptOf ε (EStateT ε σ m) where
   throw    := EStateT.throw
   tryCatch := EStateT.tryCatch
 

tests/lean/run/catchThe.lean

@@ -14,7 +14,7 @@ def testM {α} [BEq α] [ToString α] (x : M α) (expected : α)  : MetaM Unit :
   | Except.error e => throwError m!"FAILED: {e}"
 
 @[noinline] def act1 : M Nat :=
-  throw <| Exception.error Syntax.missing "Error at act1"
+  throwThe Exception <| Exception.error Syntax.missing "Error at act1"
 
 def g1 : M Nat :=
   tryCatchThe Exception
@@ -25,7 +25,7 @@ def g1 : M Nat :=
 #eval testM g1 200
 
 @[noinline] def act2 : M Nat :=
-  throwThe String "hello world"
+  throw "hello world"
 
 def g2 : M Nat :=
 tryCatchThe Exception