@notUndefined in an interface is not checked against the implementation #8964

An interface can declare an abstract type @notUndefined while its implementation is a type that holds undefined. Interface inclusion does not compare the attribute, so clients unbox option of the type, and Some(None) becomes None.

// M.resi
@notUndefined type t
let none: t

// M.res
type t = option<int>
let none: t = None

// C.res
@inline(never) let id = x => x
let o: option<M.t> = id(Some(M.none))
Console.log2(
  "Some(none) is",
  switch o {
  | Some(_) => "Some"
  | None => "None"
  },
)

Output on master: Some(none) is None. C builds Some(M.none) as M.none itself, which is undefined.

Expected: the implementation is rejected, because type t = option<int> can hold undefined, which the interface rules out. An implementation satisfies @notUndefined when its own type cannot hold undefined: it is @notUndefined itself, a record, a builtin type other than option/unit, or a type declared with @instanceOf/@typeOf (#8950).

The same holds for functor arguments and with type constraints. compiler/ml/UntaggedVariants.md (rule 13, #8952) states that inclusion does not compare @notUndefined.