From fdbe893c408bb5360e802d2e39a2a6d9eb125a2b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Mar 2022 17:34:04 -0700
Subject: [PATCH] fix: catch `mkAppM` exceptions

---
 src/Lean/Elab/Extra.lean         |  2 +-
 tests/lean/run/forInElabBug.lean | 17 +++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/forInElabBug.lean

diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 52e48f9a22..65460b0fb9 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/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}"
diff --git a/tests/lean/run/forInElabBug.lean b/tests/lean/run/forInElabBug.lean
new file mode 100644
index 0000000000..e238290555
--- /dev/null
+++ b/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