[MLton] Phantom typing of sockets broken in MLton

[Matthew Fluet]

On Tue, 14 Oct 2008, Vesa Karvonen wrote:
> Just a quick note before going to bed.  Phantom typing of sockets
> seems broken in MLton.  Here is a small example that should not pass
> type checking (but does in MLton):
>
> val socket = INetSock.TCP.socket ()
> val () = Socket.listen (socket, 1)
> val _ = Socket.recvVec (socket, 1)
>
> Both SML/NJ and Poly/ML reject this example.

I think the issue is that basis-library/net/socket.{sig,sml} has

   structure Socket : SOCKET_EXTRA = ...

and basis-library/libs/basis-extra/basis.{sig,sml} has

   signature BASIS_EXTRA =
     sig
       ...
     end
     ...
     where type ('a, 'b) Socket.sock = ('a, 'b) Socket.sock
     ...
   structure BasisExtra :> BASIS_EXTRA

The non-opaque signature constraint on Socket allows the phantomness of 
the type-arguments to ('a, 'b) Socket.sock to leak out as a transparent 
type, and the where type... propagates the transparent type out to user 
code.

Using Socket :> SOCKET_EXTRA leads to lots of type errors in the Basis 
Library; Deleting where type ('a, 'b) Socket.sock = ('a, 'b) Socket.sock 
doesn't lead to type errors in the Basis Library itself, but does lose the 
type equivalence between the visible Socket.sock and the Socket.sock type 
mentioned in INetSock and UnixSock.