chore: set literal notation (#3348)

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

src/Init/NotationExtra.lean

@@ -460,3 +460,9 @@ macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
   `(((match $e:term with | $[$p:term]|* => true | _ => false) : Bool))
 
 end Lean
+
+syntax "{" term,+ "}" : term
+
+macro_rules
+  | `({$x:term}) => `(singleton $x)
+  | `({$x:term, $xs:term,*}) => `(insert $x {$xs:term,*})

src/Lean/Elab/MutualDef.lean

@@ -214,7 +214,7 @@ private def expandWhereStructInst : Macro
         `(structInstField|$id:ident := $val)
       | stx@`(letIdDecl|_ $_* $[: $_]? := $_) => Macro.throwErrorAt stx "'_' is not allowed here"
       | _ => Macro.throwUnsupported
-    let body ← `({ $structInstFields,* })
+    let body ← `(structInst| { $structInstFields,* })
     match whereDecls? with
     | some whereDecls => expandWhereDecls whereDecls body
     | none => return body

src/Lean/Server/Rpc/Deriving.lean

@@ -41,7 +41,6 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
       decInits := decInits.push (← `(structInstField| $fid:ident := ← rpcDecode a.$fid))
 
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
-
   let indName := mkIdent indVal.name
   `(-- Workaround for https://github.com/leanprover/lean4/issues/2044
     namespace $indName
@@ -57,7 +56,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
       enc a := return toJson { $[$encInits],* : RpcEncodablePacket }
       dec j := do
         let a : RpcEncodablePacket ← fromJson? j
-        return { $[$decInits],* }
+        return { $decInits:structInstField,* }
     end $indName
   )
 

tests/lean/interactive/fieldCompletion.lean.expected.out

@@ -1,4 +1,3 @@
 {"textDocument": {"uri": "file:///fieldCompletion.lean"},
  "position": {"line": 5, "character": 3}}
-{"items": [{"label": "modifiers", "kind": 5, "detail": "field"}],
- "isIncomplete": true}
+{"items": [], "isIncomplete": true}

tests/lean/run/setStructInstNotation.lean

@@ -30,11 +30,8 @@ protected def insert (a : α) (s : Set α) : Set α :=
 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,*})
+instance : Insert α (Set α) := ⟨Set.insert⟩
+instance : Singleton α (Set α) := ⟨Set.singleton⟩
 
 #check { 1, 2 } -- Set Nat
 
@@ -45,12 +42,12 @@ def f1 (a b : Nat) : Set Nat :=
 def f2 (a b : Nat) : Foo :=
   { a, b }
 
-def f3 (a b : Nat) :=
+def f3 (a b : Nat) : Set Nat :=
   { a, b }
 
 #check f3 -- Nat → Nat → Set Nat
 
-def f4 (a b : α) :=
+def f4 (a b : α) : Set α :=
   { a, b }
 
 #check @f4 -- {α : Type u_1} → α → α → Set α

tests/lean/semicolonOrLinebreak.lean.expected.out

@@ -1,4 +1,9 @@
 semicolonOrLinebreak.lean:2:12: error: expected ';' or line break
 semicolonOrLinebreak.lean:9:31-10:8: error: fields missing: 'y'
 semicolonOrLinebreak.lean:10:8-10:9: error: unexpected identifier; expected command
-semicolonOrLinebreak.lean:20:7-20:9: error: unexpected token '}'; expected ':'
+semicolonOrLinebreak.lean:20:4-20:7: error: function expected at
+  x
+term has type
+  Nat
+semicolonOrLinebreak.lean:20:2-20:9: error: failed to synthesize instance
+  Singleton ?m Point

tests/lean/setLit.lean

@@ -0,0 +1,24 @@
+structure Foo where
+  val := 10
+
+instance : Singleton α (List α) where
+  singleton a := [a]
+
+instance : Insert α (List α) where
+  insert a as := a :: as
+
+def f1 : Foo := {}
+
+def f2 : List Nat := {}
+
+def f3 : List Nat := {1, 2}
+
+def f4 (a : Nat) : List Nat := {a}
+
+def f5 (val : Nat) : Foo := {val}
+
+def f6 (val : Nat) : List Nat := {val}
+
+def f7 : String := {}
+
+def f8 (val : Nat) : String := { val }

tests/lean/setLit.lean.expected.out

@@ -0,0 +1,10 @@
+setLit.lean:22:19-22:21: error: overloaded, errors 
+  failed to synthesize instance
+    EmptyCollection String
+  
+  fields missing: 'data'
+setLit.lean:24:31-24:38: error: overloaded, errors 
+  failed to synthesize instance
+    Singleton Nat String
+  
+  24:33 'val' is not a field of structure 'String'