chore: remove workaround for bug at new { ... : <expected-type> } syntax

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
 

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)

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;

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;

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

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⟩
 
 /--

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
    }

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 }, {})