diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 084800219d..7221eb929f 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -25,7 +25,7 @@ instances are provided for the same type.
 instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
   forIn x b f := forIn' x b fun a _ => f a
 
-@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
+@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} (x : ρ) (b : β)
     (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : (a : α) → β → m (ForInStep β))
     (h : ∀ a m b, f a m b = g a b) :
     forIn' x b f = forIn x b g := by
@@ -40,7 +40,7 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
   simp [h]
   rfl
 
-@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m]
+@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β}
     (x : ρ) (b : β) (f : (a : α) → β → m (ForInStep β)) :
     forIn x b f = forIn' x b (fun x h => binderNameHint x f <| binderNameHint h () <| f x) := by
   rfl
@@ -403,7 +403,7 @@ class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂))
   /--
   Runs the monadic action `f` on each element of the collection `coll`.
   -/
-  forM [Monad m] (coll : γ) (f : α → m PUnit) : m PUnit
+  forM (coll : γ) (f : α → m PUnit) : m PUnit
 
 export ForM (forM)
 
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 937a34dd98..edd95ec580 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -377,7 +377,7 @@ class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v))
   More information about the translation of `for` loops into `ForIn.forIn` is available in [the Lean
   reference manual](lean-manual://section/monad-iteration-syntax).
   -/
-  forIn {β} [Monad m] (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
+  forIn {β} (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
 
 export ForIn (forIn)
 
@@ -405,7 +405,7 @@ class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)
   More information about the translation of `for` loops into `ForIn'.forIn'` is available in [the
   Lean reference manual](lean-manual://section/monad-iteration-syntax).
   -/
-  forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
+  forIn' {β} (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
 
 export ForIn' (forIn')
 
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 58dd1d9045..5805456fcb 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -570,7 +570,7 @@ protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
 
-instance : ForIn' m (Array α) α inferInstance where
+instance [Monad m] : ForIn' m (Array α) α inferInstance where
   forIn' := Array.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -1001,7 +1001,7 @@ unless `start < stop`. By default, the entire array is used.
 protected def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit :=
   as.foldlM (fun _ => f) ⟨⟩ start stop
 
-instance : ForM m (Array α) α where
+instance [Monad m] : ForM m (Array α) α where
   forM xs f := Array.forM f xs
 
 -- We simplify `Array.forM` to `forM`.
diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean
index 44a6265598..9b59bfff74 100644
--- a/src/Init/Data/ByteArray/Basic.lean
+++ b/src/Init/Data/ByteArray/Basic.lean
@@ -243,7 +243,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
 
-instance : ForIn m ByteArray UInt8 where
+instance [Monad m] : ForIn m ByteArray UInt8 where
   forIn := ByteArray.forIn
 
 /--
diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean
index 21de86a98a..759e3b0de5 100644
--- a/src/Init/Data/FloatArray/Basic.lean
+++ b/src/Init/Data/FloatArray/Basic.lean
@@ -129,7 +129,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatA
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
 
-instance : ForIn m FloatArray Float where
+instance [Monad m] : ForIn m FloatArray Float where
   forIn := FloatArray.forIn
 
 /-- See comment at `forInUnsafe` -/
diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean
index 778d67d4ee..61eb64f890 100644
--- a/src/Init/Data/Iterators/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Loop.lean
@@ -63,12 +63,12 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
   instForInOfForIn'
 
 instance {m : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] :
+    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] [Monad m] :
     ForM m (Iter (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
 instance {m : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] :
+    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] [Monad m] :
     ForM m (Iter.Partial (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
index b2b286b97d..49f1a69949 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
@@ -247,10 +247,10 @@ This `ForIn'`-style loop construct traverses a finite iterator using an `Iterato
 -/
 @[always_inline, inline]
 def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
+    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) :
     ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
-  forIn' {γ} [Monad n] it init f :=
+  forIn' {γ} it init f :=
     IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
       wellFounded_of_finite
       it init (fun out h acc => (⟨·, .intro⟩) <$> f out h acc)
@@ -288,13 +288,13 @@ instance {m : Type w → Type w'} {n : Type w → Type w''}
   instForInOfForIn'
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
+    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
     [MonadLiftT m n] :
     ForM n (IterM (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n]
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [Monad n]
     [MonadLiftT m n] :
     ForM n (IterM.Partial (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index c2c2eebbd1..247a237494 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -471,7 +471,7 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
         loop as' b this
   loop as init ⟨[], rfl⟩
 
-instance : ForIn' m (List α) α inferInstance where
+instance [Monad m] : ForIn' m (List α) α inferInstance where
   forIn' := List.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -485,7 +485,7 @@ instance : ForIn' m (List α) α inferInstance where
 @[simp, grind =] theorem forIn_nil [Monad m] {f : α → β → m (ForInStep β)} {b : β} : forIn [] b f = pure b :=
   rfl
 
-instance : ForM m (List α) α where
+instance [Monad m] : ForM m (List α) α where
   forM := List.forM
 
 -- We simplify `List.forM` to `forM`.
diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean
index 0dbbaa1420..c792f12d04 100644
--- a/src/Init/Data/Option/Instances.lean
+++ b/src/Init/Data/Option/Instances.lean
@@ -168,10 +168,10 @@ Examples:
   | none  , _ => pure ⟨⟩
   | some a, f => f a
 
-instance : ForM m (Option α) α :=
+instance [Monad m] : ForM m (Option α) α :=
   ⟨Option.forM⟩
 
-instance : ForIn' m (Option α) α inferInstance where
+instance [Monad m] : ForIn' m (Option α) α inferInstance where
   forIn' x init f := do
     match x with
     | none => return init
diff --git a/src/Init/Data/Range/Basic.lean b/src/Init/Data/Range/Basic.lean
index a9bab2b03f..4c9c3e96ee 100644
--- a/src/Init/Data/Range/Basic.lean
+++ b/src/Init/Data/Range/Basic.lean
@@ -43,7 +43,7 @@ universe u v
   have := range.step_pos
   loop init range.start (by simp)
 
-instance : ForIn' m Range Nat inferInstance where
+instance [Monad m] : ForIn' m Range Nat inferInstance where
   forIn' := Range.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -59,7 +59,7 @@ instance : ForIn' m Range Nat inferInstance where
   have := range.step_pos
   loop range.start
 
-instance : ForM m Range Nat where
+instance [Monad m] : ForM m Range Nat where
   forM := Range.forM
 
 syntax:max "[" withoutPosition(":" term) "]" : term
diff --git a/src/Init/Data/Slice/List/Iterator.lean b/src/Init/Data/Slice/List/Iterator.lean
index 804aec8881..087155ef6f 100644
--- a/src/Init/Data/Slice/List/Iterator.lean
+++ b/src/Init/Data/Slice/List/Iterator.lean
@@ -37,7 +37,7 @@ instance : SliceSize (Internal.ListSliceData α) where
   size s := (Internal.iter s).count
 
 @[no_expose]
-instance {α : Type u} {m : Type v → Type w} :
+instance {α : Type u} {m : Type v → Type w} [Monad m] :
     ForIn m (ListSlice α) α where
   forIn xs init f := forIn (Internal.iter xs) init f
 
diff --git a/src/Init/Data/Slice/Operations.lean b/src/Init/Data/Slice/Operations.lean
index e1796fa02b..ffdb849ae6 100644
--- a/src/Init/Data/Slice/Operations.lean
+++ b/src/Init/Data/Slice/Operations.lean
@@ -75,7 +75,7 @@ def toListRev [ToIterator (Slice γ) Id α β] [Iterator α Id β]
     [Finite α Id] (s : Slice γ) : List β :=
   Internal.iter s |>.toListRev
 
-instance {γ : Type u} {β : Type v} [ToIterator (Slice γ) Id α β]
+instance {γ : Type u} {β : Type v} [Monad m] [ToIterator (Slice γ) Id α β]
     [Iterator α Id β]
     [IteratorLoop α Id m]
     [Finite α Id] :
diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean
index 021089ca3d..623c9f2e95 100644
--- a/src/Init/Data/Stream.lean
+++ b/src/Init/Data/Stream.lean
@@ -66,7 +66,7 @@ protected partial def Stream.forIn [Stream ρ α] [Monad m] (s : ρ) (b : β) (f
     | none => return b
   visit s b
 
-instance (priority := low) [Stream ρ α] : ForIn m ρ α where
+instance (priority := low) [Monad m] [Stream ρ α] : ForIn m ρ α where
   forIn := Stream.forIn
 
 instance : ToStream (List α) (List α) where
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 9d810ef552..8755e112fc 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -525,12 +525,12 @@ and do not provide separate verification theorems.
 @[simp] theorem mem_toArray_iff (a : α) (xs : Vector α n) : a ∈ xs.toArray ↔ a ∈ xs :=
   ⟨fun h => ⟨h⟩, fun ⟨h⟩ => h⟩
 
-instance : ForIn' m (Vector α n) α inferInstance where
+instance [Monad m] : ForIn' m (Vector α n) α inferInstance where
   forIn' xs b f := Array.forIn' xs.toArray b (fun a h b => f a (by simpa using h) b)
 
 /-! ### ForM instance -/
 
-instance : ForM m (Vector α n) α where
+instance [Monad m] : ForM m (Vector α n) α where
   forM := Vector.forM
 
 -- We simplify `Vector.forM` to `forM`.
diff --git a/src/Init/While.lean b/src/Init/While.lean
index 4d59c5b28d..808aa94c57 100644
--- a/src/Init/While.lean
+++ b/src/Init/While.lean
@@ -29,7 +29,7 @@ partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop
       | ForInStep.yield b => loop b
   loop init
 
-instance : ForIn m Loop Unit where
+instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
 syntax "repeat " doSeq : doElem
diff --git a/src/Lean/Data/AssocList.lean b/src/Lean/Data/AssocList.lean
index c5c0f5ffd2..5d53e2230b 100644
--- a/src/Lean/Data/AssocList.lean
+++ b/src/Lean/Data/AssocList.lean
@@ -110,7 +110,7 @@ def all (p : α → β → Bool) : AssocList α β → Bool
       | ForInStep.yield d => loop d es
   loop init as
 
-instance : ForIn m (AssocList α β) (α × β) where
+instance [Monad m] : ForIn m (AssocList α β) (α × β) where
   forIn := AssocList.forIn
 
 end Lean.AssocList
diff --git a/src/Lean/Data/KVMap.lean b/src/Lean/Data/KVMap.lean
index 14d031f510..9030058ef9 100644
--- a/src/Lean/Data/KVMap.lean
+++ b/src/Lean/Data/KVMap.lean
@@ -183,7 +183,7 @@ def updateSyntax (m : KVMap) (k : Name) (f : Syntax → Syntax) : KVMap :=
   (kv : KVMap) (init : δ) (f : Name × DataValue → δ → m (ForInStep δ)) : m δ :=
   forIn kv.entries init f
 
-instance : ForIn m KVMap (Name × DataValue) where
+instance [Monad m] : ForIn m KVMap (Name × DataValue) where
   forIn := KVMap.forIn
 
 def subsetAux : List (Name × DataValue) → KVMap → Bool
diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean
index abf17ce3b7..04ee843854 100644
--- a/src/Lean/Data/Lsp/Internal.lean
+++ b/src/Lean/Data/Lsp/Internal.lean
@@ -188,7 +188,7 @@ instance : FromJson RefInfo where
 @[expose] def ModuleRefs := Std.TreeMap RefIdent RefInfo
   deriving EmptyCollection
 
-instance : ForIn m ModuleRefs (RefIdent × RefInfo) where
+instance [Monad m] : ForIn m ModuleRefs (RefIdent × RefInfo) where
   forIn map init f :=
     let map : Std.TreeMap RefIdent RefInfo := map
     forIn map init f
diff --git a/src/Lean/Data/NameMap/Basic.lean b/src/Lean/Data/NameMap/Basic.lean
index 4aa4e2934a..4229f72ade 100644
--- a/src/Lean/Data/NameMap/Basic.lean
+++ b/src/Lean/Data/NameMap/Basic.lean
@@ -35,7 +35,7 @@ def contains (m : NameMap α) (n : Name) : Bool := Std.TreeMap.contains m n
 
 def find? (m : NameMap α) (n : Name) : Option α := Std.TreeMap.get? m n
 
-instance : ForIn m (NameMap α) (Name × α) :=
+instance [Monad m] : ForIn m (NameMap α) (Name × α) :=
   inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) ..)
 
 /-- `filter f m` returns the `NameMap` consisting of all
@@ -52,7 +52,7 @@ instance : EmptyCollection NameSet := ⟨empty⟩
 instance : Inhabited NameSet := ⟨empty⟩
 def insert (s : NameSet) (n : Name) : NameSet := Std.TreeSet.insert s n
 def contains (s : NameSet) (n : Name) : Bool := Std.TreeSet.contains s n
-instance : ForIn m NameSet Name :=
+instance [Monad m] : ForIn m NameSet Name :=
   inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)
 
 /-- The union of two `NameSet`s. -/
diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean
index b099036067..57fec1fda6 100644
--- a/src/Lean/Data/Options.lean
+++ b/src/Lean/Data/Options.lean
@@ -20,7 +20,7 @@ def Options.empty : Options  := {}
 instance : Inhabited Options where
   default := {}
 instance : ToString Options := inferInstanceAs (ToString KVMap)
-instance : ForIn m Options (Name × DataValue) := inferInstanceAs (ForIn _ KVMap _)
+instance [Monad m] : ForIn m Options (Name × DataValue) := inferInstanceAs (ForIn _ KVMap _)
 instance : BEq Options := inferInstanceAs (BEq KVMap)
 
 structure OptionDecl where
diff --git a/src/Lean/Data/PersistentArray.lean b/src/Lean/Data/PersistentArray.lean
index d236641647..d98f5c1dc1 100644
--- a/src/Lean/Data/PersistentArray.lean
+++ b/src/Lean/Data/PersistentArray.lean
@@ -252,7 +252,7 @@ partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       | ForInStep.yield bNew => b := bNew
     return b
 
-instance : ForIn m (PersistentArray α) α where
+instance [Monad m] : ForIn m (PersistentArray α) α where
   forIn := PersistentArray.forIn
 
 @[specialize] partial def findSomeMAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β)
diff --git a/src/Lean/Data/PersistentHashMap.lean b/src/Lean/Data/PersistentHashMap.lean
index c2109f966b..e8bc3ce88b 100644
--- a/src/Lean/Data/PersistentHashMap.lean
+++ b/src/Lean/Data/PersistentHashMap.lean
@@ -304,7 +304,7 @@ protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
   match result with
   | .ok s | .error s => pure s
 
-instance {_ : BEq α} {_ : Hashable α} : ForIn m (PersistentHashMap α β) (α × β) where
+instance {_ : BEq α} {_ : Hashable α} [Monad m] : ForIn m (PersistentHashMap α β) (α × β) where
   forIn := PersistentHashMap.forIn
 
 end
diff --git a/src/Lean/Data/PersistentHashSet.lean b/src/Lean/Data/PersistentHashSet.lean
index 014c7e69d7..6ffad96c4a 100644
--- a/src/Lean/Data/PersistentHashSet.lean
+++ b/src/Lean/Data/PersistentHashSet.lean
@@ -61,7 +61,7 @@ protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
     (s : PersistentHashSet α) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ := do
   PersistentHashMap.forIn s.set init fun p s => f p.1 s
 
-instance {_ : BEq α} {_ : Hashable α} : ForIn m (PersistentHashSet α) α where
+instance {_ : BEq α} {_ : Hashable α} [Monad m] : ForIn m (PersistentHashSet α) α where
   forIn := PersistentHashSet.forIn
 
 end PersistentHashSet
diff --git a/src/Lean/Data/RBMap.lean b/src/Lean/Data/RBMap.lean
index bf702ddb58..4fe7a63777 100644
--- a/src/Lean/Data/RBMap.lean
+++ b/src/Lean/Data/RBMap.lean
@@ -295,7 +295,7 @@ def isSingleton (t : RBMap α β cmp) : Bool :=
 @[inline] protected def forIn [Monad m] (t : RBMap α β cmp) (init : σ) (f : (α × β) → σ → m (ForInStep σ)) : m σ :=
   t.val.forIn init (fun a b acc => f (a, b) acc)
 
-instance : ForIn m (RBMap α β cmp) (α × β) where
+instance [Monad m] : ForIn m (RBMap α β cmp) (α × β) where
   forIn := RBMap.forIn
 
 @[inline] def isEmpty : RBMap α β cmp → Bool
diff --git a/src/Lean/Data/RBTree.lean b/src/Lean/Data/RBTree.lean
index 5768c468b5..af0e305b2a 100644
--- a/src/Lean/Data/RBTree.lean
+++ b/src/Lean/Data/RBTree.lean
@@ -48,7 +48,7 @@ variable {α : Type u} {β : Type v} {cmp : α → α → Ordering}
 @[inline] protected def forIn [Monad m] (t : RBTree α cmp) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ :=
   t.val.forIn init (fun a _ acc => f a acc)
 
-instance : ForIn m (RBTree α cmp) α where
+instance [Monad m] : ForIn m (RBTree α cmp) α where
   forIn := RBTree.forIn
 
 @[inline] def isEmpty (t : RBTree α cmp) : Bool :=
diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index fdc76ae5c8..0cb3f5ff0f 100644
--- a/src/Lean/Data/SMap.lean
+++ b/src/Lean/Data/SMap.lean
@@ -80,10 +80,10 @@ def forM [Monad m] (s : SMap α β) (f : α → β → m PUnit) : m PUnit := do
   s.map₁.forM f
   s.map₂.forM f
 
-instance : ForM m (SMap α β) (α × β) where
+instance [Monad m] : ForM m (SMap α β) (α × β) where
   forM s f := forM s fun x y => f (x, y)
 
-instance : ForIn m (SMap α β) (α × β) where
+instance [Monad m] : ForIn m (SMap α β) (α × β) where
   forIn := ForM.forIn
 
 /-- Move from stage 1 into stage 2. -/
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 3d5195bc25..bc1614d2dd 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -218,7 +218,7 @@ This is a persistent data structure implemented using `Std.TreeSet`. -/
 @[expose] def FVarIdSet := Std.TreeSet FVarId (Name.quickCmp ·.name ·.name)
   deriving Inhabited, EmptyCollection
 
-instance : ForIn m FVarIdSet FVarId := inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)
+instance [Monad m] : ForIn m FVarIdSet FVarId := inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)
 
 def FVarIdSet.insert (s : FVarIdSet) (fvarId : FVarId) : FVarIdSet :=
   Std.TreeSet.insert s fvarId
@@ -272,7 +272,7 @@ def MVarIdSet.ofList (l : List MVarId) : MVarIdSet :=
 def MVarIdSet.ofArray (l : Array MVarId) : MVarIdSet :=
   Std.TreeSet.ofArray l _
 
-instance : ForIn m MVarIdSet MVarId := inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)
+instance [Monad m] : ForIn m MVarIdSet MVarId := inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)
 
 @[expose] def MVarIdMap (α : Type) := Std.TreeMap MVarId α (Name.quickCmp ·.name ·.name)
 
@@ -281,7 +281,7 @@ def MVarIdMap.insert (s : MVarIdMap α) (mvarId : MVarId) (a : α) : MVarIdMap 
 
 instance : EmptyCollection (MVarIdMap α) := inferInstanceAs (EmptyCollection (Std.TreeMap _ _ _))
 
-instance : ForIn m (MVarIdMap α) (MVarId × α) := inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) ..)
+instance [Monad m] : ForIn m (MVarIdMap α) (MVarId × α) := inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) ..)
 
 instance : Inhabited (MVarIdMap α) where
   default := {}
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index fcf61993f2..0ffb00e1bd 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -74,13 +74,13 @@ instance : Repr LMVarId where
 @[expose] def LMVarIdSet := Std.TreeSet LMVarId (Name.quickCmp ·.name ·.name)
   deriving Inhabited, EmptyCollection
 
-instance : ForIn m LMVarIdSet LMVarId := inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)
+instance [Monad m] : ForIn m LMVarIdSet LMVarId := inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)
 
 @[expose] def LMVarIdMap (α : Type) := Std.TreeMap LMVarId α (Name.quickCmp ·.name ·.name)
 
 instance : EmptyCollection (LMVarIdMap α) := inferInstanceAs (EmptyCollection (Std.TreeMap _ _ _))
 
-instance : ForIn m (LMVarIdMap α) (LMVarId × α) := inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) ..)
+instance [Monad m] : ForIn m (LMVarIdMap α) (LMVarId × α) := inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) ..)
 
 instance : Inhabited (LMVarIdMap α) where
   default := {}
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 14751357c0..708e0ce285 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -506,7 +506,7 @@ def getAt? (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
     | none      => pure none
     | some decl => f decl
 
-instance : ForIn m LocalContext LocalDecl where
+instance [Monad m] : ForIn m LocalContext LocalDecl where
   forIn lctx init f := lctx.decls.forIn init fun d? b => match d? with
     | none   => return ForInStep.yield b
     | some d => f d b
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index ce8fed4544..77defa7a75 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1612,7 +1612,7 @@ instance : Inhabited (TokenMap α) where
 
 instance : EmptyCollection (TokenMap α) := ⟨Std.TreeMap.empty⟩
 
-instance : ForIn m (TokenMap α) (Name × List α) := inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) _)
+instance [Monad m] : ForIn m (TokenMap α) (Name × List α) := inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) _)
 
 end TokenMap
 
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index 00e55d5e4e..690f8738e6 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -138,7 +138,7 @@ section Utils
     def contains (m : RequestQueueMap) (id : RequestID) : Bool :=
       m.reqs.contains id
 
-    instance : ForIn m RequestQueueMap (RequestID × JsonRpc.Request Json) where
+    instance [Monad m] : ForIn m RequestQueueMap (RequestID × JsonRpc.Request Json) where
       forIn map init f := map.queue.forIn (fun _ a b => f a b) init
   end RequestQueueMap
 
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 489f631059..d6f3a9e8ec 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -368,7 +368,7 @@ If `firstChoiceOnly` is `true`, only visit the first argument of each choice nod
 -/
 def topDown (stx : Syntax) (firstChoiceOnly := false) : TopDown := ⟨firstChoiceOnly, stx⟩
 
-partial instance : ForIn m TopDown Syntax where
+partial instance [Monad m] : ForIn m TopDown Syntax where
   forIn := fun ⟨firstChoiceOnly, stx⟩ init f => do
     let rec @[specialize] loop stx b [Inhabited (type_of% b)] := do
       match (← f stx b) with
diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean
index 88abac99b4..9094436568 100644
--- a/src/Std/Data/DHashMap/Basic.lean
+++ b/src/Std/Data/DHashMap/Basic.lean
@@ -235,10 +235,10 @@ end
     (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (b : DHashMap α β) : m δ :=
   b.1.forIn f init
 
-instance [BEq α] [Hashable α] : ForM m (DHashMap α β) ((a : α) × β a) where
+instance [Monad m] [BEq α] [Hashable α] : ForM m (DHashMap α β) ((a : α) × β a) where
   forM m f := m.forM (fun a b => f ⟨a, b⟩)
 
-instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) where
+instance [Monad m] [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
 namespace Const
diff --git a/src/Std/Data/DHashMap/RawDef.lean b/src/Std/Data/DHashMap/RawDef.lean
index f17b03f1c7..da98931f82 100644
--- a/src/Std/Data/DHashMap/RawDef.lean
+++ b/src/Std/Data/DHashMap/RawDef.lean
@@ -75,10 +75,10 @@ map in some order.
 @[inline] def forIn [Monad m] (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (b : Raw α β) : m δ :=
   ForIn.forIn b.buckets init (fun bucket acc => bucket.forInStep acc f)
 
-instance x : ForM m (Raw α β) ((a : α) × β a) where
+instance [Monad m] : ForM m (Raw α β) ((a : α) × β a) where
   forM m f := m.forM (fun a b => f ⟨a, b⟩)
 
-instance : ForIn m (Raw α β) ((a : α) × β a) where
+instance [Monad m] : ForIn m (Raw α β) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
 end Raw
diff --git a/src/Std/Data/DTreeMap/Basic.lean b/src/Std/Data/DTreeMap/Basic.lean
index b99d200d90..7868d4c0e3 100644
--- a/src/Std/Data/DTreeMap/Basic.lean
+++ b/src/Std/Data/DTreeMap/Basic.lean
@@ -842,10 +842,10 @@ def forM (f : (a : α) → β a → m PUnit) (t : DTreeMap α β cmp) : m PUnit
 def forIn (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (t : DTreeMap α β cmp) : m δ :=
   t.inner.forIn f init
 
-instance : ForM m (DTreeMap α β cmp) ((a : α) × β a) where
+instance [Monad m] : ForM m (DTreeMap α β cmp) ((a : α) × β a) where
   forM t f := t.forM (fun a b => f ⟨a, b⟩)
 
-instance : ForIn m (DTreeMap α β cmp) ((a : α) × β a) where
+instance [Monad m] : ForIn m (DTreeMap α β cmp) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
 namespace Const
diff --git a/src/Std/Data/DTreeMap/Internal/Queries.lean b/src/Std/Data/DTreeMap/Internal/Queries.lean
index 8936025576..fb2c05b486 100644
--- a/src/Std/Data/DTreeMap/Internal/Queries.lean
+++ b/src/Std/Data/DTreeMap/Internal/Queries.lean
@@ -290,7 +290,7 @@ def forIn {m} [Monad m] (f : (a : α) → β a → δ → m (ForInStep δ)) (ini
   | ForInStep.done d => return d
   | ForInStep.yield d => return d
 
-instance : ForIn m (Impl α β) ((a : α) × β a) where
+instance [Monad m] : ForIn m (Impl α β) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
 /-- Returns a `List` of the keys in order. -/
diff --git a/src/Std/Data/DTreeMap/Raw/Basic.lean b/src/Std/Data/DTreeMap/Raw/Basic.lean
index 2d8e2c38cc..88b6db876e 100644
--- a/src/Std/Data/DTreeMap/Raw/Basic.lean
+++ b/src/Std/Data/DTreeMap/Raw/Basic.lean
@@ -577,10 +577,10 @@ def forM (f : (a : α) → β a → m PUnit) (t : Raw α β cmp) : m PUnit :=
 def forIn (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (t : Raw α β cmp) : m δ :=
   t.inner.forIn f init
 
-instance : ForM m (Raw α β cmp) ((a : α) × β a) where
+instance [Monad m] : ForM m (Raw α β cmp) ((a : α) × β a) where
   forM t f := t.forM (fun a b => f ⟨a, b⟩)
 
-instance : ForIn m (Raw α β cmp) ((a : α) × β a) where
+instance [Monad m] : ForIn m (Raw α β cmp) ((a : α) × β a) where
   forIn t init f := t.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
 namespace Const
diff --git a/src/Std/Data/ExtDTreeMap/Basic.lean b/src/Std/Data/ExtDTreeMap/Basic.lean
index 6e23a4c09f..72ecae2d59 100644
--- a/src/Std/Data/ExtDTreeMap/Basic.lean
+++ b/src/Std/Data/ExtDTreeMap/Basic.lean
@@ -727,16 +727,11 @@ def forM [TransCmp cmp] (f : (a : α) → β a → m PUnit) (t : ExtDTreeMap α
 def forIn [TransCmp cmp] (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (t : ExtDTreeMap α β cmp) : m δ :=
   t.lift (fun m => m.forIn f init) (fun _ _ h => h.forIn_eq (f := fun x => f x.1 x.2))
 
-/-
-Note: We ignore the monad instance provided by `forM` / `forIn` and instead use the one from the
-instance in order to get the `LawfulMonad m` assumption
--/
+instance [TransCmp cmp] [Monad m] [LawfulMonad m] : ForM m (ExtDTreeMap α β cmp) ((a : α) × β a) where
+  forM t f := forM (fun a b => f ⟨a, b⟩) t
 
-instance [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForM m (ExtDTreeMap α β cmp) ((a : α) × β a) where
-  forM t f := @forM _ _ _ _ inst _ _ (fun a b => f ⟨a, b⟩) t
-
-instance [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForIn m (ExtDTreeMap α β cmp) ((a : α) × β a) where
-  forIn m init f := @forIn _ _ _ _ _ inst _ _ (fun a b acc => f ⟨a, b⟩ acc) init m
+instance [TransCmp cmp] [Monad m] [LawfulMonad m] : ForIn m (ExtDTreeMap α β cmp) ((a : α) × β a) where
+  forIn m init f := forIn (fun a b acc => f ⟨a, b⟩ acc) init m
 
 namespace Const
 
diff --git a/src/Std/Data/ExtTreeMap/Basic.lean b/src/Std/Data/ExtTreeMap/Basic.lean
index 65e1288641..75adc6d62a 100644
--- a/src/Std/Data/ExtTreeMap/Basic.lean
+++ b/src/Std/Data/ExtTreeMap/Basic.lean
@@ -451,16 +451,11 @@ def forM [TransCmp cmp] (f : α → β → m PUnit) (t : ExtTreeMap α β cmp) :
 def forIn [TransCmp cmp] (f : α → β → δ → m (ForInStep δ)) (init : δ) (t : ExtTreeMap α β cmp) : m δ :=
   t.inner.forIn (fun a b c => f a b c) init
 
-/-
-Note: We ignore the monad instance provided by `forM` / `forIn` and instead use the one from the
-instance in order to get the `LawfulMonad m` assumption
--/
+instance [TransCmp cmp] [Monad m] [LawfulMonad m] : ForM m (ExtTreeMap α β cmp) (α × β) where
+  forM t f := forM (fun a b => f ⟨a, b⟩) t
 
-instance [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForM m (ExtTreeMap α β cmp) (α × β) where
-  forM t f := @forM _ _ _ _ inst _ _ (fun a b => f ⟨a, b⟩) t
-
-instance [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForIn m (ExtTreeMap α β cmp) (α × β) where
-  forIn m init f := @forIn _ _ _ _ _ inst _ _ (fun a b acc => f ⟨a, b⟩ acc) init m
+instance [TransCmp cmp] [Monad m] [LawfulMonad m] : ForIn m (ExtTreeMap α β cmp) (α × β) where
+  forIn m init f := forIn (fun a b acc => f ⟨a, b⟩ acc) init m
 
 @[inline, inherit_doc ExtDTreeMap.any]
 def any [TransCmp cmp] (t : ExtTreeMap α β cmp) (p : α → β → Bool) : Bool :=
diff --git a/src/Std/Data/ExtTreeSet/Basic.lean b/src/Std/Data/ExtTreeSet/Basic.lean
index 8f455ec7e5..e0e558eab5 100644
--- a/src/Std/Data/ExtTreeSet/Basic.lean
+++ b/src/Std/Data/ExtTreeSet/Basic.lean
@@ -446,16 +446,12 @@ order.
 def forIn [TransCmp cmp] (f : α → δ → m (ForInStep δ)) (init : δ) (t : ExtTreeSet α cmp) : m δ :=
   t.inner.forIn (fun a _ c => f a c) init
 
-/-
-Note: We ignore the monad instance provided by `forM` / `forIn` and instead use the one from the
-instance in order to get the `LawfulMonad m` assumption
--/
 
-instance [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForM m (ExtTreeSet α cmp) α where
-  forM t f := @forM _ _ _ inst _ _ f t
+instance [TransCmp cmp] [Monad m] [LawfulMonad m] : ForM m (ExtTreeSet α cmp) α where
+  forM t f := forM f t
 
-instance [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForIn m (ExtTreeSet α cmp) α where
-  forIn m init f := @forIn _ _ _ _ inst _ _ f init m
+instance [TransCmp cmp] [Monad m] [LawfulMonad m] : ForIn m (ExtTreeSet α cmp) α where
+  forIn m init f := forIn f init m
 
 /-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/
 @[inline]
diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index 941caf239a..9c0ca3906f 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -218,10 +218,10 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a 
     {γ : Type w} (f : (a : α) → β → γ → m (ForInStep γ)) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.forIn f init
 
-instance [BEq α] [Hashable α] {m : Type w → Type w'} : ForM m (HashMap α β) (α × β) where
+instance [BEq α] [Hashable α] {m : Type w → Type w'} [Monad m] : ForM m (HashMap α β) (α × β) where
   forM m f := m.forM (fun a b => f (a, b))
 
-instance [BEq α] [Hashable α] {m : Type w → Type w'} : ForIn m (HashMap α β) (α × β) where
+instance [BEq α] [Hashable α] {m : Type w → Type w'} [Monad m] : ForIn m (HashMap α β) (α × β) where
   forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init
 
 @[inline, inherit_doc DHashMap.filter] def filter (f : α → β → Bool)
diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean
index 585cd215c6..5d5983455c 100644
--- a/src/Std/Data/HashMap/Raw.lean
+++ b/src/Std/Data/HashMap/Raw.lean
@@ -219,10 +219,10 @@ instance [BEq α] [Hashable α] : GetElem? (Raw α β) α β (fun m a => a ∈ m
     (f : (a : α) → β → γ → m (ForInStep γ)) (init : γ) (b : Raw α β) : m γ :=
   b.inner.forIn f init
 
-instance {m : Type w → Type w'} : ForM m (Raw α β) (α × β) where
+instance {m : Type w → Type w'} [Monad m] : ForM m (Raw α β) (α × β) where
   forM m f := m.forM (fun a b => f (a, b))
 
-instance {m : Type w → Type w'} : ForIn m (Raw α β) (α × β) where
+instance {m : Type w → Type w'} [Monad m] : ForIn m (Raw α β) (α × β) where
   forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init
 
 @[inline, inherit_doc DHashMap.Raw.all] def all (m : Raw α β) (p : α → β → Bool) : Bool :=
diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean
index f59584ac4c..02a86d12e5 100644
--- a/src/Std/Data/HashSet/Basic.lean
+++ b/src/Std/Data/HashSet/Basic.lean
@@ -206,10 +206,10 @@ order.
     (f : α → β → m (ForInStep β)) (init : β) (b : HashSet α) : m β :=
   b.inner.forIn (fun a _ acc => f a acc) init
 
-instance [BEq α] [Hashable α] {m : Type v → Type w} : ForM m (HashSet α) α where
+instance [BEq α] [Hashable α] {m : Type v → Type w} [Monad m] : ForM m (HashSet α) α where
   forM m f := m.forM f
 
-instance [BEq α] [Hashable α] {m : Type v → Type w} : ForIn m (HashSet α) α where
+instance [BEq α] [Hashable α] {m : Type v → Type w} [Monad m] : ForIn m (HashSet α) α where
   forIn m init f := m.forIn f init
 
 /-- Removes all elements from the hash set for which the given function returns `false`. -/
diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean
index c314cbd87e..7bf2bfdd3f 100644
--- a/src/Std/Data/HashSet/Raw.lean
+++ b/src/Std/Data/HashSet/Raw.lean
@@ -207,10 +207,10 @@ order.
     (init : β) (b : Raw α) : m β :=
   b.inner.forIn (fun a _ acc => f a acc) init
 
-instance {m : Type v → Type w} : ForM m (Raw α) α where
+instance {m : Type v → Type w} [Monad m] : ForM m (Raw α) α where
   forM m f := m.forM f
 
-instance {m : Type v → Type w} : ForIn m (Raw α) α where
+instance {m : Type v → Type w} [Monad m] : ForIn m (Raw α) α where
   forIn m init f := m.forIn f init
 
 /-- Removes all elements from the hash set for which the given function returns `false`. -/
diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean
index 49e9d35f77..89085da941 100644
--- a/src/Std/Data/TreeMap/Basic.lean
+++ b/src/Std/Data/TreeMap/Basic.lean
@@ -419,10 +419,10 @@ def forM (f : α → β → m PUnit) (t : TreeMap α β cmp) : m PUnit :=
 def forIn (f : α → β → δ → m (ForInStep δ)) (init : δ) (t : TreeMap α β cmp) : m δ :=
   t.inner.forIn (fun a b c => f a b c) init
 
-instance : ForM m (TreeMap α β cmp) (α × β) where
+instance [Monad m] : ForM m (TreeMap α β cmp) (α × β) where
   forM t f := t.forM (fun a b => f ⟨a, b⟩)
 
-instance : ForIn m (TreeMap α β cmp) (α × β) where
+instance [Monad m] : ForIn m (TreeMap α β cmp) (α × β) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
 @[inline, inherit_doc DTreeMap.any]
diff --git a/src/Std/Data/TreeMap/Raw/Basic.lean b/src/Std/Data/TreeMap/Raw/Basic.lean
index d72813610e..4fd241f1b3 100644
--- a/src/Std/Data/TreeMap/Raw/Basic.lean
+++ b/src/Std/Data/TreeMap/Raw/Basic.lean
@@ -421,10 +421,10 @@ def forM (f : α → β → m PUnit) (t : Raw α β cmp) : m PUnit :=
 def forIn (f : α → β → δ → m (ForInStep δ)) (init : δ) (t : Raw α β cmp) : m δ :=
   t.inner.forIn (fun a b c => f a b c) init
 
-instance : ForM m (Raw α β cmp) (α × β) where
+instance [Monad m] : ForM m (Raw α β cmp) (α × β) where
   forM t f := t.forM (fun a b => f ⟨a, b⟩)
 
-instance : ForIn m (Raw α β cmp) (α × β) where
+instance [Monad m] : ForIn m (Raw α β cmp) (α × β) where
   forIn t init f := t.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
 @[inline, inherit_doc DTreeMap.Raw.any]
diff --git a/src/Std/Data/TreeSet/Basic.lean b/src/Std/Data/TreeSet/Basic.lean
index 31682b9ad3..7aa106c38f 100644
--- a/src/Std/Data/TreeSet/Basic.lean
+++ b/src/Std/Data/TreeSet/Basic.lean
@@ -421,10 +421,10 @@ order.
 def forIn (f : α → δ → m (ForInStep δ)) (init : δ) (t : TreeSet α cmp) : m δ :=
   t.inner.forIn (fun a _ c => f a c) init
 
-instance : ForM m (TreeSet α cmp) α where
+instance [Monad m] : ForM m (TreeSet α cmp) α where
   forM t f := t.forM f
 
-instance : ForIn m (TreeSet α cmp) α where
+instance [Monad m] : ForIn m (TreeSet α cmp) α where
   forIn m init f := m.forIn (fun a acc => f a acc) init
 
 /-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/
diff --git a/src/Std/Data/TreeSet/Raw/Basic.lean b/src/Std/Data/TreeSet/Raw/Basic.lean
index 427c634611..19d4b5f251 100644
--- a/src/Std/Data/TreeSet/Raw/Basic.lean
+++ b/src/Std/Data/TreeSet/Raw/Basic.lean
@@ -294,10 +294,10 @@ def forM (f : α → m PUnit) (t : Raw α cmp) : m PUnit :=
 def forIn (f : α → δ → m (ForInStep δ)) (init : δ) (t : Raw α cmp) : m δ :=
   t.inner.forIn (fun a _ c => f a c) init
 
-instance : ForM m (Raw α cmp) α where
+instance [Monad m] : ForM m (Raw α cmp) α where
   forM t f := t.forM f
 
-instance : ForIn m (Raw α cmp) α where
+instance [Monad m] : ForIn m (Raw α cmp) α where
   forIn t init f := t.forIn (fun a acc => f a acc) init
 
 @[inline, inherit_doc TreeSet.empty]
diff --git a/src/Std/Sync/Broadcast.lean b/src/Std/Sync/Broadcast.lean
index cd3dba37c9..1b363f433c 100644
--- a/src/Std/Sync/Broadcast.lean
+++ b/src/Std/Sync/Broadcast.lean
@@ -633,7 +633,7 @@ partial def forIn [Inhabited α] [Monad m] [MonadLiftT BaseIO m]
     | .yield b => ch.forIn f b
 
 /-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed. -/
-instance [Inhabited α] [MonadLiftT BaseIO m] : ForIn m (Sync.Receiver α) α where
+instance [Inhabited α] [Monad m] [MonadLiftT BaseIO m] : ForIn m (Sync.Receiver α) α where
   forIn ch b f := Receiver.forIn ch f b
 
 end Receiver
diff --git a/src/Std/Sync/Channel.lean b/src/Std/Sync/Channel.lean
index f1e6246c2e..a6fd56371f 100644
--- a/src/Std/Sync/Channel.lean
+++ b/src/Std/Sync/Channel.lean
@@ -813,7 +813,7 @@ private partial def forIn [Monad m] [MonadLiftT BaseIO m]
   | none => pure b
 
 /-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed. -/
-instance [MonadLiftT BaseIO m] : ForIn m (Sync α) α where
+instance [Monad m] [MonadLiftT BaseIO m] : ForIn m (Sync α) α where
   forIn ch b f := private ch.forIn f b
 
 end Sync
@@ -950,7 +950,7 @@ private partial def forIn [Inhabited α] [Monad m] [MonadLiftT BaseIO m]
   | .yield b => ch.forIn f b
 
 /-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed. -/
-instance [Inhabited α] [MonadLiftT BaseIO m] : ForIn m (Sync α) α where
+instance [Inhabited α] [Monad m] [MonadLiftT BaseIO m] : ForIn m (Sync α) α where
   forIn ch b f := private ch.forIn f b
 
 end Sync
diff --git a/src/lake/Lake/Util/OrdHashSet.lean b/src/lake/Lake/Util/OrdHashSet.lean
index fcbab48f41..25b8e9a221 100644
--- a/src/lake/Lake/Util/OrdHashSet.lean
+++ b/src/lake/Lake/Util/OrdHashSet.lean
@@ -73,4 +73,4 @@ public def ofArray (arr : Array α) : OrdHashSet α :=
 @[inline] public protected def forIn [Monad m] (self : OrdHashSet α) (init : β) (f : α → β → m (ForInStep β)) : m β :=
   ForIn.forIn self.toArray init f
 
-public instance : ForIn m (OrdHashSet α) α := ⟨OrdHashSet.forIn⟩
+public instance [Monad m] : ForIn m (OrdHashSet α) α := ⟨OrdHashSet.forIn⟩
diff --git a/src/lake/Lake/Util/RBArray.lean b/src/lake/Lake/Util/RBArray.lean
index da078d4bb0..6de919e713 100644
--- a/src/lake/Lake/Util/RBArray.lean
+++ b/src/lake/Lake/Util/RBArray.lean
@@ -68,7 +68,7 @@ public def insert (self : RBArray α β cmp) (a : α) (b : β) : RBArray α β c
   [Monad m] (self : RBArray α β cmp) (init : σ) (f : β → σ → m (ForInStep σ))
 : m σ := ForIn.forIn self.toArray init f
 
-instance : ForIn m (RBArray α β cmp) β := ⟨RBArray.forIn⟩
+instance [Monad m] : ForIn m (RBArray α β cmp) β := ⟨RBArray.forIn⟩
 
 end RBArray
 
diff --git a/tests/lean/run/6332.lean b/tests/lean/run/6332.lean
index 314081ec95..3fb60200eb 100644
--- a/tests/lean/run/6332.lean
+++ b/tests/lean/run/6332.lean
@@ -128,7 +128,7 @@ deriving Inhabited, BEq
 
 open Tile
 
-def solve (mat : Matrix Tile) (guard : Nat × Nat) := do
+def solve (mat : Matrix Tile) (guard : Nat × Nat) : IO Unit := do
   let mut mat := mat
   let mut pos := guard + (1 : Nat)
   let mut dir : Offset × Offset := (-1, 0)
diff --git a/tests/lean/run/discrTreeKey.lean b/tests/lean/run/discrTreeKey.lean
index a28d7a6bc2..71975e1c65 100644
--- a/tests/lean/run/discrTreeKey.lean
+++ b/tests/lean/run/discrTreeKey.lean
@@ -76,8 +76,8 @@ open Nat List
 #check List.instDecidableMemOfLawfulBEq
 #discr_tree_key List.instDecidableMemOfLawfulBEq
 
-#check List.instForIn'InferInstanceMembership
-#discr_tree_key List.instForIn'InferInstanceMembership
+#check List.instForIn'InferInstanceMembershipOfMonad
+#discr_tree_key List.instForIn'InferInstanceMembershipOfMonad
 
 /-!
   We can also specify a term directly.
diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean
index a7b3415510..a104505279 100644
--- a/tests/lean/run/doLogicTests.lean
+++ b/tests/lean/run/doLogicTests.lean
@@ -485,11 +485,11 @@ theorem test_match_splitting {m : Option Nat} (h : m = some 4) :
 
 theorem test_sum :
   ⦃⌜True⌝⦄
-  do
+  (do
     let mut x := 0
     for i in [1:5] do
       x := x + i
-    pure (f := Id) x
+    pure x : Id _)
   ⦃⇓r => ⌜r < 30⌝⦄ := by
   mvcgen
   case inv1 => exact (⇓ (xs, r) => ⌜r + xs.suffix.length * 5 ≤ 25⌝)
diff --git a/tests/lean/run/forInColErr.lean b/tests/lean/run/forInColErr.lean
index 8559893126..532e0e516a 100644
--- a/tests/lean/run/forInColErr.lean
+++ b/tests/lean/run/forInColErr.lean
@@ -15,7 +15,7 @@ example {c} := Id.run do
 
 /--
 error: don't know how to synthesize implicit argument `ρ`
-  @forIn Id (List ?_) ?_ instForInOfForIn' PUnit Id.instMonad [] PUnit.unit fun x r => do
+  @forIn Id (List ?_) ?_ instForInOfForIn' PUnit [] PUnit.unit fun x r => do
     pure ()
     pure (ForInStep.yield PUnit.unit)
 context:
@@ -48,16 +48,16 @@ example {c} := Id.run do
 
 /--
 error: don't know how to synthesize implicit argument `d`
-  @forIn' Id (List ?_) ?_ inferInstance List.instForIn'InferInstanceMembership PUnit Id.instMonad [] PUnit.unit
-    fun x h r => do
+  @forIn' Id (List ?_) ?_ inferInstance List.instForIn'InferInstanceMembershipOfMonad PUnit [] PUnit.unit fun x h r =>
+    do
     pure ()
     pure (ForInStep.yield PUnit.unit)
 context:
 ⊢ outParam (Membership ?_ (List ?_))
 ---
 error: don't know how to synthesize implicit argument `ρ`
-  @forIn' Id (List ?_) ?_ inferInstance List.instForIn'InferInstanceMembership PUnit Id.instMonad [] PUnit.unit
-    fun x h r => do
+  @forIn' Id (List ?_) ?_ inferInstance List.instForIn'InferInstanceMembershipOfMonad PUnit [] PUnit.unit fun x h r =>
+    do
     pure ()
     pure (ForInStep.yield PUnit.unit)
 context:
diff --git a/tests/lean/run/partial_fixpoint_monotonicity.lean b/tests/lean/run/partial_fixpoint_monotonicity.lean
index d3513a2055..3de0baafbb 100644
--- a/tests/lean/run/partial_fixpoint_monotonicity.lean
+++ b/tests/lean/run/partial_fixpoint_monotonicity.lean
@@ -23,7 +23,7 @@ example : monotone (fun (f : Option Unit) => do {do f; f; f}) := by
 
 example : monotone
   (fun (f : Nat → Option Unit) => do
-    for x in [1,2,3] do f x) := by
+    for x in [1,2,3] do f x : _ → Option _) := by
   repeat' monotonicity
 
 example : monotone
@@ -33,5 +33,5 @@ example : monotone
       acc := acc + (← f x)
       if acc > 10 then
         return 5
-    pure acc) := by
+    pure acc : _ → Option _) := by
   repeat' monotonicity