diff --git a/stage0/src/Init/Lean/Attributes.lean b/stage0/src/Init/Lean/Attributes.lean
index 06b99ea8e3..1716651dc6 100644
--- a/stage0/src/Init/Lean/Attributes.lean
+++ b/stage0/src/Init/Lean/Attributes.lean
@@ -383,17 +383,18 @@ ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← register
     r.qsort (fun a b => Name.quickLt a.1 b.1),
   statsFn         := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
 };
-let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => { AttributeImpl .
+let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => {
   name            := name,
   descr           := descr,
   applicationTime := applicationTime,
-  add             := fun env decl args persistent => do
+  add             := (fun env decl args persistent => do
     unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
     unless (env.getModuleIdxFor? decl).isNone $
       throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
     match validate env decl val with
     | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
-    | _                => pure $ ext.addEntry env (decl, val)
+    | _                => pure $ ext.addEntry env (decl, val))
+  : AttributeImpl
 };
 attrs.forM registerBuiltinAttribute;
 pure { ext := ext, attrs := attrs }
diff --git a/stage0/src/Init/Lean/Compiler/IR/Basic.lean b/stage0/src/Init/Lean/Compiler/IR/Basic.lean
index df47ec6e9b..a6d7a9e468 100644
--- a/stage0/src/Init/Lean/Compiler/IR/Basic.lean
+++ b/stage0/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/stage0/src/Init/Lean/Compiler/IR/Boxing.lean b/stage0/src/Init/Lean/Compiler/IR/Boxing.lean
index 6365424f76..87b1bb0cf5 100644
--- a/stage0/src/Init/Lean/Compiler/IR/Boxing.lean
+++ b/stage0/src/Init/Lean/Compiler/IR/Boxing.lean
@@ -53,7 +53,7 @@ let ps := decl.params;
 
 def mkBoxedVersionAux (decl : Decl) : N Decl := do
 let ps := decl.params;
-qs ← ps.mapM (fun _ => do x ← mkFresh; pure { Param . x := x, ty := IRType.object, borrow := false });
+qs ← ps.mapM (fun _ => do x ← mkFresh; pure { x := x, ty := IRType.object, borrow := false : Param });
 (newVDecls, xs) ← qs.size.foldM
   (fun i (r : Array FnBody × Array Arg) =>
      let (newVDecls, xs) := r;
diff --git a/stage0/src/Init/Lean/Data/Options.lean b/stage0/src/Init/Lean/Data/Options.lean
index 8667c02222..145bbae172 100644
--- a/stage0/src/Init/Lean/Data/Options.lean
+++ b/stage0/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/stage0/src/Init/Lean/Elab/Frontend.lean b/stage0/src/Init/Lean/Elab/Frontend.lean
index 52f54ea512..bdd60cdf88 100644
--- a/stage0/src/Init/Lean/Elab/Frontend.lean
+++ b/stage0/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/stage0/src/Init/Lean/Elab/Import.lean b/stage0/src/Init/Lean/Elab/Import.lean
index 6c43d75af6..f862e50dd6 100644
--- a/stage0/src/Init/Lean/Elab/Import.lean
+++ b/stage0/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 [{Import . module := `Init}] 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/stage0/src/Init/Lean/Elab/Quotation.lean b/stage0/src/Init/Lean/Elab/Quotation.lean
index 9116ff1583..37ccec4585 100644
--- a/stage0/src/Init/Lean/Elab/Quotation.lean
+++ b/stage0/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) := { HeadInfo . rhsFn := rhsFn };
+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/stage0/src/Init/Lean/Expr.lean b/stage0/src/Init/Lean/Expr.lean
index e04f2500e5..05147d0ac7 100644
--- a/stage0/src/Init/Lean/Expr.lean
+++ b/stage0/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/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean b/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean
index 86fbfcf7f8..43e64107fc 100644
--- a/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean
+++ b/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean
@@ -92,7 +92,7 @@ def generalizeTelescope {α} (es : Array Expr) (prefixForNewVars : Name) (k : Ar
 es ← es.mapM $ fun e => do {
   type ← inferType e;
   type ← instantiateMVars type;
-  pure { Entry . expr := e, type := type, modified := false }
+  pure { expr := e, type := type, modified := false : Entry }
 };
 generalizeTelescopeAux prefixForNewVars k es 0 1 #[]
 
diff --git a/stage0/src/Init/Lean/Meta/SynthInstance.lean b/stage0/src/Init/Lean/Meta/SynthInstance.lean
index 7d965394cb..0bf6c7e099 100644
--- a/stage0/src/Init/Lean/Meta/SynthInstance.lean
+++ b/stage0/src/Init/Lean/Meta/SynthInstance.lean
@@ -362,7 +362,7 @@ answer ← withMCtx cNode.mctx $ do {
   val ← instantiateMVars cNode.mvar;
   result ← abstractMVars val; -- assignable metavariables become parameters
   resultType ← inferType result.expr;
-  pure { Answer . result := result, resultType := resultType }
+  pure { result := result, resultType := resultType : Answer }
 };
 -- Remark: `answer` does not contain assignable or assigned metavariables.
 let key := cNode.key;
@@ -465,7 +465,7 @@ traceCtx `Meta.synthInstance $ do
    mvar ← mkFreshExprMVar type;
    mctx ← getMCtx;
    let key := mkTableKey mctx type;
-   adaptState' (fun (s : Meta.State) => { State . toState := s }) (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/stage0/src/Init/Lean/Parser/Module.lean b/stage0/src/Init/Lean/Parser/Module.lean
index 9fd0b1ac9f..7a679aafe2 100644
--- a/stage0/src/Init/Lean/Parser/Module.lean
+++ b/stage0/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 }, {})
 
@@ -71,7 +71,7 @@ partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleP
     (mkEOI pos, s, messages)
   else
     let c  := mkParserContext env inputCtx;
-    let s  := { ParserState . cache := initCacheForInput c.input, pos := pos };
+    let s  := { cache := initCacheForInput c.input, pos := pos : ParserState };
     let s  := whitespace c s;
     let s  := (commandParser : Parser).fn c s;
     match s.errorMsg with
diff --git a/stage0/src/Init/Lean/Parser/Parser.lean b/stage0/src/Init/Lean/Parser/Parser.lean
index fd9d2252e7..81099d3c1d 100644
--- a/stage0/src/Init/Lean/Parser/Parser.lean
+++ b/stage0/src/Init/Lean/Parser/Parser.lean
@@ -580,7 +580,7 @@ private def rawAux (startPos : Nat) (trailingWs : Bool) : ParserFn
   if trailingWs then
     let s        := whitespace c s;
     let stopPos' := s.pos;
-    let trailing := { Substring . str := input, startPos := stopPos, stopPos := stopPos' };
+    let trailing := { str := input, startPos := stopPos, stopPos := stopPos' : Substring };
     let atom     := mkAtom { leading := leading, pos := startPos, trailing := trailing } val;
     s.pushSyntax atom
   else
@@ -637,8 +637,8 @@ let leading   := mkEmptySubstringAt input startPos;
 let val       := input.extract startPos stopPos;
 let s         := whitespace c s;
 let wsStopPos := s.pos;
-let trailing  := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos };
-let info      := { SourceInfo . leading := leading, pos := startPos, trailing := trailing };
+let trailing  := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring };
+let info      := { leading := leading, pos := startPos, trailing := trailing : SourceInfo };
 s.pushSyntax (mkStxLit n val info)
 
 def charLitFnAux (startPos : Nat) : ParserFn
@@ -760,7 +760,7 @@ match tk with
   let s         := s.setPos stopPos;
   let s         := whitespace c s;
   let wsStopPos := s.pos;
-  let trailing  := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos };
+  let trailing  := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring };
   let atom      := mkAtom { leading := leading, pos := startPos, trailing := trailing } val;
   s.pushSyntax atom
 
@@ -771,12 +771,12 @@ if isToken startPos stopPos tk then
   mkTokenAndFixPos startPos tk c s
 else
   let input           := c.input;
-  let rawVal          := { Substring . str := input, startPos := startPos, stopPos := stopPos };
+  let rawVal          := { str := input, startPos := startPos, stopPos := stopPos  : Substring };
   let s               := whitespace c s;
   let trailingStopPos := s.pos;
   let leading         := mkEmptySubstringAt input startPos;
-  let trailing        := { Substring . str := input, startPos := stopPos, stopPos := trailingStopPos };
-  let info            := { SourceInfo . leading := leading, trailing := trailing, pos := startPos };
+  let trailing        := { str := input, startPos := stopPos, stopPos := trailingStopPos : Substring };
+  let info            := { leading := leading, trailing := trailing, pos := startPos : SourceInfo };
   let atom            := mkIdent info rawVal val;
   s.pushSyntax atom
 
diff --git a/stage0/src/Init/System/FilePath.lean b/stage0/src/Init/System/FilePath.lean
index 3e8fba0ed9..946cd0e4e1 100644
--- a/stage0/src/Init/System/FilePath.lean
+++ b/stage0/src/Init/System/FilePath.lean
@@ -49,7 +49,7 @@ def dirName (fname : String) : String :=
 let fname := normalizePath fname;
 match fname.revPosOf pathSeparator with
 | none => "."
-| some pos => { Substring . str := fname, startPos := 0, stopPos := pos }.toString
+| some pos => { str := fname, startPos := 0, stopPos := pos : Substring }.toString
 
 end FilePath
 
diff --git a/stage0/src/frontends/lean/brackets.cpp b/stage0/src/frontends/lean/brackets.cpp
index b2cf3001e7..7dee425acb 100644
--- a/stage0/src/frontends/lean/brackets.cpp
+++ b/stage0/src/frontends/lean/brackets.cpp
@@ -82,6 +82,8 @@ static expr parse_structure_instance_core(parser & p, optional<expr> const & src
             p.next();
             catchall = true;
             break;
+        } else if (p.curr_is_token(get_colon_tk())) {
+            break;
         } else if (!read_source) {
             fns.push_back(p.check_id_next("invalid structure instance, identifier expected"));
             p.check_token_next(get_assign_tk(), "invalid structure instance, ':=' expected");
@@ -176,6 +178,8 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
         return p.save_pos(mk_structure_instance(), pos);
     } else if (p.curr_is_token(get_dotdot_tk())) {
         return parse_structure_instance_core(p);
+    } else if (p.curr_is_token(get_colon_tk())) {
+        return parse_structure_instance_core(p);
     } else {
         e = p.parse_expr();
     }