From c1231b1b43fd77cd0e304599057e6161b3cda02e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 22 Feb 2021 11:08:45 -0800
Subject: [PATCH] fix: fixes #317

BTW, I had to add the auxiliary `loop` fuction to workaround a bug in the
old compiler C++ code.

cc @Kha
---
 src/Lean/Elab/Binders.lean | 38 +++++++++++++++++++++-----------------
 1 file changed, 21 insertions(+), 17 deletions(-)

diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 2754bee52e..0da728b456 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -477,23 +477,27 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
       `(@fun $x => $body)
   loop (getMatchAltsNumPatterns matchAlts) #[]
 
-@[builtinTermElab «fun»] def elabFun : TermElab := fun stx expectedType? => match stx with
-  | `(fun $binders* => $body) => do
-    let (binders, body, expandedPattern) ← expandFunBinders binders body
-    if expandedPattern then
-      let newStx ← `(fun $binders* => $body)
-      withMacroExpansion stx newStx <| elabTerm newStx expectedType?
-    else
-      elabFunBinders binders expectedType? fun xs expectedType? => do
-        /- We ensure the expectedType here since it will force coercions to be applied if needed.
-           If we just use `elabTerm`, then we will need to a coercion `Coe (α → β) (α → δ)` whenever there is a coercion `Coe β δ`,
-           and another instance for the dependent version. -/
-        let e ← elabTermEnsuringType body expectedType?
-        mkLambdaFVars xs e
-  | `(fun $m:matchAlts) => do
-    let stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx m
-    withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
-  | _ => throwUnsupportedSyntax
+@[builtinTermElab «fun»] partial def elabFun : TermElab :=
+  fun stx expectedType? => loop stx expectedType?
+where
+  loop (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
+    match stx with
+    | `(fun $binders* => $body) => do
+      let (binders, body, expandedPattern) ← expandFunBinders binders body
+      if expandedPattern then
+        let newStx ← `(fun $binders* => $body)
+        loop newStx expectedType?
+      else
+        elabFunBinders binders expectedType? fun xs expectedType? => do
+          /- We ensure the expectedType here since it will force coercions to be applied if needed.
+             If we just use `elabTerm`, then we will need to a coercion `Coe (α → β) (α → δ)` whenever there is a coercion `Coe β δ`,
+             and another instance for the dependent version. -/
+          let e ← elabTermEnsuringType body expectedType?
+          mkLambdaFVars xs e
+    | `(fun $m:matchAlts) => do
+      let stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx m
+      withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+    | _ => throwUnsupportedSyntax
 
 /- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created.
    Otherwise, we create a term of the form `(fun (x : type) => body) val`