fix: for result type

src/Lean/Elab/Do.lean

@@ -843,8 +843,8 @@ ctx ← read;
 u ← mkUVarTuple ref;
 match ctx.kind with
 | Kind.regular         => if ctx.uvars.isEmpty then pure action else `(HasBind.bind $action fun y => HasPure.pure (y, $u))
-| Kind.forIn           => `(HasBind.bind $action fun _ => HasPure.pure (ForInStep.yield $u))
-| Kind.forInWithReturn => `(HasBind.bind $action fun _ => HasPure.pure (ForInStep.yield (none, $u)))
+| Kind.forIn           => `(HasBind.bind $action fun (_ : PUnit) => HasPure.pure (ForInStep.yield $u))
+| Kind.forInWithReturn => `(HasBind.bind $action fun (_ : PUnit) => HasPure.pure (ForInStep.yield (none, $u)))
 | Kind.nestedBC        => unreachable!
 | Kind.nestedPR        => `(HasBind.bind $action fun y => (HasPure.pure (DoResultPR.«pure» y $u)))
 | Kind.nestedSBC       => `(HasBind.bind $action fun y => (HasPure.pure (DoResultSBC.«pureReturn» y $u)))

tests/lean/run/forBodyResultTypeIssue.lean

@@ -0,0 +1,17 @@
+new_frontend
+
+abbrev M := ExceptT String $ StateT Nat Id
+
+def f (xs : List Nat) : M Unit := do
+for x in xs do
+  if x == 0 then
+    throw "contains zero"
+
+#eval f [1, 2, 3] $.run' 0
+#eval f [1, 0, 3] $.run' 0
+
+theorem ex1 : f [1, 2, 3] $.run' 0 = Except.ok () :=
+rfl
+
+theorem ex2 : f [1, 0, 3] $.run' 0 = Except.error "contains zero" :=
+rfl