Got rid of refreshType; it's not needed

Our old strategy was, when checking subsumption T <= U:

  1) refresh U ~> U'
  2) skolemize T ~> T'
  3) unify U' with T'
  4) check for the skolems we just made in T and U

However, if any skolems were to appear in U after this process, it would be
due to U containing non-refreshable variables. Any refreshable variables in
U would be replaced when creating U', and unification with those variables
wouldn't show up in U (unless they were unified with other, non-refreshable
variables in U).

But, any non-refreshable variables in U have a depth less than the current
depth (that is what makes them non-refreshable). So, if a skolem would
appear in U, its depth would have to be set to less-than-current as a part
of the unification process. We run this check anyway.

Further, the type we actually use as the result of a subsumption check is T,
as it is the ascribed type, more or less. So we cannot be passing out any
skolems into a synthesized type via U. Checking U was purely for
environmental purposes, which is now handled by the depth check. So it is
sufficient to check T for skolems, and verify the depths of the recently
created skolems.