feat: introduce MonadLiftT Id m (#8977)

This PR adds a generic `MonadLiftT Id m` instance. We do not implement a
`MonadLift Id m` instance because it would slow down instance resolution
and because it would create more non-canonical instances. This change
makes it possible to iterate over a pure iterator, such as `[1, 2,
3].iter`, in arbitrary monads.

src/Init/Control/Id.lean

@@ -62,4 +62,7 @@ protected def run (x : Id α) : α := x
 instance [OfNat α n] : OfNat (Id α) n :=
   inferInstanceAs (OfNat α n)
 
+instance {m : Type u → Type v} [Pure m] : MonadLiftT Id m where
+  monadLift x := pure x.run
+
 end Id

src/Init/Control/Lawful/MonadLift/Instances.lean

@@ -11,6 +11,7 @@ import all Init.Control.Except
 import all Init.Control.ExceptCps
 import all Init.Control.StateRef
 import all Init.Control.StateCps
+import all Init.Control.Id
 import Init.Control.Lawful.MonadLift.Lemmas
 import Init.Control.Lawful.Instances
 
@@ -135,3 +136,11 @@ instance {ε : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (ExceptCpsT
     simp only [bind_assoc]
 
 end ExceptCpsT
+
+namespace Id
+
+instance [Monad m] [LawfulMonad m] : LawfulMonadLiftT Id m where
+  monadLift_pure a := by simp [monadLift]
+  monadLift_bind a f := by simp [monadLift]
+
+end Id

src/Init/Data/Iterators/Consumers/Loop.lean

@@ -47,7 +47,6 @@ instance (α : Type w) (β : Type w) (n : Type w → Type w') [Monad n]
     [Iterator α Id β] [IteratorLoopPartial α Id n] :
     ForIn n (Iter.Partial (α := α) β) β where
   forIn it init f :=
-    letI : MonadLift Id n := ⟨pure⟩
     ForIn.forIn it.it.toIterM.allowNontermination init f
 
 instance {m : Type w → Type w'}

src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean

@@ -42,7 +42,6 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
     {f : (out : β) → _ → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     ForIn'.forIn' it init f =
-      letI : MonadLift Id m := ⟨Std.Internal.idToMonad (α := _)⟩
       letI : ForIn' m (IterM (α := α) Id β) β _ := IterM.instForIn'
       ForIn'.forIn' it.toIterM init
         (fun out h acc => f out (isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
@@ -54,7 +53,6 @@ theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : β → γ → m (ForInStep γ)} :
     ForIn.forIn it init f =
-      letI : MonadLift Id m := ⟨Std.Internal.idToMonad (α := _)⟩
       ForIn.forIn it.toIterM init f := by
   rfl
 
@@ -197,7 +195,7 @@ theorem Iter.foldM_eq_foldM_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     {γ : Type w} {it : Iter (α := α) β} {init : γ} {f : γ → β → m γ} :
-    it.foldM (init := init) f = letI : MonadLift Id m := ⟨pure⟩; it.toIterM.foldM (init := init) f :=
+    it.foldM (init := init) f = it.toIterM.foldM (init := init) f :=
   (rfl)
 
 theorem Iter.forIn_yield_eq_foldM {α β γ δ : Type w} [Iterator α Id β]

src/Std/Data/Iterators/Lemmas/Combinators/FilterMap.lean

@@ -142,7 +142,6 @@ theorem Iter.step_filterMapM {β' : Type w} {f : β → n (Option β')}
   generalize it.toIterM.step = step
   match step with
   | .yield it' out h =>
-    simp only
     apply bind_congr
     intro step
     rcases step with _ | _ <;> rfl

src/Std/Data/Iterators/Lemmas/Producers/Empty.lean

@@ -40,11 +40,6 @@ theorem Iter.forIn_empty {m β γ} [Monad m] [LawfulMonad m]
     {init : γ} {f} :
     ForIn.forIn (m := m) (Iter.empty β) init f = pure init := by
   simp [Iter.forIn_eq_forIn_toIterM]
-  letI : MonadLift Id m := ⟨Internal.idToMonad (α := _)⟩
-  letI := Internal.LawfulMonadLiftFunction.idToMonad (m := m)
-  haveI : LawfulMonadLiftT Id m := inferInstance
-  rw [IterM.forIn_empty]
-
 
 @[simp]
 theorem Iter.foldM_empty {m β γ} [Monad m] [LawfulMonad m]

tests/lean/run/iterators.lean

@@ -122,6 +122,22 @@ example (l : List Nat) :
     return s) = l.iter.fold (init := 0) (· + ·) := by
   simp
 
+def forInIO (l : List Nat) : IO Nat := do
+  let mut s := 0
+  for x in l.iter do
+    IO.println s!"adding {x}"
+    s := s + x
+  return s
+
+/--
+info: adding 1
+adding 2
+---
+info: 3
+-/
+#guard_msgs in
+#eval forInIO [1, 2]
+
 end Loop
 
 section Take