set high 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 => throw ⟨.invalidParams, s!"no constant named '{name}'"⟩
       Widget.ppExprTagged c.type
 
 /-!

doc/monads/transformers.lean

@@ -218,7 +218,7 @@ def liftTest2 (x : Except String Float) :
 The ReaderT monadLift is even simpler than the one for StateT:
 
 ```lean,ignore
-instance  : MonadLift m (ReaderT ρ m) where
+instance : MonadLift m (ReaderT ρ m) where
   monadLift x := fun _ => x
 ```
 
@@ -313,4 +313,4 @@ truly master monads, you should know how to make your own, and there's one final
 should understand for that. This is the idea of type "laws". Each of the structures you've learned
 so far has a series of laws associated with it. And for your instances of these classes to make
 sense, they should follow the laws! Check out [Monad Laws](laws.lean.md).
--/
+-/

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/Prelude.lean

@@ -3016,7 +3016,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]
@@ -3112,7 +3112,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
 
 /--
@@ -3149,7 +3150,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)
 
 /--
@@ -3235,8 +3237,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
@@ -3373,7 +3373,8 @@ instance : MonadStateOf σ (EStateM ε σ) where
   get       := EStateM.get
   modifyGet := EStateM.modifyGet
 
-instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) where
+/- (priority := high) -/
+instance (priority := 10000) {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) where
   throw    := EStateM.throw
   tryCatch := EStateM.tryCatch
 

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
 
@@ -347,9 +347,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

@@ -55,7 +55,7 @@ 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
 

src/lake/Lake/Util/EStateT.lean

@@ -199,7 +199,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,23 +14,23 @@ 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
-    (tryCatchThe String act1 (fun ex => pure 100))
+    (tryCatch act1 (fun ex => pure 100))
     (fun ex => pure 200)
 
 /-- info: -/
 #guard_msgs in
 #eval testM g1 200
 
 @[noinline] def act2 : M Nat :=
-  throwThe String "hello world"
+  throw "hello world"
 
 def g2 : M Nat :=
 tryCatchThe Exception
-  (tryCatchThe String act2 (fun ex => pure 100))
+  (tryCatch act2 (fun ex => pure 100))
   (fun ex => pure 200)
 
 /-- info: -/