feat: remove emptyc elaboration hack

@Kha I removed the hack. We know get a nice error message.

src/Lean/Elab/BuiltinNotation.lean

@@ -287,6 +287,11 @@ fun stx =>
 @[builtinMacro Lean.Parser.Term.«sorry»]  def expandSorry : Macro :=
 fun _ => `(sorryAx _ false)
 
+@[builtinTermElab emptyC] def expandEmptyC : TermElab :=
+fun stx expectedType? => do
+  stxNew ← `(HasEmptyc.emptyc);
+  withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+
 /-
 TODO
 @[builtinTermElab] def elabsubst : TermElab := expandInfixOp infixR " ▸ " 75

src/Lean/Elab/StructInst.lean

@@ -773,17 +773,6 @@ else
   let stxNew   := stx.setArg 4 mkNullNode;
   `(($stxNew : $expected))
 
-private def isEmptyStructInst (stx : Syntax) : Bool :=
-(stx.getArg 1).isNone &&
-(stx.getArg 2).isNone &&
-(stx.getArg 3).isNone &&
-(stx.getArg 4).isNone
-
-@[builtinTermElab emptyC] def expandEmptyC : TermElab :=
-fun stx expectedType? => do
-  stxNew ← `(HasEmptyc.emptyc);
-  withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
-
 @[builtinTermElab structInst] def elabStructInst : TermElab :=
 fun stx expectedType? => do
   stxNew? ← liftMacroM $ expandStructInstExpectedType stx;
@@ -795,22 +784,11 @@ fun stx expectedType? => do
     | some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
     | none => do
       sourceView ← getStructSource stx;
-      if isEmptyStructInst stx then do
-        /- Recall that we also want to use `{}` as notation for `HasEmptyc.emptyc` -/
-        tryPostponeIfNoneOrMVar expectedType?;
-        match expectedType? with
-        | none => expandEmptyC stx expectedType?
-        | some expectedType =>
-          /- We first try to create `@HasEmptyc.emptyc expectedType _`, if it fails, we elaborate as the empty structure. -/
-          catch
-            (mkAppOptM `HasEmptyc.emptyc #[expectedType, none])
-            (fun _ => elabStructInstAux stx expectedType? sourceView)
-      else do
-        modifyOp?  ← isModifyOp? stx;
-        match modifyOp?, sourceView with
-        | some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
-        | some _,        _                        => throwError ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
-        | _,             _                        => elabStructInstAux stx expectedType? sourceView
+      modifyOp?  ← isModifyOp? stx;
+      match modifyOp?, sourceView with
+      | some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
+      | some _,        _                        => throwError ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
+      | _,             _                        => elabStructInstAux stx expectedType? sourceView
 
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `Elab.struct;

src/Lean/Parser/Term.lean

@@ -56,7 +56,7 @@ def leadPrec := maxPrec - 1
 @[builtinTermParser] def syntheticHole := parser! "?" >> (ident <|> hole)
 @[builtinTermParser] def «sorry» := parser! "sorry"
 @[builtinTermParser] def cdot   := parser! "·"
-@[builtinTermParser] def emptyC := parser! "∅"
+@[builtinTermParser] def emptyC := parser! "∅" <|> ("{" >> "}")
 def typeAscription := parser! " : " >> termParser
 def tupleTail      := parser! ", " >> sepBy1 termParser ", "
 def parenSpecial : Parser := optional (tupleTail <|> typeAscription)

tests/lean/emptyc.lean

@@ -16,7 +16,4 @@ instance : HasEmptyc A :=
 ⟨{ x := 10 }⟩
 
 def boo : A :=
-{} -- this HasEmptyc.emptyc
-
-theorem ex3 : boo.x = 10 :=
-rfl
+{}  -- this is ambiguous

tests/lean/emptyc.lean.expected.out

@@ -0,0 +1 @@
+emptyc.lean:19:0: error: ambiguous, possible interpretations [{x := 0}, ∅]

tests/lean/run/choiceExpectedTypeBug.lean

@@ -5,8 +5,6 @@ new_frontend
 structure A :=
 (x : Nat := 10)
 
-syntax "{" "}"  : term -- overload `{ }` notation
-
 def f : A :=
 { }
 

tests/lean/run/expr_maps.lean

@@ -1,4 +1,5 @@
 import Lean.Expr
+new_frontend
 open Lean
 
 def exprType : Expr := mkSort levelOne