Use more descriptive English terms in type error messages

[byorgey]

This is a follow-up to #1308.

We should try harder to use more descriptive English terms in error messages, especially where unification variables or skolem variables occur in types. For example, instead of saying "expecting xyz to have type u3 -> u4 but it actually..." we could say something like "expecting xyz to be a function but it actually..." In other words, when printing type error messages, we should do some work to analyze the types involved and see if we can describe them in some way that doesn't involve a bunch of type variables, rather than simply pretty-printing them. At the very least we could replace unification variables with underscores or ellipses, as in "expecting xyz to have a type like (_ -> _) * _, but ..."

So, concretely, I propose the following. In the context of expecting xyz to ...

• If a type has no variables, pretty-print it directly: have type `int -> text`
• If a type consists of a top-level type constructor with variables in it, print it as a phrase: be a function
• If a type is more complex but has variables in it, print it with underscores in place of the variables: have a type like `(_ -> _) * _`