From 145bd5090334582355d2efc0b32fd204ccbe1e01 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 26 Jan 2020 14:55:55 -0800
Subject: [PATCH] feat: disallow patterns with `choice` nodes

@Kha Patterns with nested "choice" nodes produce counterintuitive
behavior, and hard to understand errors. They only work when we have
the exact same overloads at macro definition and application time.

Here is a funky example
```
syntax [myAdd] term "++":65 term:65 : term    -- overloads "++"
/- The following `macro_rules` manages to eliminate "choice" node by using the
   explicitly provided node kind. -/
macro_rules [myAdd] `($a ++ $b) => `($a + $b)

check (1:Nat) ++ 2 -- works as expected

syntax "FOO!" term : term

/- Before this commit, the following pattern was accepted,
   and it contained a "choice" node for `++`. It is a `myAdd` or
   `HasAppend.append`.

   Now, this kind of pattern is rejected since it contains a nested
   "choice" -/
macro_rules `(FOO! $a ++ $b) => `($a ++ $b)

/- Before this commit, the following command worked because
   it contained a "choice" node similar to the one at macro definition
   time. -/
check FOO! [1, 2] ++ [2, 3]

-- Now, we have 3 overloads for "++".
syntax [myAppend] term "++":65 term:65 : term

-- The `macro_rules` fails here.
```

This commit fixes this weird behavior by disallowing "choice" nodes in
patterns.
---
 src/Init/Lean/Elab/Quotation.lean | 7 +++++--
 src/Init/LeanInit.lean            | 7 +++++++
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
index 7e259170d2..e3d72608e0 100644
--- a/src/Init/Lean/Elab/Quotation.lean
+++ b/src/Init/Lean/Elab/Quotation.lean
@@ -330,8 +330,11 @@ alts ← alts.getArgs.getSepElems.mapM $ fun alt => do {
   pat ← if pats.getArgs.size == 1 then pure $ pats.getArg 0
     else throwError stx "match_syntax: expected exactly one pattern per alternative";
   let pat := if pat.isOfKind `Lean.Parser.Term.stxQuot then pat.setArg 1 $ elimAntiquotChoices $ pat.getArg 1 else pat;
-  let rhs := alt.getArg 2;
-  pure ([pat], rhs)
+  match pat.find? $ fun stx => stx.getKind == choiceKind with
+  | some choiceStx => throwError choiceStx "invalid pattern, nested syntax has multiple interpretations"
+  | none           =>
+    let rhs := alt.getArg 2;
+    pure ([pat], rhs)
 };
 -- letBindRhss (compileStxMatch stx [discr]) alts.toList []
 compileStxMatch stx [discr] alts.toList
diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index 5820bac15e..2e477a29b6 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -750,6 +750,13 @@ match stx.isTermId? relaxed with
 | some (id, opt) => if opt.isNone then some id else none
 | none           => none
 
+partial def findAux (p : Syntax → Bool) : Syntax → Option Syntax
+| stx@(Syntax.node _ args) => if p stx then some stx else args.findSome? findAux
+| stx                      => if p stx then some stx else none
+
+def find? (stx : Syntax) (p : Syntax → Bool) : Option Syntax :=
+findAux p stx
+
 end Syntax
 end Lean