feat: report better types in API for embeddings

[brprice]

For embeddings, (i.e. where we have both a checked-at and synthesised type), we must (with the current API design) choose one type to report as the type of the selection. Previously we chose the synthed, but we now:

• if exactly one is a hole, then choose the other
• otherwise, chose the synthed (As future work, we may want to change the api to report both types, or maybe "merge" the two types. However, it is not clear what the correct design is here. (Note that "merging" is somewhat awkward due to binders and needing to worry about alpha equivalence).)

Note that these two types must be consistent. Consider the situation where we are checking T ∋ e and discover that e ∈ S. If we did not have T ~ S, then this would be a type error, which smartholes would rectify by putting e in a non-empty hole, giving T ∋ {? e ?} ∈ ? and ? ∋ e ∈ S. In this case, we report that {? e ?} has type T and e has type S.

The most obvious place that this change will affect is asking for the type of an expression hole: these synthesise the hole type, but may be in a checkable context. We now report the type the context requires them to have, rather than a hole. However, there are other situations, such as (assuming swap ∈ ∀a b . Pair a b -> Pair b a) swap @Int @? (swap @Char @? ?) where the inner swap is checked at Pair Int ? and synthesises Pair ? Char.