fix: catch mkAppM exceptions

src/Lean/Elab/Extra.lean

@@ -103,9 +103,9 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
         let m ← getMonadForIn expectedType?
         let colType ← inferType colFVar
         let elemType ← mkFreshExprMVar (mkSort (mkLevelSucc (← mkFreshLevelMVar)))
-        let memType ← mkFreshExprMVar (← mkAppM ``Membership #[elemType, colType])
         let forInInstance ←
           try
+            let memType ← mkFreshExprMVar (← mkAppM ``Membership #[elemType, colType])
             mkAppM ``ForIn' #[m, colType, elemType, memType]
           catch
             ex => tryPostpone; throwError "failed to construct `ForIn'` instance for collection{indentExpr colType}\nand monad{indentExpr m}"

tests/lean/run/forInElabBug.lean

@@ -0,0 +1,17 @@
+import Std
+
+namespace Std.BinomialHeapImp
+
+open Heap
+
+partial def toArrayUnordered' (h : Heap α) : Array α :=
+  go #[] h
+where
+    go (acc : Array α) : Heap α → Array α
+      | heap ns => Id.run do
+        let mut acc := acc
+        for h₁ : n in ns do
+          acc := acc.push n.val
+          for h₂ : h in n.children do
+            acc := go acc h
+        return acc