feat: adjust deriving Inhabited to use structure field defaults (#9815)

This PR changes the `Inhabited` deriving handler for `structure` types
to use default field values when present; this ensures that `{}` and
`default` are interchangeable when all fields have default values. The
handler effectively uses `by refine' {..} <;> exact default` to
construct the inhabitant. (Note: when default field values cannot be
resolved, they are ignored, as usual for ellipsis mode.)

Implementation note: the handler now constructs the `Expr` directly and
adds it to the environment, though the `instance` is still added using
`elabCommand`.

Closes #9463

src/Lean/Elab/App.lean

@@ -13,6 +13,7 @@ public import Lean.IdentifierSuggestion
 import all Lean.Elab.ErrorUtils
 import Lean.Elab.DeprecatedArg
 import Init.Omega
+import Init.Data.List.MapIdx
 
 public section
 
@@ -1299,13 +1300,13 @@ where
 inductive LValResolution where
   /-- When applied to `f`, effectively expands to `BaseStruct.fieldName (self := Struct.toBase f)`.
   This is a special named argument where it suppresses any explicit arguments depending on it so that type parameters don't need to be supplied. -/
-  | projFn   (baseStructName : Name) (structName : Name) (fieldName : Name)
+  | projFn   (baseStructName : Name) (structName : Name) (fieldName : Name) (levels : List Level)
   /-- Similar to `projFn`, but for extracting field indexed by `idx`. Works for one-constructor inductive types in general. -/
   | projIdx  (structName : Name) (idx : Nat)
   /-- When applied to `f`, effectively expands to `constName ... (Struct.toBase f)`, with the argument placed in the correct
   positional argument if possible, or otherwise as a named argument. The `Struct.toBase` is not present if `baseStructName == structName`,
   in which case these do not need to be structures. Supports generalized field notation. -/
-  | const    (baseStructName : Name) (structName : Name) (constName : Name)
+  | const    (baseStructName : Name) (structName : Name) (constName : Name) (levels : List Level)
   /-- Like `const`, but with `fvar` instead of `constName`.
   The `baseName` is the base name of the type to search for in the parameter list. -/
   | localRec (baseName : Name) (fvar : Expr)
@@ -1380,7 +1381,7 @@ private def reverseFieldLookup (env : Environment) (fieldName : String) :=
 
 private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
   match eType.getAppFn, lval with
-  | .const structName _, LVal.fieldIdx ref idx =>
+  | .const structName _, LVal.fieldIdx ref idx levels =>
     if idx == 0 then
       throwError "Invalid projection: Index must be greater than 0"
     let env ← getEnv
@@ -1393,10 +1394,14 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       if idx - 1 < numFields then
         if isStructure env structName then
           let fieldNames := getStructureFields env structName
-          return LValResolution.projFn structName structName fieldNames[idx - 1]!
+          return LValResolution.projFn structName structName fieldNames[idx - 1]! levels
         else
           /- `structName` was declared using `inductive` command.
             So, we don't projection functions for it. Thus, we use `Expr.proj` -/
+          unless levels.isEmpty do
+            throwError "Invalid projection: Explicit universe levels are only supported for inductive types \
+              defined using the `structure` command. \
+              The expression{indentExpr e}\nhas type{inlineExpr eType}which is not a `structure`."
           return LValResolution.projIdx structName (idx - 1)
       else
         if numFields == 0 then
@@ -1409,31 +1414,33 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           ++ MessageData.note m!"The expression{indentExpr e}\nhas type{inlineExpr eType}which has only \
           {numFields} field{numFields.plural}"
           ++ tupleHint
-  | .const structName _, LVal.fieldName ref fieldName _ _ => withRef ref do
+  | .const structName _, LVal.fieldName ref fieldName levels _ _ => withRef ref do
     let env ← getEnv
     if isStructure env structName then
       if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then
-        return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName)
+        return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName) levels
     -- Search the local context first
     let fullName := Name.mkStr (privateToUserName structName) fieldName
     for localDecl in (← getLCtx) do
       if localDecl.isAuxDecl then
         if let some localDeclFullName := (← getLCtx).auxDeclToFullName.get? localDecl.fvarId then
           if fullName == privateToUserName localDeclFullName then
+            unless levels.isEmpty do
+              throwInvalidExplicitUniversesForLocal localDecl.toExpr
             /- LVal notation is being used to make a "local" recursive call. -/
             return LValResolution.localRec structName localDecl.toExpr
     -- Then search the environment
     if let some (baseStructName, fullName) ← findMethod? structName (.mkSimple fieldName) then
-      return LValResolution.const baseStructName structName fullName
+      return LValResolution.const baseStructName structName fullName levels
     throwInvalidFieldAt ref fieldName fullName
       -- Suggest a potential unreachable private name as hint. This does not cover structure
       -- inheritance, nor `import all`.
       (declHint := (mkPrivateName env structName).mkStr fieldName)
 
-  | .forallE .., LVal.fieldName ref fieldName suffix? fullRef =>
+  | .forallE .., LVal.fieldName ref fieldName levels suffix? fullRef =>
     let fullName := Name.str `Function fieldName
     if (← getEnv).contains fullName then
-      return LValResolution.const `Function `Function fullName
+      return LValResolution.const `Function `Function fullName levels
     match e.getAppFn, suffix? with
     | Expr.const c _, some suffix =>
       throwUnknownNameWithSuggestions (idOrConst := "constant")  (ref? := fullRef) (c ++ suffix)
@@ -1443,7 +1450,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     throwError "Invalid projection: Projections cannot be used on functions, and{indentExpr e}\n\
       has function type{inlineExprTrailing eType}"
 
-  | .mvar .., .fieldName _ fieldName _ _ =>
+  | .mvar .., .fieldName _ fieldName levels _ _ =>
     let hint := match reverseFieldLookup (← getEnv) fieldName with
       | #[] => MessageData.nil
       | #[opt] => .hint' m!"Consider replacing the field projection `.{fieldName}` with a call to the function `{.ofConstName opt}`."
@@ -1451,13 +1458,13 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           {MessageData.joinSep (opts.toList.map (indentD m!"• `{.ofConstName ·}`")) .nil}"
     throwNamedError lean.invalidField (m!"Invalid field notation: Type of{indentExpr e}\nis not \
       known; cannot resolve field `{fieldName}`" ++ hint)
-  | .mvar .., .fieldIdx _ i  =>
+  | .mvar .., .fieldIdx _ i _ =>
     throwError m!"Invalid projection: Type of{indentExpr e}\nis not known; cannot resolve \
       projection `{i}`"
 
   | _, _ =>
     match e.getAppFn, lval with
-    | Expr.const c _, .fieldName _ref _fieldName (some suffix) fullRef =>
+    | Expr.const c _, .fieldName _ref _fieldName _levels (some suffix) fullRef =>
       throwUnknownNameWithSuggestions (idOrConst := "constant") (ref? := fullRef) (c ++ suffix)
     | _, .fieldName .. =>
       throwNamedError lean.invalidField m!"Invalid field notation: Field projection operates on \
@@ -1706,12 +1713,12 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       let f ← mkProjAndCheck structName idx f
       let f ← addTermInfo lval.getRef f
       loop f lvals
-    | LValResolution.projFn baseStructName structName fieldName =>
+    | LValResolution.projFn baseStructName structName fieldName levels =>
       let f ← mkBaseProjections baseStructName structName f
       let some info := getFieldInfo? (← getEnv) baseStructName fieldName | unreachable!
       if (← isInaccessiblePrivateName info.projFn) then
         throwError "Field `{fieldName}` from structure `{structName}` is private"
-      let projFn ← withRef lval.getRef <| mkConst info.projFn
+      let projFn ← withRef lval.getRef <| mkConst info.projFn levels
       let projFn ← addProjTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
@@ -1719,9 +1726,9 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       else
         let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
         loop f lvals
-    | LValResolution.const baseStructName structName constName =>
+    | LValResolution.const baseStructName structName constName levels =>
       let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
-      let projFn ← withRef lval.getRef <| mkConst constName
+      let projFn ← withRef lval.getRef <| mkConst constName levels
       let projFn ← addProjTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let (args, namedArgs) ← addLValArg baseStructName f args namedArgs projFn explicit
@@ -1772,15 +1779,19 @@ false, no elaboration function executed by `x` will reset it to
 /--
 Elaborates the resolutions of a function. The `fns` array is the output of `resolveName'`.
 -/
-private def elabAppFnResolutions (fRef : Syntax) (fns : List (Expr × Syntax × List Syntax)) (lvals : List LVal)
+private def elabAppFnResolutions (fRef : Syntax) (fns : List (Expr × Syntax × List Syntax × List Level)) (lvals : List LVal)
     (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool)
     (acc : Array (TermElabResult Expr)) (forceTermInfo : Bool := false) :
     TermElabM (Array (TermElabResult Expr)) := do
   let overloaded := overloaded || fns.length > 1
   -- Set `errToSorry` to `false` if `fns` > 1. See comment above about the interaction between `errToSorry` and `observing`.
   withReader (fun ctx => { ctx with errToSorry := fns.length == 1 && ctx.errToSorry }) do
-    fns.foldlM (init := acc) fun acc (f, fIdent, fields) => do
-      let lvals' := toLVals fields (first := true)
+    fns.foldlM (init := acc) fun acc (f, fIdent, fields, projLevels) => do
+      let lastIdx := fields.length - 1
+      let lvals' := fields.mapIdx fun idx field =>
+        let suffix? := if idx == 0       then some <| toName fields else none
+        let levels  := if idx == lastIdx then projLevels            else []
+        LVal.fieldName field field.getId.getString! levels suffix? fRef
       let s ← observing do
         checkDeprecated fIdent f
         let f ← addTermInfo fIdent f expectedType? (force := forceTermInfo)
@@ -1794,11 +1805,6 @@ where
       | field :: fields => .mkStr (go fields) field.getId.toString
     go fields.reverse
 
-  toLVals : List Syntax → (first : Bool) → List LVal
-    | [],            _     => []
-    | field::fields, true  => .fieldName field field.getId.getString! (toName (field::fields)) fRef :: toLVals fields false
-    | field::fields, false => .fieldName field field.getId.getString! none fRef :: toLVals fields false
-
 private def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level) (lvals : List LVal)
     (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool)
     (acc : Array (TermElabResult Expr)) :
@@ -1832,7 +1838,7 @@ To infer a namespace from the expected type, we do the following operations:
 - if the type is of the form `c x₁ ... xₙ` with `c` a constant, then try using `c` as the namespace,
   and if that doesn't work, try unfolding the expression and continuing.
 -/
-private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
+private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax × List Level)) := do
   unless id.isAtomic do
     throwError "Invalid dotted identifier notation: The name `{id}` must be atomic"
   tryPostponeIfNoneOrMVar expectedType?
@@ -1844,7 +1850,7 @@ private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitU
   withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
-  throwNoExpectedType := do
+  throwNoExpectedType {α} : TermElabM α := do
     let hint ← match reverseFieldLookup (← getEnv) (id.getString!) with
       | #[] => pure MessageData.nil
       | suggestions =>
@@ -1863,7 +1869,7 @@ where
         withForallBody body k
     else
       k type
-  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM (List (Expr × Syntax × List Syntax)) := do
+  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM (List (Expr × Syntax × List Syntax × List Level)) := do
     let resultType ← instantiateMVars resultType
     let resultTypeFn := resultType.getAppFn
     try
@@ -1880,11 +1886,11 @@ where
           |>.filter (fun (_, fieldList) => fieldList.isEmpty)
           |>.map Prod.fst
         if !candidates.isEmpty then
-          candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← getRef, [])
+          candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← getRef, [], [])
         else if let some (fvar, []) ← resolveLocalName fullName then
           unless explicitUnivs.isEmpty do
             throwInvalidExplicitUniversesForLocal fvar
-          return [(fvar, ← getRef, [])]
+          return [(fvar, ← getRef, [], [])]
         else
           throwUnknownIdentifierAt (← getRef) (declHint := fullName) <| m!"Unknown constant `{.ofConstName fullName}`"
             ++ .note m!"Inferred this name from the expected resulting type of `.{id}`:{indentExpr expectedType}"
@@ -1914,26 +1920,37 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     withReader (fun ctx => { ctx with errToSorry := false }) do
       f.getArgs.foldlM (init := acc) fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc
   else
-    let elabFieldName (e field : Syntax) (explicit : Bool) := do
-      let newLVals := field.identComponents.map fun comp =>
-        -- We use `none` in `suffix?` since `field` can't be part of a composite name
-        LVal.fieldName comp comp.getId.getString! none f
+    let elabFieldName (e field : Syntax) (explicitUnivs : List Level) := do
+      let comps := field.identComponents
+      let lastIdx := comps.length - 1
+      let newLVals := comps.mapIdx fun idx comp =>
+        let levels := if idx = lastIdx then explicitUnivs else []
+        let suffix? := none -- We use `none` since the field can't be part of a composite name
+        LVal.fieldName comp comp.getId.getString! levels suffix? f
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    let elabFieldIdx (e idxStx : Syntax) (explicit : Bool) := do
+    let elabFieldIdx (e idxStx : Syntax) (explicitUnivs : List Level) := do
       let some idx := idxStx.isFieldIdx?
         | throwError "Internal error: Unexpected field index syntax `{idxStx}`"
-      elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) (explicit : Bool) : TermElabM (Array (TermElabResult Expr)) := do
+      elabAppFn e (LVal.fieldIdx idxStx idx explicitUnivs :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
+    let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) : TermElabM (Array (TermElabResult Expr)) := do
       let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes explicitUnivs expectedType?
       -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
       elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
     match f with
-    | `($(e).$idx:fieldIdx) => elabFieldIdx e idx explicit
-    | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx explicit
-    | `($(e).$field:ident) => elabFieldName e field explicit
-    | `($e |>.$field:ident) => elabFieldName e field explicit
-    | `(@$(e).$idx:fieldIdx) => elabFieldIdx e idx (explicit := true)
-    | `(@$(e).$field:ident) => elabFieldName e field (explicit := true)
+    | `($(e).$idx:fieldIdx)
+    | `($e |>.$idx:fieldIdx) =>
+      elabFieldIdx e idx []
+    | `($(e).$idx:fieldIdx.{$us,*})
+    | `($e |>.$idx:fieldIdx.{$us,*}) =>
+      let us ← elabExplicitUnivs us
+      elabFieldIdx e idx us
+    | `($(e).$field:ident)
+    | `($e |>.$field:ident) =>
+      elabFieldName e field []
+    | `($(e).$field:ident.{$us,*})
+    | `($e |>.$field:ident.{$us,*}) =>
+      let us ← elabExplicitUnivs us
+      elabFieldName e field us
     | `($_:ident@$_:term) =>
       throwError m!"Expected a function, but found the named pattern{indentD f}"
         ++ .note m!"Named patterns `<identifier>@<term>` can only be used when pattern-matching"
@@ -1942,12 +1959,15 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `($id:ident.{$us,*}) => do
       let us ← elabExplicitUnivs us
       elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc
-    | `(.$id:ident) => elabDottedIdent id [] explicit
+    | `(.$id:ident) => elabDottedIdent id []
     | `(.$id:ident.{$us,*}) =>
       let us ← elabExplicitUnivs us
-      elabDottedIdent id us explicit
+      elabDottedIdent id us
     | `(@$_:ident)
     | `(@$_:ident.{$_us,*})
+    | `(@$(_).$_:fieldIdx)
+    | `(@$(_).$_:ident)
+    | `(@$(_).$_:ident.{$_us,*})
     | `(@.$_:ident)
     | `(@.$_:ident.{$_us,*}) =>
       elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
@@ -2084,10 +2104,10 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 @[builtin_term_elab dotIdent] def elabDotIdent : TermElab := elabAtom
 @[builtin_term_elab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
 @[builtin_term_elab pipeProj] def elabPipeProj : TermElab
-  | `($e |>.%$tk$f $args*), expectedType? =>
+  | `($e |>.%$tk$f$[.{$us?,*}]? $args*), expectedType? =>
     universeConstraintsCheckpoint do
       let (namedArgs, args, ellipsis) ← expandArgs args
-      let mut stx ← `($e |>.%$tk$f)
+      let mut stx ← `($e |>.%$tk$f$[.{$us?,*}]?)
       if let (some startPos, some stopPos) := (e.raw.getPos?, f.raw.getTailPos?) then
         stx := ⟨stx.raw.setInfo <| .synthetic (canonical := true) startPos stopPos⟩
       elabAppAux stx namedArgs args (ellipsis := ellipsis) expectedType?
@@ -2095,15 +2115,16 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 
 @[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
   match stx with
-  | `(@$_:ident)           => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
-  | `(@$_:ident.{$_us,*})  => elabAtom stx expectedType?
-  | `(@$(_).$_:fieldIdx)   => elabAtom stx expectedType?
-  | `(@$(_).$_:ident)      => elabAtom stx expectedType?
-  | `(@.$_:ident)          => elabAtom stx expectedType?
-  | `(@.$_:ident.{$_us,*}) => elabAtom stx expectedType?
-  | `(@($t))               => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | `(@$t)                 => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | _                      => throwUnsupportedSyntax
+  | `(@$_:ident)               => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
+  | `(@$_:ident.{$_us,*})      => elabAtom stx expectedType?
+  | `(@$(_).$_:fieldIdx)       => elabAtom stx expectedType?
+  | `(@$(_).$_:ident)          => elabAtom stx expectedType?
+  | `(@$(_).$_:ident.{$_us,*}) => elabAtom stx expectedType?
+  | `(@.$_:ident)              => elabAtom stx expectedType?
+  | `(@.$_:ident.{$_us,*})     => elabAtom stx expectedType?
+  | `(@($t))                   => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | `(@$t)                     => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | _                          => throwUnsupportedSyntax
 
 @[builtin_term_elab choice] def elabChoice : TermElab := elabAtom
 @[builtin_term_elab proj] def elabProj : TermElab := elabAtom

src/Lean/Elab/Deriving/Inhabited.lean

@@ -25,25 +25,23 @@ private def mkInhabitedInstanceUsing (inductiveTypeName : Name) (ctorName : Name
   | none =>
     return false
 where
-  addLocalInstancesForParamsAux {α} (k : LocalInst2Index → TermElabM α) : List Expr → Nat → LocalInst2Index → TermElabM α
-    | [], _, map    => k map
-    | x::xs, i, map =>
+  addLocalInstancesForParamsAux {α} (k : Array Expr → LocalInst2Index → TermElabM α) : List Expr → Nat → Array Expr → LocalInst2Index → TermElabM α
+    | [],    _, insts, map => k insts map
+    | x::xs, i, insts, map =>
       try
         let instType ← mkAppM `Inhabited #[x]
-        if (← isTypeCorrect instType) then
-          withLocalDeclD (← mkFreshUserName `inst) instType fun inst => do
-            trace[Elab.Deriving.inhabited] "adding local instance {instType}"
-            addLocalInstancesForParamsAux k xs (i+1) (map.insert inst.fvarId! i)
-        else
-          addLocalInstancesForParamsAux k xs (i+1) map
+        check instType
+        withLocalDecl (← mkFreshUserName `inst) .instImplicit instType fun inst => do
+          trace[Elab.Deriving.inhabited] "adding local instance {instType}"
+          addLocalInstancesForParamsAux k xs (i+1) (insts.push inst) (map.insert inst.fvarId! i)
       catch _ =>
-        addLocalInstancesForParamsAux k xs (i+1) map
+        addLocalInstancesForParamsAux k xs (i+1) insts map
 
-  addLocalInstancesForParams {α} (xs : Array Expr) (k : LocalInst2Index → TermElabM α) : TermElabM α := do
+  addLocalInstancesForParams {α} (xs : Array Expr) (k : Array Expr → LocalInst2Index → TermElabM α) : TermElabM α := do
     if addHypotheses then
-      addLocalInstancesForParamsAux k xs.toList 0 {}
+      addLocalInstancesForParamsAux k xs.toList 0 #[] {}
     else
-      k {}
+      k #[] {}
 
   collectUsedLocalsInsts (usedInstIdxs : IndexSet) (localInst2Index : LocalInst2Index) (e : Expr) : IndexSet :=
     if localInst2Index.isEmpty then
@@ -58,58 +56,88 @@ where
       runST (fun _ => visit |>.run usedInstIdxs) |>.2
 
   /-- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters
-     at position `i` and `i ∈ assumingParamIdxs`. -/
-  mkInstanceCmdWith (assumingParamIdxs : IndexSet) : TermElabM Syntax := do
-    let ctx ← Deriving.mkContext ``Inhabited "inhabited" inductiveTypeName
+     at position `i` and `i ∈ usedInstIdxs`. -/
+  mkInstanceCmdWith (instId : Ident) (usedInstIdxs : IndexSet) (auxFunId : Ident) : TermElabM Syntax := do
     let indVal ← getConstInfoInduct inductiveTypeName
-    let ctorVal ← getConstInfoCtor ctorName
     let mut indArgs := #[]
     let mut binders := #[]
     for i in *...indVal.numParams + indVal.numIndices do
       let arg := mkIdent (← mkFreshUserName `a)
       indArgs := indArgs.push arg
-      let binder ← `(bracketedBinderF| { $arg:ident })
-      binders := binders.push binder
-      if assumingParamIdxs.contains i then
-        let binder ← `(bracketedBinderF| [Inhabited $arg:ident ])
-        binders := binders.push binder
+      binders := binders.push <| ← `(bracketedBinderF| { $arg:ident })
+      if usedInstIdxs.contains i then
+        binders := binders.push <| ← `(bracketedBinderF| [Inhabited $arg:ident ])
     let type ← `(@$(mkCIdent inductiveTypeName):ident $indArgs:ident*)
-    let mut ctorArgs := #[]
-    for _ in *...ctorVal.numParams do
-      ctorArgs := ctorArgs.push (← `(_))
-    for _ in *...ctorVal.numFields do
-      ctorArgs := ctorArgs.push (← ``(Inhabited.default))
-    let val ← `(@$(mkIdent ctorName):ident $ctorArgs*)
-    let ctx ← mkContext ``Inhabited "default" inductiveTypeName
-    let auxFunName := ctx.auxFunNames[0]!
-    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type := $val
-      instance $(mkIdent ctx.instName):ident $binders:bracketedBinder* : Inhabited $type := ⟨$(mkIdent auxFunName)⟩)
+    `(instance $instId:ident $binders:bracketedBinder* : Inhabited $type := ⟨$auxFunId⟩)
 
+  solveMVarsWithDefault (e : Expr) : TermElabM Unit := do
+    let mvarIds ← getMVarsNoDelayed e
+    mvarIds.forM fun mvarId => mvarId.withContext do
+      unless ← mvarId.isAssigned do
+        let type ← mvarId.getType
+        withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"synthesizing Inhabited instance for{inlineExprTrailing type}") do
+          let val ← mkDefault type
+          mvarId.assign val
+          trace[Elab.Deriving.inhabited] "value:{inlineExprTrailing val}"
 
-  mkInstanceCmd? : TermElabM (Option Syntax) := do
-    let ctorVal ← getConstInfoCtor ctorName
-    forallTelescopeReducing ctorVal.type fun xs _ =>
-      addLocalInstancesForParams xs[*...ctorVal.numParams] fun localInst2Index => do
-        let mut usedInstIdxs := {}
-        let mut ok := true
-        for h : i in ctorVal.numParams...xs.size do
-          let x := xs[i]
-          let instType ← mkAppM `Inhabited #[(← inferType x)]
-          trace[Elab.Deriving.inhabited] "checking {instType} for `{ctorName}`"
-          match (← trySynthInstance instType) with
-          | LOption.some e =>
-            usedInstIdxs := collectUsedLocalsInsts usedInstIdxs localInst2Index e
-          | _ =>
-            trace[Elab.Deriving.inhabited] "failed to generate instance using `{ctorName}` {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
-            ok := false
-            break
-        if !ok then
-          return none
+  mkDefaultValue (indVal : InductiveVal) : TermElabM (Expr × Expr × IndexSet) := do
+    let us := indVal.levelParams.map Level.param
+    forallTelescopeReducing indVal.type fun xs _ =>
+    withImplicitBinderInfos xs do
+    addLocalInstancesForParams xs[0...indVal.numParams] fun insts localInst2Index => do
+      let type := mkAppN (.const inductiveTypeName us) xs
+      let val ←
+        if isStructure (← getEnv) inductiveTypeName then
+          withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using structure instance elaborator") do
+            let stx ← `(structInst| {..})
+            withoutErrToSorry <| elabTermAndSynthesize stx type
         else
-          trace[Elab.Deriving.inhabited] "inhabited instance using `{ctorName}` {if addHypotheses then "(assuming parameters are inhabited)" else ""} {usedInstIdxs.toList}"
-          let cmd ← mkInstanceCmdWith usedInstIdxs
-          trace[Elab.Deriving.inhabited] "\n{cmd}"
-          return some cmd
+          withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using constructor `{.ofConstName ctorName}`") do
+            let val := mkAppN (.const ctorName us) xs[0...indVal.numParams]
+            let (mvars, _, type') ← forallMetaTelescopeReducing (← inferType val)
+            unless ← isDefEq type type' do
+              throwError "cannot unify{indentExpr type}\nand type of constructor{indentExpr type'}"
+            pure <| mkAppN val mvars
+      solveMVarsWithDefault val
+      let val ← instantiateMVars val
+      if val.hasMVar then
+        throwError "default value contains metavariables{inlineExprTrailing val}"
+      let fvars := Lean.collectFVars {} val
+      let insts' := insts.filter fvars.visitedExpr.contains
+      let usedInstIdxs := collectUsedLocalsInsts {} localInst2Index val
+      assert! insts'.size == usedInstIdxs.size
+      trace[Elab.Deriving.inhabited] "inhabited instance using{inlineExpr val}{if insts'.isEmpty then m!"" else m!"(assuming parameters {insts'} are inhabited)"}"
+      let xs' := xs ++ insts'
+      let auxType ← mkForallFVars xs' type
+      let auxVal ← mkLambdaFVars xs' val
+      return (auxType, auxVal, usedInstIdxs)
+
+  mkInstanceCmd? : TermElabM (Option Syntax) :=
+    withExporting (isExporting := !isPrivateName ctorName) do
+      let ctx ← mkContext ``Inhabited "default" inductiveTypeName
+      let auxFunName := (← getCurrNamespace) ++ ctx.auxFunNames[0]!
+      let indVal ← getConstInfoInduct inductiveTypeName
+      let (auxType, auxVal, usedInstIdxs) ←
+        try
+          withDeclName auxFunName do mkDefaultValue indVal
+        catch e =>
+          trace[Elab.Deriving.inhabited] "error: {e.toMessageData}"
+          return none
+      addDecl <| .defnDecl <| ← mkDefinitionValInferringUnsafe
+        (name        := auxFunName)
+        (levelParams := indVal.levelParams)
+        (type        := auxType)
+        (value       := auxVal)
+        (hints       := ReducibilityHints.regular (getMaxHeight (← getEnv) auxVal + 1))
+      if isMarkedMeta (← getEnv) inductiveTypeName then
+        modifyEnv (markMeta · auxFunName)
+      unless (← read).isNoncomputableSection do
+        compileDecls #[auxFunName]
+      enableRealizationsForConst auxFunName
+      trace[Elab.Deriving.inhabited] "defined {.ofConstName auxFunName}"
+      let cmd ← mkInstanceCmdWith (mkIdent ctx.instName) usedInstIdxs (mkCIdent auxFunName)
+      trace[Elab.Deriving.inhabited] "\n{cmd}"
+      return some cmd
 
 private def mkInhabitedInstance (declName : Name) : CommandElabM Unit := do
   withoutExposeFromCtors declName do

src/Lean/Elab/Import.lean

@@ -10,6 +10,7 @@ public import Lean.Parser.Module
 meta import Lean.Parser.Module
 import Lean.Compiler.ModPkgExt
 public import Lean.DeprecatedModule
+import Init.Data.String.Modify
 
 public section
 
@@ -97,6 +98,43 @@ def checkDeprecatedImports
       | none => messages
     | none => messages
 
+private def osForbiddenChars : Array Char :=
+  #['<', '>', '"', '|', '?', '*', '!']
+
+private def osForbiddenNames : Array String :=
+  #["CON", "PRN", "AUX", "NUL",
+    "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9",
+    "COM¹", "COM²", "COM³",
+    "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9",
+    "LPT¹", "LPT²", "LPT³"]
+
+private def checkComponentPortability (comp : String) : Option String :=
+  if osForbiddenNames.contains comp.toUpper then
+    some s!"'{comp}' is a reserved file name on some operating systems"
+  else if let some c := osForbiddenChars.find? (comp.contains ·) then
+    some s!"contains character '{c}' which is forbidden on some operating systems"
+  else
+    none
+
+def checkModuleNamePortability
+    (mainModule : Name) (inputCtx : Parser.InputContext) (startPos : String.Pos.Raw)
+    (messages : MessageLog) : MessageLog :=
+  go mainModule messages
+where
+  go : Name → MessageLog → MessageLog
+    | .anonymous, messages => messages
+    | .str parent s, messages =>
+      let messages := match checkComponentPortability s with
+        | some reason => messages.add {
+            fileName := inputCtx.fileName
+            pos := inputCtx.fileMap.toPosition startPos
+            severity := .error
+            data := s!"module name '{mainModule}' is not portable: {reason}"
+          }
+        | none => messages
+      go parent messages
+    | .num parent _, messages => go parent messages
+
 def processHeaderCore
     (startPos : String.Pos.Raw) (imports : Array Import) (isModule : Bool)
     (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
@@ -124,6 +162,7 @@ def processHeaderCore
     pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
   let env := env.setMainModule mainModule |>.setModulePackage package?
   let messages := checkDeprecatedImports env imports opts inputCtx startPos messages headerStx? origHeaderStx?
+  let messages := checkModuleNamePortability mainModule inputCtx startPos messages
   return (env, messages)
 
 /--

src/Lean/Elab/Quotation/Precheck.lean

@@ -113,7 +113,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
     if (← read).quotLCtx.contains val then
       return
     let rs ← try resolveName stx val [] [] catch _ => pure []
-    for (e, _) in rs do
+    for (e, _, _) in rs do
       match e with
       | Expr.fvar _      .. =>
         if quotPrecheck.allowSectionVars.get (← getOptions) && (← isSectionVariable e) then

src/Lean/Elab/Term/TermElabM.lean

@@ -232,7 +232,10 @@ structure TacticFinishedSnapshot extends Language.Snapshot where
   state? : Option SavedState
   /-- Untyped snapshots from `logSnapshotTask`, saved at this level for cancellation. -/
   moreSnaps : Array (SnapshotTask SnapshotTree)
-deriving Inhabited
+
+instance : Inhabited TacticFinishedSnapshot where
+  default := { toSnapshot := default, state? := default, moreSnaps := default }
+
 instance : ToSnapshotTree TacticFinishedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, s.moreSnaps⟩
 
@@ -246,7 +249,10 @@ structure TacticParsedSnapshot extends Language.Snapshot where
   finished : SnapshotTask TacticFinishedSnapshot
   /-- Tasks for subsequent, potentially parallel, tactic steps. -/
   next     : Array (SnapshotTask TacticParsedSnapshot) := #[]
-deriving Inhabited
+
+instance : Inhabited TacticParsedSnapshot where
+  default := { toSnapshot := default, stx := default, finished := default }
+
 partial instance : ToSnapshotTree TacticParsedSnapshot where
   toSnapshotTree := go where
     go := fun s => ⟨s.toSnapshot,
@@ -627,13 +633,13 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl
   `[LVal.fieldName "foo", LVal.fieldIdx 1]`.
 -/
 inductive LVal where
-  | fieldIdx  (ref : Syntax) (i : Nat)
+  | fieldIdx  (ref : Syntax) (i : Nat) (levels : List Level)
   /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierarchical/composite name.
   `ref` is the syntax object representing the field. `fullRef` includes the LHS. -/
-  | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (fullRef : Syntax)
+  | fieldName (ref : Syntax) (name : String) (levels : List Level) (suffix? : Option Name) (fullRef : Syntax)
 
 def LVal.getRef : LVal → Syntax
-  | .fieldIdx ref _    => ref
+  | .fieldIdx ref ..   => ref
   | .fieldName ref ..  => ref
 
 def LVal.isFieldName : LVal → Bool
@@ -642,8 +648,11 @@ def LVal.isFieldName : LVal → Bool
 
 instance : ToString LVal where
   toString
-    | .fieldIdx _ i     => toString i
-    | .fieldName _ n .. => n
+    | .fieldIdx _ i levels ..  => toString i ++ levelsToString levels
+    | .fieldName _ n levels .. => n ++ levelsToString levels
+where
+  levelsToString levels :=
+    if levels.isEmpty then "" else ".{" ++ String.intercalate "," (levels.map toString) ++ "}"
 
 /-- Return the name of the declaration being elaborated if available. -/
 def getDeclName? : TermElabM (Option Name) := return (← read).declName?
@@ -2111,8 +2120,10 @@ def checkDeprecated (ref : Syntax) (e : Expr) : TermElabM Unit := do
 @[inline] def withoutCheckDeprecated [MonadWithReaderOf Context m] : m α → m α :=
   withTheReader Context (fun ctx => { ctx with checkDeprecated := false })
 
-private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
+private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String × List Level)) := do
   candidates.foldlM (init := []) fun result (declName, projs) => do
+    -- levels apply to the last projection, not the constant
+    let (constLevels, projLevels) := if projs.isEmpty then (explicitLevels, []) else ([], explicitLevels)
     -- TODO: better support for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail.
     /-
     We disable `checkDeprecated` here because there may be many overloaded symbols.
@@ -2121,25 +2132,38 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
     At `elabAppFnId`, we perform the check when converting the list returned by `resolveName'` into a list of
     `TermElabResult`s.
     -/
-    let const ← withoutCheckDeprecated <| mkConst declName explicitLevels
-    return (const, projs) :: result
+    let const ← withoutCheckDeprecated <| mkConst declName constLevels
+    return (const, projs, projLevels) :: result
 
 def throwInvalidExplicitUniversesForLocal {α} (e : Expr) : TermElabM α :=
   throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
 
-def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
+/--
+  Gives all resolutions of the name `n`.
+
+- `explicitLevels` provides a prefix of level parameters to the constant. For resolutions with a projection
+  component, the levels are not used, since they must apply to the last projection, not the constant.
+  In that case, the third component of the tuple is `explicitLevels`.
+-/
+def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String × List Level)) := do
   addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
+  let processLocal (e : Expr) (projs : List String) := do
+    if projs.isEmpty then
+      if explicitLevels.isEmpty then
+        return [(e, [], [])]
+      else
+        throwInvalidExplicitUniversesForLocal e
+    else
+      return [(e, projs, explicitLevels)]
   if let some (e, projs) ← resolveLocalName n then
-    unless explicitLevels.isEmpty do
-      throwInvalidExplicitUniversesForLocal e
-    return [(e, projs)]
+    return ← processLocal e projs
   let preresolved := preresolved.filterMap fun
     | .decl n projs => some (n, projs)
     | _             => none
   -- check for section variable capture by a quotation
   let ctx ← read
   if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
-    return [(e, projs)]  -- section variables should shadow global decls
+    return ← processLocal e projs  -- section variables should shadow global decls
   if preresolved.isEmpty then
     mkConsts (← realizeGlobalName n) explicitLevels
   else
@@ -2148,14 +2172,17 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
 /--
   Similar to `resolveName`, but creates identifiers for the main part and each projection with position information derived from `ident`.
   Example: Assume resolveName `v.head.bla.boo` produces `(v.head, ["bla", "boo"])`, then this method produces
-  `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/
-def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax)) := do
+  `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`.
+
+  See the comment there about `explicitLevels` and the meaning of the `List Level` component of the returned tuple.
+-/
+def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax × List Level)) := do
   let .ident _ _ n preresolved := ident
     | throwError "identifier expected"
   let r ← resolveName ident n preresolved explicitLevels expectedType?
-  let rc ← r.mapM fun (c, fields) => do
+  let rc ← r.mapM fun (c, fields, levels) => do
     let ids := ident.identComponents (nFields? := fields.length)
-    return (c, ids.head!, ids.tail!)
+    return (c, ids.head!, ids.tail!, levels)
   return (n, rc)
 
 
@@ -2163,7 +2190,7 @@ def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (
   match stx with
   | .ident _ _ val preresolved =>
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
-    let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty
+    let rs := rs.filter fun ⟨_, projs, _⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f
     match fs with
     | []  => return none

src/Lean/Language/Basic.lean

@@ -67,7 +67,9 @@ structure Snapshot where
   `diagnostics`) occurred that prevents processing of the remainder of the file.
   -/
   isFatal := false
-deriving Inhabited
+
+instance : Inhabited Snapshot where
+  default := { desc := "", diagnostics := default }
 
 /-- Range that is marked as being processed by the server while a task is running. -/
 inductive SnapshotTask.ReportingRange where
@@ -236,7 +238,10 @@ partial def SnapshotTask.cancelRec [ToSnapshotTree α] (t : SnapshotTask α) : B
 
 /-- Snapshot type without child nodes. -/
 structure SnapshotLeaf extends Snapshot
-deriving Inhabited, TypeName
+deriving TypeName
+
+instance : Inhabited SnapshotLeaf where
+  default := { toSnapshot := default }
 
 instance : ToSnapshotTree SnapshotLeaf where
   toSnapshotTree s := SnapshotTree.mk s.toSnapshot #[]

src/Lean/Meta/WrapInstance.lean

@@ -9,8 +9,8 @@ prelude
 public import Lean.Meta.Closure
 public import Lean.Meta.SynthInstance
 public import Lean.Meta.CtorRecognizer
-
-public section
+public import Lean.Meta.AppBuilder
+import Lean.Structure
 
 /-!
 # Instance Wrapping
@@ -25,22 +25,30 @@ Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
 `wrapInstance` constructs a result instance as follows, executing all steps at
 `instances` transparency:
 
-1. If `I'` is not a class, return `i` unchanged.
+1. If `I'` is not a class application, return `i` unchanged.
 2. If `I'` is a proposition, wrap `i` in an auxiliary theorem of type `I'` and return it
    (controlled by `backward.inferInstanceAs.wrap.instances`).
 3. Reduce `i` to whnf.
-4. If `i` is not a constructor application: if the type of `i` is already defeq to `I'`,
+4. If `i` is not a constructor application: if `I` is already defeq to `I'`,
    return `i`; otherwise wrap it in an auxiliary definition of type `I'` and return it
    (controlled by `backward.inferInstanceAs.wrap.instances`).
-5. Otherwise, for `i = ctor a₁ ... aₙ` with `ctor : C ?p₁ ... ?pₙ`:
-   - Unify `C ?p₁ ... ?pₙ` with `I'`.
-   - Return a new application `ctor a₁' ... aₙ' : I'` where each `aᵢ'` is constructed as:
+5. Otherwise, if `i` is an application of `ctor` of class `C`:
+   - Unify the conclusion of the type of `ctor` with `I'` to obtain adjusted field type `Fᵢ'` for
+     each field.
+   - Return a new application `ctor ... : I'` where the fields are adjusted as follows:
      - If the field type is a proposition: assign directly if types are defeq, otherwise
        wrap in an auxiliary theorem.
-     - If the field type is a class: first try to reuse an existing synthesized instance
-       for the target type (controlled by `backward.inferInstanceAs.wrap.reuseSubInstances`);
-       if that fails, recurse with source instance `aᵢ` and expected type `?pᵢ`.
-     - Otherwise (data field): assign directly if types are defeq, otherwise wrap in an
+     - If the field is a parent field (subobject) `p : P`: first try to reuse an existing
+       instance that can be synthesized for `P` (controlled by
+       `backward.inferInstanceAs.wrap.reuseSubInstances`) in order to preserve defeqs; if that
+       fails, recurse.
+     - If it is a field of a flattened parent class `C'` and
+       `backward.inferInstanceAs.wrap.reuseSubInstances` is true, try synthesizing an instance of
+       `C'` for `I'` and if successful, use the corresponding projection of the found instance in
+       order to preserve defeqs; otherwise, continue.
+       - Specifically, construct the chain of base projections from `C` to `C'` applied to `_ : I'`
+         and infer its type to obtain an appropriate application of `C'` for the instance search.
+     - Otherwise (non-inherited data field): assign directly if types are defeq, otherwise wrap in an
        auxiliary definition to fix the type (controlled by `backward.inferInstanceAs.wrap.data`).
 
 ## Options
@@ -56,34 +64,36 @@ Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
 
 namespace Lean.Meta
 
-register_builtin_option backward.inferInstanceAs.wrap : Bool := {
+public register_builtin_option backward.inferInstanceAs.wrap : Bool := {
   defValue := true
   descr := "wrap instance bodies in `inferInstanceAs` and the default `deriving` handler"
 }
 
-register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
+public register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
   defValue := true
   descr := "when recursing into sub-instances, reuse existing instances for the target type instead of re-wrapping them, which can be important to avoid non-defeq instance diamonds"
 }
 
-register_builtin_option backward.inferInstanceAs.wrap.instances : Bool := {
+public register_builtin_option backward.inferInstanceAs.wrap.instances : Bool := {
   defValue := true
   descr := "wrap non-reducible instances in auxiliary definitions to fix their types"
 }
 
-register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
+public register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
   defValue := true
   descr := "wrap data fields in auxiliary definitions to fix their types"
 }
 
 builtin_initialize registerTraceClass `Meta.wrapInstance
 
+open Meta
+
 /--
 Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
 Non-instance-implicit arguments are assigned from the original application's arguments.
 If the function is over-applied, extra arguments are preserved.
 -/
-def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
+public def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
   let fn := type.getAppFn
   let args := type.getAppArgs
   let (mvars, bis, _) ← forallMetaTelescope (← inferType fn)
@@ -93,11 +103,38 @@ def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
   let args := mvars ++ args.drop mvars.size
   instantiateMVars (mkAppN fn args)
 
+partial def getFieldOrigin (structName field : Name) : MetaM (Name × StructureFieldInfo) := do
+  let env ← getEnv
+  for parent in getStructureParentInfo env structName do
+    if (findField? env parent.structName field).isSome then
+      return ← getFieldOrigin parent.structName field
+  let some fi := getFieldInfo? env structName field
+    | throwError "no such field {field} in {structName}"
+  return (structName, fi)
+
+/-- Projects application of a structure type to corresponding application of a parent structure. -/
+def getParentStructType? (structName parentStructName : Name) (structType : Expr) : MetaM (Option Expr) := OptionT.run do
+  let env ← getEnv
+  let some path := getPathToBaseStructure? env parentStructName structName | failure
+  withLocalDeclD `self structType fun self => do
+    let proj ← path.foldlM (init := self) fun e projFn => do
+      let ty ← whnf (← inferType e)
+      let .const _ us := ty.getAppFn
+        | trace[Meta.wrapInstance] "could not reduce type `{ty}`"
+          failure
+      let params := ty.getAppArgs
+      pure <| mkApp (mkAppN (.const projFn us) params) e
+    let projTy ← whnf <| ← inferType proj
+    if projTy.containsFVar self.fvarId! then
+      trace[Meta.wrapInstance] "parent type depends on instance fields{indentExpr projTy}"
+      failure
+    return projTy
+
 /--
 Wrap an instance value so its type matches the expected type exactly.
 See the module docstring for the full algorithm specification.
 -/
-partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
+public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
     (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
   withTraceNode `Meta.wrapInstance
       (fun _ => return m!"type: {expectedType}") do
@@ -155,8 +192,10 @@ partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
           else
             trace[Meta.wrapInstance] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
             mvarId.assign (← mkAuxTheorem argExpectedType arg (zetaDelta := true))
+          continue
+
         -- Recurse into instance arguments of the constructor
-        else if (← isClass? argExpectedType).isSome then
+        if (← isClass? argExpectedType).isSome then
           if backward.inferInstanceAs.wrap.reuseSubInstances.get (← getOptions) then
             -- Reuse existing instance for the target type if any. This is especially important when recursing
             -- as it guarantees subinstances of overlapping instances are defeq under more than just
@@ -170,22 +209,35 @@ partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
 
           mvarId.assign (← wrapInstance arg argExpectedType (compile := compile)
             (logCompileErrors := logCompileErrors) (isMeta := isMeta))
-        else
-          -- For data fields, assign directly or wrap in aux def to fix types.
-          if backward.inferInstanceAs.wrap.data.get (← getOptions) then
-            let argType ← inferType arg
-            if ← isDefEq argExpectedType argType then
-              mvarId.assign arg
-            else
-              let name ← mkAuxDeclName
-              mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
-              setInlineAttribute name
-              if isMeta then modifyEnv (markMeta · name)
-              if compile then
-                compileDecls (logErrors := logCompileErrors) #[name]
-              enableRealizationsForConst name
-          else
-            mvarId.assign arg
-      return mkAppN f (← mvars.mapM instantiateMVars)
+          continue
 
-end Lean.Meta
+        if backward.inferInstanceAs.wrap.reuseSubInstances.get (← getOptions) then
+          let (baseClassName, fieldInfo) ← getFieldOrigin className mvarDecl.userName
+          if baseClassName != className then
+            trace[Meta.wrapInstance] "found inherited field `{mvarDecl.userName}` from parent `{baseClassName}`"
+            if let some baseClassType ← getParentStructType? className baseClassName expectedType then
+              try
+                if let .some existingBaseClassInst ← trySynthInstance baseClassType then
+                  trace[Meta.wrapInstance] "using projection of existing instance `{existingBaseClassInst}`"
+                  mvarId.assign (← mkProjection existingBaseClassInst fieldInfo.fieldName)
+                  continue
+                trace[Meta.wrapInstance] "did not find existing instance for `{baseClassName}`"
+              catch e =>
+                trace[Meta.wrapInstance] "error when attempting to reuse existing instance for `{baseClassName}`: {e.toMessageData}"
+
+        -- For data fields, assign directly or wrap in aux def to fix types.
+        if backward.inferInstanceAs.wrap.data.get (← getOptions) then
+          let argType ← inferType arg
+          if ← isDefEq argExpectedType argType then
+            mvarId.assign arg
+          else
+            let name ← mkAuxDeclName
+            mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
+            setInlineAttribute name
+            if isMeta then modifyEnv (markMeta · name)
+            if compile then
+              compileDecls (logErrors := logCompileErrors) #[name]
+            enableRealizationsForConst name
+        else
+          mvarId.assign arg
+      return mkAppN f (← mvars.mapM instantiateMVars)

src/Lean/Parser/Basic.lean

@@ -1115,11 +1115,6 @@ def symbolNoAntiquot (sym : String) : Parser :=
   { info := symbolInfo sym
     fn   := symbolFn sym }
 
-def checkTailNoWs (prev : Syntax) : Bool :=
-  match prev.getTailInfo with
-  | .original _ _ trailing _ => trailing.stopPos == trailing.startPos
-  | _                        => false
-
 /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
     parsing local tokens that have not been added to the token table (but may have
     been so by some unrelated code).
@@ -1168,13 +1163,18 @@ partial def strAux (sym : String) (errorMsg : String) (j : String.Pos.Raw) :Pars
       else parse (j.next' sym h₁) c (s.next' c i h₂)
   parse j
 
+private def pickNonNone (stack : SyntaxStack) : Syntax :=
+  match stack.toSubarray.findRev? fun stx => !stx.isNone with
+  | none => Syntax.missing
+  | some stx => stx
+
 def checkTailWs (prev : Syntax) : Bool :=
   match prev.getTailInfo with
   | .original _ _ trailing _ => trailing.stopPos > trailing.startPos
   | _                        => false
 
 def checkWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
-  let prev := s.stxStack.back
+  let prev := pickNonNone s.stxStack
   if checkTailWs prev then s else s.mkError errorMsg
 
 /-- The `ws` parser requires that there is some whitespace at this location.
@@ -1202,10 +1202,10 @@ This parser has arity 0 - it does not capture anything. -/
   info := epsilonInfo
   fn   := checkLinebreakBeforeFn errorMsg
 
-private def pickNonNone (stack : SyntaxStack) : Syntax :=
-  match stack.toSubarray.findRev? fun stx => !stx.isNone with
-  | none => Syntax.missing
-  | some stx => stx
+def checkTailNoWs (prev : Syntax) : Bool :=
+  match prev.getTailInfo with
+  | .original _ _ trailing _ => trailing.stopPos == trailing.startPos
+  | _                        => false
 
 def checkNoWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
   let prev := pickNonNone s.stxStack

src/Lean/Parser/Command.lean

@@ -122,7 +122,9 @@ def declModifiers (inline : Bool) := leading_parser
 /-- `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names -/
 -- @[builtin_doc] -- FIXME: suppress the hover
 def declId := leading_parser
-  ident >> optional (".{" >> sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}")
+  ident >>
+  optional (checkNoWsBefore "no space before '.{'" >> ".{" >>
+    sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}")
 /-- `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` -/
 -- @[builtin_doc] -- FIXME: suppress the hover
 def declSig := leading_parser

src/Lean/Parser/Term.lean

@@ -889,14 +889,21 @@ def isIdent (stx : Syntax) : Bool :=
   -- antiquotations should also be allowed where an identifier is expected
   stx.isAntiquot || stx.isIdent
 
-def isIdentOrDotIdent (stx : Syntax) : Bool :=
-  isIdent stx || stx.isOfKind ``dotIdent
+/-- Predicate for what `explicitUniv` can follow. It is only meant to be used on an identifier
+that becomes the head constant of an application. -/
+def isIdentOrDotIdentOrProj (stx : Syntax) : Bool :=
+  isIdent stx || stx.isOfKind ``dotIdent || stx.isOfKind ``proj
 
-/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
-@[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
-  checkStackTop isIdentOrDotIdent "expected preceding identifier" >>
+/-- Syntax for `.{u, ...}` itself. Generally the `explicitUniv` trailing parser suffices.
+However, for `e |>.x.{u} a1 a2 a3` notation we need to be able to express explicit universes in the
+middle of the syntax. -/
+def explicitUnivSuffix : Parser :=
   checkNoWsBefore "no space before '.{'" >> ".{" >>
   sepBy1 levelParser ", " >> "}"
+/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
+@[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
+  checkStackTop isIdentOrDotIdentOrProj "expected preceding identifier" >>
+  explicitUnivSuffix
 /-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
 If present, the identifier `h` is bound to a proof of `x = e`. -/
 @[builtin_term_parser] def namedPattern : TrailingParser := trailing_parser
@@ -909,7 +916,7 @@ If present, the identifier `h` is bound to a proof of `x = e`. -/
 It is especially useful for avoiding parentheses with repeated applications.
 -/
 @[builtin_term_parser] def pipeProj   := trailing_parser:minPrec
-  " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
+  " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> optional explicitUnivSuffix >> many argument
 @[builtin_term_parser] def pipeCompletion := trailing_parser:minPrec
   " |>."
 

src/lake/Lake/Build/Library.lean

@@ -24,6 +24,11 @@ namespace Lake
 
 /-! ## Build Lean & Static Lib -/
 
+private structure ModuleCollection where
+  mods : Array Module := #[]
+  modSet : ModuleSet := ∅
+  hasErrors : Bool := false
+
 /--
 Collect the local modules of a library.
 That is, the modules from `getModuleArray` plus their local transitive imports.
@@ -31,23 +36,27 @@ That is, the modules from `getModuleArray` plus their local transitive imports.
 private partial def LeanLib.recCollectLocalModules
   (self : LeanLib) : FetchM (Job (Array Module))
 := ensureJob do
-  let mut mods := #[]
-  let mut modSet := ModuleSet.empty
+  let mut col : ModuleCollection := {}
   for mod in (← self.getModuleArray) do
-    (mods, modSet) ← go mod mods modSet
-  return Job.pure mods
+    col ← go mod col
+  if col.hasErrors then
+    -- This is not considered a fatal error because we want the modules
+    -- built to provide better error categorization in the monitor.
+    logError s!"{self.name}: some modules have bad imports"
+  return Job.pure col.mods
 where
-  go root mods modSet := do
-    let mut mods := mods
-    let mut modSet := modSet
-    unless modSet.contains root do
-      modSet := modSet.insert root
-      let imps ← (← root.imports.fetch).await
+  go root col := do
+    let mut col := col
+    unless col.modSet.contains root do
+      col := {col with modSet := col.modSet.insert root}
+      -- We discard errors here as they will be reported later when the module is built.
+      let some imps ← (← root.imports.fetch).wait?
+        | return {col with hasErrors := true}
       for mod in imps do
         if mod.lib.name = self.name then
-          (mods, modSet) ← go mod mods modSet
-      mods := mods.push root
-    return (mods, modSet)
+          col ← go mod col
+      col := {col with mods := col.mods.push root}
+    return col
 
 /-- The `LibraryFacetConfig` for the builtin `modulesFacet`. -/
 private def LeanLib.modulesFacetConfig : LibraryFacetConfig modulesFacet :=

src/lakefile.toml.in

@@ -76,7 +76,7 @@ globs = ["Lake.*"]
 defaultFacets = ["static", "static.export"]
 # Load the previous stage's lake native code into lake's build process in order to prevent ABI
 # breakages from affecting bootstrapping.
-moreLeanArgs = ["--plugin", "${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
+weakLeanArgs = ["--plugin", "${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
 
 [[lean_lib]]
 name = "LakeMain"