feat: improve forIn elaborator element type propagation

src/Lean/Elab/Extra.lean

@@ -38,9 +38,13 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
         catch _ =>
           tryPostpone; throwError "failed to construct 'ForIn' instance for collection{indentExpr colType}\nand monad{indentExpr m}"
         match (← trySynthInstance forInInstance) with
-        | LOption.some _   =>
+        | LOption.some inst =>
           let forInFn ← mkConst ``forIn
-          elabAppArgs forInFn #[] #[Arg.stx col, Arg.stx init, Arg.stx body] expectedType? (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
+          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])
+            (expectedType? := expectedType?)
+            (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
         | LOption.undef    => tryPostpone; throwForInFailure forInInstance
         | LOption.none     => throwForInFailure forInInstance
   | _ => throwUnsupportedSyntax
@@ -62,9 +66,13 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
           catch _ =>
             tryPostpone; throwError "failed to construct `ForIn'` instance for collection{indentExpr colType}\nand monad{indentExpr m}"
         match (← trySynthInstance forInInstance) with
-        | LOption.some _   =>
+        | LOption.some inst  =>
           let forInFn ← mkConst ``forIn'
-          elabAppArgs forInFn #[] #[Arg.expr colFVar, Arg.stx init, Arg.stx body] expectedType? (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
+          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])
+            (expectedType? := expectedType?)
+            (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
         | LOption.undef    => tryPostpone; throwForInFailure forInInstance
         | LOption.none     => throwForInFailure forInInstance
   | _ => throwUnsupportedSyntax

tests/lean/linterUnusedVariables.lean.expected.out

@@ -12,8 +12,8 @@ linterUnusedVariables.lean:50:11-50:12: warning: unused variable `z`
 linterUnusedVariables.lean:55:14-55:15: warning: unused variable `y`
 linterUnusedVariables.lean:61:20-61:21: warning: unused variable `y`
 linterUnusedVariables.lean:66:34-66:38: warning: unused variable `inst`
-linterUnusedVariables.lean:107:25-107:26: warning: unused variable `x`
 linterUnusedVariables.lean:108:6-108:7: warning: unused variable `y`
+linterUnusedVariables.lean:107:25-107:26: warning: unused variable `x`
 linterUnusedVariables.lean:114:6-114:7: warning: unused variable `a`
 linterUnusedVariables.lean:124:26-124:27: warning: unused variable `z`
 linterUnusedVariables.lean:132:9-132:10: warning: unused variable `h`

tests/lean/run/coeOutParamIssue2.lean

@@ -1,3 +1,4 @@
+namespace Ex
 class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
   getElem (xs : Cont) (i : Idx) : Elem
 
@@ -12,3 +13,4 @@ opaque g : Bool → Bool
 def bad (xs : Array Bool) : Bool :=
   let x := getElem xs 0
   f x && g x
+end Ex

tests/lean/run/forOutParamIssue.lean

@@ -0,0 +1,22 @@
+namespace Ex
+class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
+  getElem (xs : Cont) (i : Idx) : Elem
+
+export GetElem (getElem)
+
+instance : GetElem (Array α) Nat α where
+  getElem xs i := xs.get ⟨i, sorry⟩
+
+opaque f : Option Bool → Id Unit
+
+def bad2 (bs : Array Bool) (n : Nat) : Id Unit := do
+  for idx in [:n] do
+    let b  := getElem bs idx
+    f b
+
+def bad3 (bs : Array Bool) (n : Nat) : Id Unit := do
+  for h : idx in [:n] do
+    let b  := getElem bs idx
+    f b
+
+end Ex