Change of approach for dealing with value restriction + inference completeness

The weakening theorems needed to prove type soundness aren't true if you
check for multiple possible types on a non-value definition. For
example, in the following v has type int -> int

structure M :> sig val f : int -> int end =
struct
  fun f x = x
end;
val v = (fn y => y) M.f;

However, if you drop the signature (which is something has to happen in
the type soundness proof), then you get M.f : 'a -> 'a and since the
value restriction prevents v : 'a -> 'a, there are many choices for v :
int -> int, v : bool -> bool, etc.

So now I've added a flag to type_d (and type_ds, etc) to indicate
whether to do the check. So the semantics can do the check, and the
inferencer can be complete with respect to that, but the type soundness
proof can turn off the check (since if something types with the check on
it will still type with it off).