Use original variable names in error messages about Skolem variables

[byorgey]

Each type variable now carries two variable names: one, the original, user-supplied name of the type variable, and another, the (potentially different) current freshly generated name. These can diverge specifically in the case that we skolemize a user-supplied polymorphic type. We use the second name for all comparisons, but the first name when pretty-printing.

For example, def f : a -> a = \x. 3 end used to generate an error message saying something like "expected 3 to have type s1 ; it now says "expected 3 to have type a".

Closes #2102. That issue also talks about improving the error message that says "skolem variable would escape its scope", but at the moment I can't even find a way to get that error message to be generated at all, so I propose to not worry about it for now.

There is one specific situation where this can be confusing, when one type variable is shadowed by another with the same name. For example:

> def f : a -> (a * Int) = \\x. let g : forall a. a * Int = (x, 3) in g end
1:59: Type mismatch:\n  From context, expected `x` to have type `a`,\n  but it actually has type `a`

Not sure whether it's worth doing anything about this; open to suggestions.

[xsebek]

@byorgey this is great! I remember that any error messages with skolemized type names were hard for me to understand, but this should fix that in most cases. 👍

Regarding the same name, I take it that the type names do not keep the source span like values do?
If they did, the error messages could continue with "a declared at source.sw: line 12 char 42" and similarly for the other a.

[byorgey]

I take it that the type names do not keep the source span like values do?

Yeah, they don't, but they probably should! That would be a bigger change though. Filed as #2343.