Changed the inferencer a bit.

Made it so that let (and match and letrec) bind fresh unification
variables in the environment and then unify those variables with the
types that should be there.  This saves us having to do some careful
reasoning about what can be in the types that the inferencer returns to
meet the invariants on the environment.  The non-polymorphic let case
goes through, so now I think it's just a matter of a day or two to grind
the rest of the cases of the proof out, now that we're not trying to do
polymorphic nested let expressions.