From 1ebf69e1634a75901bf9f47b7aeec6c8fc624072 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 12 Jan 2021 06:41:32 -0800
Subject: [PATCH] fix: simple-match macro

---
 src/Lean/Elab/Match.lean            | 25 +++++++++++++++++++++----
 tests/lean/patvar.lean              | 17 +++++++++++++++++
 tests/lean/patvar.lean.expected.out |  6 ++++++
 3 files changed, 44 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/patvar.lean
 create mode 100644 tests/lean/patvar.lean.expected.out

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index bd4d44b85c0c..58fb4544f04c 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -862,12 +862,29 @@ private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermEla
   let matchOptType := getMatchOptType stx
   elabMatchAux discrStxs altViews matchOptType expectedType
 
+private def isPatternVar (stx : Syntax) : TermElabM Bool := do
+  match (← resolveId? stx "pattern") with
+  | none   => isAtomicIdent stx
+  | some f => match f with
+    | Expr.const fName _ _ =>
+      match (← getEnv).find? fName with
+      | some (ConstantInfo.ctorInfo _) => return false
+      | _ => isAtomicIdent stx
+    | _ => isAtomicIdent stx
+where
+  isAtomicIdent (stx : Syntax) : Bool :=
+    stx.isIdent && stx.getId.eraseMacroScopes.isAtomic
+
 -- parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
-@[builtinTermElab «match»] def elabMatch : TermElab := fun stx expectedType? =>
+@[builtinTermElab «match»] def elabMatch : TermElab := fun stx expectedType? => do
   match stx with
-  | `(match $discr:term with | $y:ident => $rhs:term)         => expandSimpleMatch stx discr y rhs expectedType?
-  | `(match $discr:term : $type with | $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
-  | _ => do
+  | `(match $discr:term with | $y:ident => $rhs:term) =>
+     if (← isPatternVar y) then expandSimpleMatch stx discr y rhs expectedType? else elabMatchDefault stx expectedType?
+  | `(match $discr:term : $type with | $y:ident => $rhs:term) =>
+     if (← isPatternVar y) then expandSimpleMatchWithType stx discr y type rhs expectedType? else elabMatchDefault stx expectedType?
+  | _ => elabMatchDefault stx expectedType?
+where
+  elabMatchDefault (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
     match (← expandNonAtomicDiscrs? stx) with
     | some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
     | none =>
diff --git a/tests/lean/patvar.lean b/tests/lean/patvar.lean
new file mode 100644
index 000000000000..1ed25c3b723b
--- /dev/null
+++ b/tests/lean/patvar.lean
@@ -0,0 +1,17 @@
+-- set_option trace.Elab true
+def myId : List α → List α
+| List.nil => List.nil
+
+def constNil : List α → List α
+| List.nil => List.nil
+| List.cons x y => List.nil
+
+def failing1 : List α → List α
+| [] => List.nil
+
+def failing2 : List α → List α
+| x => List.nil
+| foo.bar => List.nil -- "invalid pattern variable"
+
+def myId2 : List α → List α
+| foo.bar => foo.bar
diff --git a/tests/lean/patvar.lean.expected.out b/tests/lean/patvar.lean.expected.out
new file mode 100644
index 000000000000..4e19d59da404
--- /dev/null
+++ b/tests/lean/patvar.lean.expected.out
@@ -0,0 +1,6 @@
+patvar.lean:3:0: error: missing cases:
+(List.cons _ _)
+patvar.lean:10:0: error: missing cases:
+(List.cons _ _)
+patvar.lean:14:0: error: invalid pattern variable, must be atomic
+patvar.lean:17:0: error: invalid pattern variable, must be atomic