Opaque ascription doesn't generate fresh abstract type

Question

One truly great feature of the ML module system is the interaction between opaque ascription and generative type declarations in signatures:

Poly/ML 5.7.1 Release
> structure O :> OPTION = Option;
structure O: OPTION
> O.NONE = Option.NONE;
poly: : error: Type error in function application.
   Function: = : ''a O.option * ''a O.option -> bool
   Argument: (O.NONE, Option.NONE) : ''a O.option * 'b option
   Reason:
      Can't unify ''a O.option (*Created from opaque signature*) with
         'a option (*In Basis*) (Different type constructors)
Found near O.NONE = Option.NONE
Static Errors

Imagine my surprise and disappointment when I found that, at least in Poly/ML, it doesn't work for lists:

> structure L :> LIST = List;
structure L: LIST
> L.nil = List.nil;
val it = true: bool

Is this behavior allowed by the Definition?

Answer 1

Checking the Mlton and Polyml implementations of the basis library, we see that list is defined outside of the structure/signature and just referenced there. That is not the case for option, which is defined inside the structure/signature.

Using the Polyml implementation as an example, we see that the LIST signature references a list type previously defined in the top level and that the OPTION signature defines the option type locally:

signature LIST =
sig
    datatype list = datatype list
    ...
end

signature OPTION =
sig
    datatype 'a option = NONE | SOME of 'a
    ...
end

Mlton implementation:

https://github.com/MLton/mlton/blob/master/basis-library/list/list.sml

https://github.com/MLton/mlton/blob/master/basis-library/general/option.sml

https://github.com/MLton/mlton/blob/master/basis-library/list/list.sig

https://github.com/MLton/mlton/blob/master/basis-library/general/option.sig

Polyml implementation:

https://github.com/polyml/polyml/blob/master/basis/List.sml

https://github.com/polyml/polyml/blob/master/basis/ListSignature.sml

https://github.com/polyml/polyml/blob/master/basis/Option.sml

For completeness - the sml basis library documentation says the following in the List module:

The list type is considered primitive and is defined in the top-level environment. It is rebound here for consistency.

Such a note isn't present in the documentation for Option, so I assume the above is what they meant.