This PR makes the `deriving Inhabited` handler for `structure`s be able
to inherit `Inhabited` instances from structure parents, using the same
mechanism as for class parents. This fixes a regression introduced by
#9815, which lost the ability to apply `Inhabited` instances for parents
represented as subobject fields. With this PR, now it works for all
parents in the hierarchy.
Implementation detail: adds `struct_inst_default%` for synthesizing a
structure default value using `Inhabited` instances for parents and
fields.
Closes#13372
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
