`deriving Inhabited` ignores field defaults

[Kha]

structure Config where
  iota := true
deriving Inhabited

#eval (default : Config).iota  -- false

I am very surprised this has not led to more bugs in our codebase.

[kmill]

#9815 is a quick hack that should work in most cases.

Default field value elaboration is complicated enough that it uses by refine' {.. : S} <;> exact default to construct the default term.

There are a number of ways to improve on this, but they would take much more work to carry out.

There's a related issue I didn't address, where opt-params in inductive constructor fields aren't respected. Opt-params already don't work in recursive or nested inductives. Plus, I don't believe they're used that often.