From bef1cd487284ba80136940e69055265874ea7e82 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 May 2022 19:14:22 -0700
Subject: [PATCH] fix: make structure instance notation (e.g., `{ a, b }`)
 works in patterns after we define the Set notation in Mathlib

---
 src/Lean/Elab/PatternVar.lean             | 11 +++-
 tests/lean/run/setStructInstNotation.lean | 71 +++++++++++++++++++++++
 2 files changed, 81 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/setStructInstNotation.lean

diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean
index bb30c64617..1f7b025264 100644
--- a/src/Lean/Elab/PatternVar.lean
+++ b/src/Lean/Elab/PatternVar.lean
@@ -221,7 +221,16 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     /- Similar to previous case -/
     doubleQuotedNameToPattern stx
   else if k == choiceKind then
-    let args := stx.getArgs
+    /- Remark: If there are `Term.structInst` alternatives, we keep only them. This is a hack to get rid of
+       Set-like notation in patterns. Recall that in Mathlib `{a, b}` can be a set with two elements or the
+       structure instance `{ a := a, b := b }`. Possible alternative solution: add a `pattern` category, or at least register
+       the `Syntax` node kinds that are allowed in patterns. -/
+    let args :=
+      let args := stx.getArgs
+      if args.any (·.isOfKind ``Parser.Term.structInst) then
+        args.filter (·.isOfKind ``Parser.Term.structInst)
+      else
+        args
     let stateSaved ← get
     let arg0 ← collect args[0]
     let stateNew ← get
diff --git a/tests/lean/run/setStructInstNotation.lean b/tests/lean/run/setStructInstNotation.lean
new file mode 100644
index 0000000000..70cb188fb7
--- /dev/null
+++ b/tests/lean/run/setStructInstNotation.lean
@@ -0,0 +1,71 @@
+structure Foo where
+  a : Nat
+  b : Nat
+
+def bla (x : Foo) : IO Unit := do
+  let { a, b } := x
+
+def Set (α : Type u) := α → Prop
+
+def setOf {α : Type u} (p : α → Prop) : Set α :=
+  p
+
+namespace Set
+
+protected def mem (a : α) (s : Set α) :=
+  s a
+
+instance : Membership α (Set α) :=
+  ⟨Set.mem⟩
+
+protected def subset (s₁ s₂ : Set α) :=
+  ∀ {a}, a ∈ s₁ → a ∈ s₂
+
+instance : EmptyCollection (Set α) :=
+  ⟨λ a => false⟩
+
+protected def insert (a : α) (s : Set α) : Set α :=
+  fun b => b = a ∨ b ∈ s
+
+protected def singleton (a : α) : Set α :=
+  fun b => b = a
+
+syntax "{" term,+ "}" : term
+
+macro_rules
+  | `({$x:term}) => `(Set.singleton $x)
+  | `({$x:term, $xs:term,*}) => `(Set.insert $x {$xs:term,*})
+
+#check { 1, 2 } -- Set Nat
+
+end Set
+def f1 (a b : Nat) : Set Nat :=
+  { a, b }
+
+def f2 (a b : Nat) : Foo :=
+  { a, b }
+
+def f3 (a b : Nat) :=
+  { a, b }
+
+#check f3 -- Nat → Nat → Set Nat
+
+def f4 (a b : α) :=
+  { a, b }
+
+#check @f4 -- {α : Type u_1} → α → α → Set α
+
+def f5 (a b : Nat) :=
+  { a, b : Foo }
+
+def boo1 (x : Foo) : IO Unit :=
+  let { a, b } := x
+  pure ()
+
+def boo2 (x : Foo) : IO Unit := do
+  let { a, b } := x
+  pure ()
+
+def boo3 (x : Nat → IO Foo) : IO Nat := do
+  let { a, b } ← x 0
+  return a + b