Modify the declarative type system to make the inferencer complete.

Enforce a restriction on declarations that are not syntactic values (and
so can't be generalised). If there are two different types that it could
have, then it has no type. All the metatheory goes through unchanged,
except for weakening, where there is stil 1 tricky cheat dealing with
weakened module environments possibly adding extra types.
More tinkering inference completeness.
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).
Work toward the new type system check for completeness.

There's now a cheat in the soundness proof, since there's an extra
condition that the type system requires.
Separate out expression level inference sound/complete

Each of definition level soundness and completeness will now require
both expression level soundness and completeness, because with the new
type type check for non-value definitions, type_d has type_e in both
positive and negative positions.
Merge remote-tracking branch 'origin/master' into complete_type_system
More work on the new type system restriction.

infer_eSound and infer_eComplete bothe defined (different) tenv_inv
relations, which was very confusing when both were in use in the same
goal in inferSound. Rename infer_eComplete one to tenv_invC
Attempt to characterise type_e determism in terms on infer_e free variables
Progress on restoring inference soundness proof
Change the determinism check in the type system

For definition val p = e; previously I was checking that there could
only be 1 type for e, but in fact the proper check to line up with what
the inference system does is that there is only 1 possible environment
from p (after ensuring that p and e have the same type).

Check that the type environment of the definition
More some theorems around
More progress on restoring inference soundness
More infer soundness
More work on fixing the inferencer soundness proof.

It much more tricky than I thought it would be.
Some good progress on inferencer soundness and completeness.
A little more inferencer completeness proof sketching
prove cheat in infer_pe_complete

with copious help from Yong Kiam
Merge remote-tracking branch 'origin/master' into complete_type_system