From 151012cb39b4cfd28fcab6f2536f627fcc0ccb4a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 11 Sep 2020 14:41:44 -0700
Subject: [PATCH] feat: remove `emptyc` elaboration hack

@Kha I removed the hack. We know get a nice error message.
---
 src/Lean/Elab/BuiltinNotation.lean        |  5 ++++
 src/Lean/Elab/StructInst.lean             | 32 ++++-------------------
 src/Lean/Parser/Term.lean                 |  2 +-
 tests/lean/emptyc.lean                    |  5 +---
 tests/lean/emptyc.lean.expected.out       |  1 +
 tests/lean/run/choiceExpectedTypeBug.lean |  2 --
 tests/lean/run/expr_maps.lean             |  1 +
 7 files changed, 14 insertions(+), 34 deletions(-)
 create mode 100644 tests/lean/emptyc.lean.expected.out

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 4918004c6d..89c64c88ef 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/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
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index d6fef9d23a..bfa99d8ef1 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/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;
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index fdec928ee3..eb62510b16 100644
--- a/src/Lean/Parser/Term.lean
+++ b/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)
diff --git a/tests/lean/emptyc.lean b/tests/lean/emptyc.lean
index 1e477ac9c2..5ad95b8468 100644
--- a/tests/lean/emptyc.lean
+++ b/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
diff --git a/tests/lean/emptyc.lean.expected.out b/tests/lean/emptyc.lean.expected.out
new file mode 100644
index 0000000000..c4bbb21125
--- /dev/null
+++ b/tests/lean/emptyc.lean.expected.out
@@ -0,0 +1 @@
+emptyc.lean:19:0: error: ambiguous, possible interpretations [{x := 0}, ∅]
diff --git a/tests/lean/run/choiceExpectedTypeBug.lean b/tests/lean/run/choiceExpectedTypeBug.lean
index 53a48be5d7..decf89fadb 100644
--- a/tests/lean/run/choiceExpectedTypeBug.lean
+++ b/tests/lean/run/choiceExpectedTypeBug.lean
@@ -5,8 +5,6 @@ new_frontend
 structure A :=
 (x : Nat := 10)
 
-syntax "{" "}"  : term -- overload `{ }` notation
-
 def f : A :=
 { }
 
diff --git a/tests/lean/run/expr_maps.lean b/tests/lean/run/expr_maps.lean
index e8b78370f3..bf862b271c 100644
--- a/tests/lean/run/expr_maps.lean
+++ b/tests/lean/run/expr_maps.lean
@@ -1,4 +1,5 @@
 import Lean.Expr
+new_frontend
 open Lean
 
 def exprType : Expr := mkSort levelOne