Make conversions between X and Id X explicit in definitions

This is free at runtime, since both `Id.run` and `pure` are inlined.

Author: eric-wieser

src/Init/Data/Array/Basic.lean

@@ -356,7 +356,7 @@ def modifyM [Monad m] (xs : Array α) (i : Nat) (f : α → m α) : m (Array α)
 
 @[inline]
 def modify (xs : Array α) (i : Nat) (f : α → α) : Array α :=
-  Id.run <| modifyM xs i f
+  Id.run <| modifyM xs i (pure <| f ·)
 
 set_option linter.indexVariables false in -- Changing `idx` causes bootstrapping issues, haven't investigated.
 @[inline]
@@ -646,11 +646,11 @@ def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit)
 
 @[inline]
 def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start := 0) (stop := as.size) : β :=
-  Id.run <| as.foldlM f init start stop
+  Id.run <| as.foldlM (pure <| f · ·) init start stop
 
 @[inline]
 def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start := as.size) (stop := 0) : β :=
-  Id.run <| as.foldrM f init start stop
+  Id.run <| as.foldrM (pure <| f · ·) init start stop
 
 /-- Sum of an array.
 
@@ -669,19 +669,19 @@ def count {α : Type u} [BEq α] (a : α) (as : Array α) : Nat :=
 
 @[inline]
 def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
-  Id.run <| as.mapM f
+  Id.run <| as.mapM (pure <| f ·)
 
 instance : Functor Array where
   map := map
 
 /-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/
 @[inline]
 def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) : Array β :=
-  Id.run <| as.mapFinIdxM f
+  Id.run <| as.mapFinIdxM (pure <| f · · ·)
 
 @[inline]
 def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) : Array β :=
-  Id.run <| as.mapIdxM f
+  Id.run <| as.mapIdxM (pure <| f · ·)
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
 def zipIdx (xs : Array α) (start := 0) : Array (α × Nat) :=
@@ -699,7 +699,7 @@ def find? {α : Type u} (p : α → Bool) (as : Array α) : Option α :=
 
 @[inline]
 def findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
-  Id.run <| as.findSomeM? f
+  Id.run <| as.findSomeM? (pure <| f ·)
 
 @[inline]
 def findSome! {α : Type u} {β : Type v} [Inhabited β] (f : α → Option β) (xs : Array α) : β :=
@@ -709,11 +709,11 @@ def findSome! {α : Type u} {β : Type v} [Inhabited β] (f : α → Option β)
 
 @[inline]
 def findSomeRev? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
-  Id.run <| as.findSomeRevM? f
+  Id.run <| as.findSomeRevM? (pure <| f ·)
 
 @[inline]
 def findRev? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
-  Id.run <| as.findRevM? p
+  Id.run <| as.findRevM? (pure <| p ·)
 
 @[inline]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
@@ -785,11 +785,11 @@ def getIdx? [BEq α] (xs : Array α) (v : α) : Option Nat :=
 
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
-  Id.run <| as.anyM p start stop
+  Id.run <| as.anyM (pure <| p ·) start stop
 
 @[inline]
 def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
-  Id.run <| as.allM p start stop
+  Id.run <| as.allM (pure <| p ·) start stop
 
 /-- `as.contains a` is true if there is some element `b` in `as` such that `a == b`. -/
 def contains [BEq α] (as : Array α) (a : α) : Bool :=
@@ -886,7 +886,7 @@ def filterMapM [Monad m] (f : α → m (Option β)) (as : Array α) (start := 0)
 
 @[inline]
 def filterMap (f : α → Option β) (as : Array α) (start := 0) (stop := as.size) : Array β :=
-  Id.run <| as.filterMapM f (start := start) (stop := stop)
+  Id.run <| as.filterMapM (pure <| f ·) (start := start) (stop := stop)
 
 @[specialize]
 def getMax? (as : Array α) (lt : α → α → Bool) : Option α :=

src/Init/Data/Array/BasicAux.lean

@@ -73,4 +73,4 @@ if the result of each `f a` is a pointer equal value `a`.
   as.mapM f
 
 @[inline] def Array.mapMono (as : Array α) (f : α → α) : Array α :=
-  Id.run <| as.mapMonoM f
+  Id.run <| as.mapMonoM (pure <| f ·)

src/Init/Data/Array/BinSearch.lean

@@ -82,6 +82,6 @@ termination_by lo hi => hi.1 - lo.1
   else binInsertAux lt merge add as k ⟨0, by omega⟩ ⟨as.size - 1, by omega⟩ (by simp) (by simpa using h')
 
 @[inline] def binInsert {α : Type u} (lt : α → α → Bool) (as : Array α) (k : α) : Array α :=
-  Id.run <| binInsertM lt (fun _ => k) (fun _ => k) as k
+  Id.run <| binInsertM lt (fun _ => pure k) (fun _ => pure k) as k
 
 end Array

src/Init/Data/Array/Subarray.lean

@@ -114,19 +114,19 @@ def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit)
 
 @[inline]
 def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
-  Id.run <| as.foldlM f (init := init)
+  Id.run <| as.foldlM (pure <| f · ·) (init := init)
 
 @[inline]
 def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Subarray α) : β :=
-  Id.run <| as.foldrM f (init := init)
+  Id.run <| as.foldrM (pure <| f · ·) (init := init)
 
 @[inline]
 def any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
-  Id.run <| as.anyM p
+  Id.run <| as.anyM (pure <| p ·)
 
 @[inline]
 def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
-  Id.run <| as.allM p
+  Id.run <| as.allM (pure <| p ·)
 
 @[inline]
 def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) : m (Option β) :=
@@ -148,7 +148,7 @@ def findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Subarray α) (p
 
 @[inline]
 def findRev? {α : Type} (as : Subarray α) (p : α → Bool) : Option α :=
-  Id.run <| as.findRevM? p
+  Id.run <| as.findRevM? (pure <| p ·)
 
 end Subarray
 

src/Init/Data/ByteArray/Basic.lean

@@ -199,7 +199,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
 
 @[inline]
 def foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β :=
-  Id.run <| as.foldlM f init start stop
+  Id.run <| as.foldlM (pure <| f · ·) init start stop
 
 /-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
 

src/Init/Data/FloatArray/Basic.lean

@@ -160,7 +160,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float →
 
 @[inline]
 def foldl {β : Type v} (f : β → Float → β) (init : β) (as : FloatArray) (start := 0) (stop := as.size) : β :=
-  Id.run <| as.foldlM f init start stop
+  Id.run <| as.foldlM (pure <| f · ·) init start stop
 
 end FloatArray
 

src/Init/Data/List/BasicAux.lean

@@ -208,7 +208,7 @@ if the result of each `f a` is a pointer equal value `a`.
   | a :: as => return (← f a) :: (← mapMonoM as f)
 
 def mapMono (as : List α) (f : α → α) : List α :=
-  Id.run <| as.mapMonoM f
+  Id.run <| as.mapMonoM (pure <| f ·)
 
 /-! ## Additional lemmas required for bootstrapping `Array`. -/
 

src/Init/Meta.lean

@@ -1211,7 +1211,7 @@ def filterSepElemsM {m : Type → Type} [Monad m] (a : Array Syntax) (p : Syntax
   filterSepElemsMAux a p 0 #[]
 
 def filterSepElems (a : Array Syntax) (p : Syntax → Bool) : Array Syntax :=
-  Id.run <| a.filterSepElemsM p
+  Id.run <| a.filterSepElemsM (pure <| p ·)
 
 private partial def mapSepElemsMAux {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax → m Syntax) (i : Nat) (acc : Array Syntax) : m (Array Syntax) := do
   if h : i < a.size then
@@ -1228,7 +1228,7 @@ def mapSepElemsM {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax 
   mapSepElemsMAux a f 0 #[]
 
 def mapSepElems (a : Array Syntax) (f : Syntax → Syntax) : Array Syntax :=
-  Id.run <| a.mapSepElemsM f
+  Id.run <| a.mapSepElemsM (pure <| f ·)
 
 end Array
 

src/Lean/Compiler/LCNF/FVarUtil.lean

@@ -205,9 +205,9 @@ where
     if !(← f fvar) then failure
 
 def anyFVar [TraverseFVar α] (f : FVarId → Bool) (x : α) : Bool :=
-  Id.run <| anyFVarM f x
+  Id.run <| anyFVarM (pure <| f ·) x
 
 def allFVar [TraverseFVar α] (f : FVarId → Bool) (x : α) : Bool :=
-  Id.run <| allFVarM f x
+  Id.run <| allFVarM (pure <| f ·) x
 
 end Lean.Compiler.LCNF

src/Lean/Data/AssocList.lean

@@ -38,7 +38,7 @@ def isEmpty : AssocList α β → Bool
     foldlM f d es
 
 @[inline] def foldl (f : δ → α → β → δ) (init : δ) (as : AssocList α β) : δ :=
-  Id.run (foldlM f init as)
+  Id.run (foldlM (pure <| f · · ·) init as)
 
 def toList (as : AssocList α β) : List (α × β) :=
   as.foldl (init := []) (fun r a b => (a, b)::r) |>.reverse