feat: additional fieldinfo in structure instance notation (#13728)

This PR improves hovers and completions for compound field names in
structure instance notation. Previously a field like `x.fst` would only
have information associated to `x` attached to the entire syntax, but
now `x` and `fst` are treated separately.

Additionally, the `trace.Elab.struct` trace class is now
`trace.Elab.structInst`, and the messages have been cleaned up and
reorganized. Furthermore, `ExceptToTraceResult` has an `Expr` instance
that shows a failure emoji when there are synthetic sorries. Lastly,
`Syntax.identComponents` has an early return for names with at most one
component, saving a re-parsing step.