From 7c809a94aff170207f6e2f45f194946575dca94d Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 8 Feb 2025 11:32:34 +0100
Subject: [PATCH] refactor: elaborate forIn notation without extra let (#6977)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR avoids a `let` in the elaboration of `forIn`. It was introduced
in https://github.com/leanprover/lean4/commit/f51328ff112 but nothing
seems to break when I simplify the code. This removes an unexpected `let
col✝ :=…` from the “Expected type” view in the Info View and from the
termination proofs.
---
 src/Lean/Elab/Extra.lean        | 16 +++----
 tests/lean/run/forInColErr.lean | 79 +++++++++++++++++++++++++++++++++
 2 files changed, 85 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/run/forInColErr.lean

diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 61edbb147a..9aab4b8135 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -26,12 +26,10 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
 @[builtin_term_elab forInMacro] def elabForIn : TermElab :=  fun stx expectedType? => do
   match stx with
   | `(for_in% $col $init $body) =>
-      match (← isLocalIdent? col) with
-      | none   => elabTerm (← `(let col := $col; for_in% col $init $body)) expectedType?
-      | some colFVar =>
         tryPostponeIfNoneOrMVar expectedType?
+        let colE ← elabTerm col none
         let m ← getMonadForIn expectedType?
-        let colType ← inferType colFVar
+        let colType ← inferType colE
         let elemType ← mkFreshExprMVar (mkSort (mkLevelSucc (← mkFreshLevelMVar)))
         let forInInstance ← try
           mkAppM ``ForIn #[m, colType, elemType]
@@ -42,7 +40,7 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
           let forInFn ← mkConst ``forIn
           elabAppArgs forInFn
             (namedArgs := #[{ name := `m, val := Arg.expr m}, { name := `α, val := Arg.expr elemType }, { name := `self, val := Arg.expr inst }])
-            (args := #[Arg.stx col, Arg.stx init, Arg.stx body])
+            (args := #[Arg.expr colE, Arg.stx init, Arg.stx body])
             (expectedType? := expectedType?)
             (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
         | .undef    => tryPostpone; throwForInFailure forInInstance
@@ -52,12 +50,10 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
 @[builtin_term_elab forInMacro'] def elabForIn' : TermElab :=  fun stx expectedType? => do
   match stx with
   | `(for_in'% $col $init $body) =>
-      match (← isLocalIdent? col) with
-      | none   => elabTerm (← `(let col := $col; for_in'% col $init $body)) expectedType?
-      | some colFVar =>
         tryPostponeIfNoneOrMVar expectedType?
+        let colE ← elabTerm col none
         let m ← getMonadForIn expectedType?
-        let colType ← inferType colFVar
+        let colType ← inferType colE
         let elemType ← mkFreshExprMVar (mkSort (mkLevelSucc (← mkFreshLevelMVar)))
         let forInInstance ←
           try
@@ -70,7 +66,7 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
           let forInFn ← mkConst ``forIn'
           elabAppArgs forInFn
             (namedArgs := #[{ name := `m, val := Arg.expr m}, { name := `α, val := Arg.expr elemType}, { name := `self, val := Arg.expr inst }])
-            (args := #[Arg.expr colFVar, Arg.stx init, Arg.stx body])
+            (args := #[Arg.expr colE, Arg.stx init, Arg.stx body])
             (expectedType? := expectedType?)
             (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
         | .undef    => tryPostpone; throwForInFailure forInInstance
diff --git a/tests/lean/run/forInColErr.lean b/tests/lean/run/forInColErr.lean
new file mode 100644
index 0000000000..f75ecf3673
--- /dev/null
+++ b/tests/lean/run/forInColErr.lean
@@ -0,0 +1,79 @@
+set_option pp.mvars.anonymous false
+
+/--
+error: failed to construct 'ForIn' instance for collection
+  ?_
+and monad
+  Id
+-/
+#guard_msgs in
+example {c} := Id.run do
+  for x in c do
+    pure ()
+  pure ()
+
+
+/--
+error: don't know how to synthesize implicit argument 'ρ'
+  @forIn Id (List ?_) ?_ instForInOfForIn' PUnit Id.instMonad [] PUnit.unit fun x r => do
+    pure ()
+    pure (ForInStep.yield PUnit.unit)
+context:
+⊢ Type _
+---
+error: failed to infer binder type
+---
+error: don't know how to synthesize implicit argument 'α'
+  @List.nil ?_
+context:
+⊢ Type _
+-/
+#guard_msgs in
+example : Unit := Id.run do
+  for x in [] do
+    pure ()
+  pure ()
+
+/--
+error: failed to construct `ForIn'` instance for collection
+  ?_
+and monad
+  Id
+-/
+#guard_msgs in
+example {c} := Id.run do
+  for h : x in c do
+    pure ()
+  pure ()
+
+/--
+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
+    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
+    pure ()
+    pure (ForInStep.yield PUnit.unit)
+context:
+⊢ Type _
+---
+error: failed to infer binder type
+---
+error: failed to infer binder type
+---
+error: don't know how to synthesize implicit argument 'α'
+  @List.nil ?_
+context:
+⊢ Type _
+-/
+#guard_msgs in
+example : Unit := Id.run do
+  for h : x in [] do
+    pure ()
+  pure ()