Check @notUndefined of an interface against the implementation
Why
Interface inclusion ignored @notUndefined. An interface could declare @notUndefined type t over type t = option<int>, and clients then unboxed option<t>, so Some(M.none) was None (#8964).
When the second declaration of an inclusion is @notUndefined, the first must be a type that cannot hold undefined, by the rule option unboxing uses, or an abstract type, which has no representation to contradict it. This covers .resi files, functor arguments and with type constraints. The check runs in Includemod, since Typeopt depends on Includecore through Typedecl.
addedDiagnostic
// Hidden.resi@notUndefined type t// Hidden.restype t = option<int>
diagnostic
Type declarations do not match: type t = option<int>is not included in type tTheir runtime representations differ:the second declaration is @notUndefined,but the first declaration can hold undefined.
Review
- Why accept an abstract implementation without the attribute? The stdlib's
Lazy.resdeclarestype t<+'a>under@notUndefinedin its interface, and so may bindings; such a type has no representation that could holdundefined, so requiring the attribute twice would only break them.