From 618d11307568286dccbbf562afe3d6ed987cd7ea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 20 May 2020 15:56:28 -0700
Subject: [PATCH] chore: remove workaround for bug at new  `{ ... :
 <expected-type> }` syntax

---
 src/Init/Lean/Compiler/IR/Basic.lean  | 2 +-
 src/Init/Lean/Data/Options.lean       | 2 +-
 src/Init/Lean/Elab/Frontend.lean      | 2 +-
 src/Init/Lean/Elab/Import.lean        | 2 +-
 src/Init/Lean/Elab/Quotation.lean     | 2 +-
 src/Init/Lean/Expr.lean               | 2 +-
 src/Init/Lean/Meta/SynthInstance.lean | 2 +-
 src/Init/Lean/Parser/Module.lean      | 2 +-
 8 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Init/Lean/Compiler/IR/Basic.lean b/src/Init/Lean/Compiler/IR/Basic.lean
index a6d7a9e468..cb280fb6a6 100644
--- a/src/Init/Lean/Compiler/IR/Basic.lean
+++ b/src/Init/Lean/Compiler/IR/Basic.lean
@@ -48,7 +48,7 @@ end JoinPointId
 
 abbrev MData := KVMap
 namespace MData
-abbrev empty : MData := ({} : KVMap)
+abbrev empty : MData := { : KVMap }
 instance : HasEmptyc MData := ⟨empty⟩
 end MData
 
diff --git a/src/Init/Lean/Data/Options.lean b/src/Init/Lean/Data/Options.lean
index 145bbae172..f0538671eb 100644
--- a/src/Init/Lean/Data/Options.lean
+++ b/src/Init/Lean/Data/Options.lean
@@ -14,7 +14,7 @@ namespace Lean
 def Options := KVMap
 
 namespace Options
-def empty : Options  := ({} : KVMap)
+def empty : Options  := { : KVMap }
 instance : HasEmptyc Options := ⟨empty⟩
 instance : Inhabited Options := ⟨empty⟩
 instance : HasToString Options := inferInstanceAs (HasToString KVMap)
diff --git a/src/Init/Lean/Elab/Frontend.lean b/src/Init/Lean/Elab/Frontend.lean
index bdd60cdf88..d146019cc8 100644
--- a/src/Init/Lean/Elab/Frontend.lean
+++ b/src/Init/Lean/Elab/Frontend.lean
@@ -88,7 +88,7 @@ EIO.adaptExcept (fun (ex : Empty) => Empty.rec _ ex) $
 def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
 let fileName   := fileName.getD "<input>";
 let inputCtx   := Parser.mkInputContext input fileName;
-parserStateRef ← IO.mkRef ({} : Parser.ModuleParserState);
+parserStateRef ← IO.mkRef { : Parser.ModuleParserState };
 cmdStateRef    ← IO.mkRef $ Command.mkState env {} opts;
 IO.processCommands inputCtx parserStateRef cmdStateRef;
 cmdState ← cmdStateRef.get;
diff --git a/src/Init/Lean/Elab/Import.lean b/src/Init/Lean/Elab/Import.lean
index f862e50dd6..0fddaade24 100644
--- a/src/Init/Lean/Elab/Import.lean
+++ b/src/Init/Lean/Elab/Import.lean
@@ -11,7 +11,7 @@ namespace Elab
 
 def headerToImports (header : Syntax) : List Import :=
 let header  := header.asNode;
-let imports := if (header.getArg 0).isNone then [({ module := `Init } : Import)] else [];
+let imports := if (header.getArg 0).isNone then [{ module := `Init : Import }] else [];
 imports ++ (header.getArg 1).getArgs.toList.map (fun stx =>
   -- `stx` is of the form `(Module.import "import" "runtime"? id)
   let runtime := !(stx.getArg 1).isNone;
diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
index 37ccec4585..6ab00149cd 100644
--- a/src/Init/Lean/Elab/Quotation.lean
+++ b/src/Init/Lean/Elab/Quotation.lean
@@ -168,7 +168,7 @@ def HeadInfo.generalizes : HeadInfo → HeadInfo → Bool
 
 private def getHeadInfo (alt : Alt) : HeadInfo :=
 let pat := alt.fst.head!;
-let unconditional (rhsFn) := ({ rhsFn := rhsFn } : HeadInfo );
+let unconditional (rhsFn) := { rhsFn := rhsFn : HeadInfo };
 -- variable pattern
 if pat.isOfKind `Lean.Parser.Term.id then unconditional $ fun rhs => `(let $pat := discr; $rhs)
 -- wildcard pattern
diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean
index 05147d0ac7..6e075dee2c 100644
--- a/src/Init/Lean/Expr.lean
+++ b/src/Init/Lean/Expr.lean
@@ -79,7 +79,7 @@ protected def BinderInfo.beq : BinderInfo → BinderInfo → Bool
 instance BinderInfo.hasBeq : HasBeq BinderInfo := ⟨BinderInfo.beq⟩
 
 abbrev MData := KVMap
-abbrev MData.empty : MData := ({} : KVMap)
+abbrev MData.empty : MData := { : KVMap }
 instance MVData.hasEmptc : HasEmptyc MData := ⟨MData.empty⟩
 
 /--
diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean
index 0bf6c7e099..80d0262fdc 100644
--- a/src/Init/Lean/Meta/SynthInstance.lean
+++ b/src/Init/Lean/Meta/SynthInstance.lean
@@ -465,7 +465,7 @@ traceCtx `Meta.synthInstance $ do
    mvar ← mkFreshExprMVar type;
    mctx ← getMCtx;
    let key := mkTableKey mctx type;
-   adaptState' (fun (s : Meta.State) => ( { toState := s } : State )) (fun (s : State) => s.toState) $ do {
+   adaptState' (fun (s : Meta.State) => { toState := s : State }) (fun (s : State) => s.toState) $ do {
      newSubgoal mctx key mvar Waiter.root;
      synth fuel
    }
diff --git a/src/Init/Lean/Parser/Module.lean b/src/Init/Lean/Parser/Module.lean
index 7a679aafe2..653301a6be 100644
--- a/src/Init/Lean/Parser/Module.lean
+++ b/src/Init/Lean/Parser/Module.lean
@@ -44,7 +44,7 @@ let stx := s.stxStack.back;
 match s.errorMsg with
 | some errorMsg =>
   let msg := mkErrorMessage ctx s.pos (toString errorMsg);
-  (stx, { pos := s.pos, recovering := true }, ({} : MessageLog).add msg)
+  (stx, { pos := s.pos, recovering := true }, { : MessageLog }.add msg)
 | none =>
   (stx, { pos := s.pos }, {})