try fix

Author: datokrat

src/Lean/Elab/Extra.lean

@@ -55,7 +55,7 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
   match stx with
   | `(for_in'% $col $init $body) =>
         tryPostponeIfNoneOrMVar expectedType?
-        let colE ← elabTerm col none
+        let colE ← withSynthesizeLight (elabTerm col none)
         let m ← getMonadForIn expectedType?
         let colType ← inferType colE
         let elemType ← mkFreshExprMVar (mkSort (mkLevelSucc (← mkFreshLevelMVar)))
@@ -65,6 +65,7 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
             mkAppM ``ForIn' #[m, colType, elemType, memType]
           catch _ =>
             tryPostpone; throwError "failed to construct `ForIn'` instance for collection{indentExpr colType}\nand monad{indentExpr m}"
+        synthesizeSyntheticMVarsUsingDefault
         match (← trySynthInstance forInInstance) with
         | .some inst  =>
           let forInFn ← mkConst ``forIn'

tests/lean/run/rangePolymorphic.lean

@@ -57,6 +57,10 @@ def h (n : Nat) : IO Unit := do
   for i in *...n, j in 2...* do
     IO.println s!"i={i}, j={j}"
 
+example : Unit := Id.run do
+  for _h : _i in 4...<12 do
+    pure .unit
+
 /--
 info: i=0, j=2
 i=1, j=3