Split UntypedSyntax out of Inference
Type inference: refactor/fix substitution on TVar

The current substitution would duplicate the handling for type variables
and not recurse into other types, which is bad.

In the context of type inference, triggering this bug is
impossible (because variable are typed by collectConstraints(UAbs) with
either type variables or type annotations, which do not contain type
variables since in practice never use them in client programs. But this
seems fragile, so let's fix it anyway.
Change prefix for vars generated by A-normalization
Move dangerous implicit conv. out of Inference

You don't want an implicit conversion in scope inside its own
implementation. In particular, a conversion from UntypedTerm to
TypedTerm is bad while you're writing a (recursive) function with that
type, since you might inadvertently call it on a subterm (which happened
to me).
Inference: cleanup overloads of substitute

* Ensure all "overloads" have the same argument order.
* Avoid actual overloading for coherence. We can't overload these
  methods if we curry them on the second argument, overloading is
  arguably "evil" anyway, so let's just avoid it.
* Inline a trivial overload (on Set[Constraint]) used only once and
  trivial to define with map.
Support Let in untyped language&type inference
ANormalFormTest.sc: misc updates

This does not yet switch yet to using the let-based desugaring of
let(...).
ANormalFormTest.sc: Switch to Let-based desugaring

This way, calls to let produce ULet nodes rather than their desugaring;
let nodes are preserved by type inference (by converting them down to
Let nodes).