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.