From f3c344e7855ca96fdcf7d1756a198c3bb4496bf0 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Wed, 11 Sep 2024 00:03:27 +0200
Subject: [PATCH] the rest

---
 src/Init/Control/Option.lean    | 2 +-
 src/Init/Control/State.lean     | 2 +-
 src/lake/Lake/Util/Cycle.lean   | 2 +-
 src/lake/Lake/Util/EStateT.lean | 2 +-
 src/lake/Lake/Util/Store.lean   | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index 1df47eda77f6..5decf1a34b4b 100644
--- a/src/Init/Control/Option.lean
+++ b/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
 
diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index c3e6e60b3066..2543519be7d2 100644
--- a/src/Init/Control/State.lean
+++ b/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
diff --git a/src/lake/Lake/Util/Cycle.lean b/src/lake/Lake/Util/Cycle.lean
index 36e5155538fd..73312ed81bb8 100644
--- a/src/lake/Lake/Util/Cycle.lean
+++ b/src/lake/Lake/Util/Cycle.lean
@@ -62,7 +62,7 @@ instance (priority := high) [Monad m] : MonadCallStackOf κ (CallStackT κ m) wh
 /-- 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
 
 /--
diff --git a/src/lake/Lake/Util/EStateT.lean b/src/lake/Lake/Util/EStateT.lean
index 31de108de8bd..84c5473ba55a 100644
--- a/src/lake/Lake/Util/EStateT.lean
+++ b/src/lake/Lake/Util/EStateT.lean
@@ -183,7 +183,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
diff --git a/src/lake/Lake/Util/Store.lean b/src/lake/Lake/Util/Store.lean
index 123ea39296c4..c4a7ba37d9ae 100644
--- a/src/lake/Lake/Util/Store.lean
+++ b/src/lake/Lake/Util/Store.lean
@@ -28,7 +28,7 @@ class MonadDStore (κ : Type u) (β : semiOutParam $ κ → Type v) (m : Type v
   fetch? : (key : κ) → m (Option (β key))
   store : (key : κ) → β key → m PUnit
 
-instance [MonadDStore κ β m] : MonadStore1Of k (β k) m where
+instance (priority := high) [MonadDStore κ β m] : MonadStore1Of k (β k) m where
   fetch? := MonadDStore.fetch? k
   store o := MonadDStore.store k o