More helpful type errors

[uncomputable]

Often unification fails on the last stretch, being almost finished. This leads to unhelpful error messages like "A = B but it should be A = B". I am not sure if this is a race condition, but I have seen a lot of these errors. Also, type errors could be more helpful in general.

[apoelstra]

I think the right approach here is to work on the "human-readable language", to output the full program with the current state of inferred types, and the error line highlighted somehow.

Trying to output isolated error messages that somehow capture a type inference error is hopeless because of how incredibly non-local type inference is.

[uncomputable]

We should experiment to see if the way we use unification arrows results in weird error messages.

[uncomputable]

Type variables get names of the form disconnect_b_10 where disconnect is the combinator type, b is the type variable of disconnect (from the tech report) and 10 is an index. The index is different for each variable, so it can be that the same disconnect has variables disconnect_b_10 and disconnect_c_42. We should try to give all variables of the same combinator the same index. Ideally, the nodes in question are shown with their index when there is an error.

Many types are also copied from existing arrows. We could use this to construct a provenance graph that captures where the type bound originally comes from. This can help users understand why a type became what it is.