[MLton] where and nj-deviations

[Matthew Fluet]

I'm adding another nj-deviation, which is essentially a variation on the
where structure specification.  To review, the MLton User Guide currently
says the following:  (for convenience, I'm labeling the examples in
comments)

****

SML/NJ allows a where structure specification that is similar to a where
type specification. For example:

(* A *)
structure S = struct type t = int end
signature SIG =
  sig
     structure T : sig type t end
  end where T = S

This is equivalent to:

(* B *)
structure S = struct type t = int end
signature SIG =
  sig
     structure T : sig type t end
  end where type T.t = S.t

****

I want to add the following:

****

SML/NJ also allows a definitional structure specification that is similar
to a definitional type specification.  For example:

(* C *)
structure S = struct type t = int end
signature SIG =
  sig
     structure T : sig type t end = S
  end

This is equivalent to the previous examples and to:

(* D *)
structure S = struct type t = int end
signature SIG =
  sig
     structure T : sig type t end where type t = S.t
  end

****

Now, the issue is that all of these examples may not be equivalent.
For example, SML/NJ rejects

(* E *)
structure S = struct type t = int end
signature SIG =
  sig
     structure T : sig type t end = S
  end
  where type T.t = S.t

with: "where type defn applied to definitional spec"

SML/NJ also rejects

(* F *)
structure S = struct type t = int end
signature SIG =
  sig
    structure T : sig type t end where type t = S.t
  end
  where type T.t = S.t

with: "where type defn applied to definitional spec"

On the other hand, MLton accepts (* F *).  But, I'm fairly certain that
that is a bug, because MLton also accepts:

(* G *)
structure S = struct type t = int end
signature SIG =
  sig
    structure T : sig type t end where type t = S.t
  end
  where type T.t = bool

which clearly sends conflicting messages about the type of T.t.

However, SML/NJ accepts

(* H *)
structure S = struct type t = int end
signature SIG =
  sig
    structure T : sig type t end where type t = S.t
  end
  where T = S

which is arguably equivalent to (* F *) when one expands "where T = S"
by the equivalence of (* A *).  But, SML/NJ rejects (* F *) and accepts
(* H *).  There may also be a bug in SML/NJ, because it accepts

(* I *)
structure R = struct type t = bool end
structure S = struct type t = int end
signature SIG =
  sig
    structure T : sig type t end where type t = S.t
  end
  where T = R

which, like (* G *) seems to be claiming conflicting things about the type
of T.t.


In any case, I'm not sure whether SML/NJ's definitional structure
specifications can really be replicated with where and/or where type
constraints.  (The analogy would seem to be that one cannot always replace
a definitional type specification with a where type constraint.)  The
problem would seem that the "real" equivalent of (* C *) is

(* J *)
structure S = struct type t = int end
signature SIG =
  sig
    structure T : sig type t = S.t end
  end

The "problem" with that is that if instead of (* C *) we started with:

(* K *)
signature T = sig type t end
structure S = struct type t = int end
signature SIG =
  sig
    structure T : T = S
  end

then we still need to expand to (* J *), which requires replicating the T
signature in order to push the definitional specification to the type.