On Sat, Jul 21, 2012 at 10:34 AM, Phil Clayton phil.clayton@lineone.net wrote:
That's immensely useful. I was miles away from value restriction. There shouldn't be any value restriction issue here - there isn't polymorphism where you may think there is. As you point out, entering at the top level gives
val x = 2: (_a, int) t
and a warning about inventing type _a. However, inside structure B, type inference should, given the signature constraint, constrain x to have type
('a t, int) t
which is just
(unit, int) t
So, no polymorphic type and no value restriction issue. In fact, if we add a type annotation in structure B to make this constraint explicit
structure B :> B = struct type 'a t = unit val x = A.mkT 2 : (unit, int) t end
then test-1.sml and test-2.sml are accepted by both Poly/ML and SML/NJ! So I think Poly/ML and SML/NJ may have a type inference issue there.
Also, I note that using 'a t rather than unit in the type annotation as follows:
val x = A.mkT 2 : ('a t, int) tdoes not help either Poly/ML or SML/NJ, which may give some clue as to where the issue is.
I am assuming that such type annotations shouldn't be necessary for a program to type check but perhaps I am wrong to do so.
I believe that both programs are valid SML programs. Both are accepted by HaMLet (http://www.mpi-sws.org/~rossberg/hamlet/), which is usually my goto for "who's right?" questions.
The value restriction does come into play, in that the result of "A.mkT 2" cannot be generalized and must have a monotype. But, if an implementation infers the correct monotype for "A.mkT 2" (namely, "(unit, int) A.t"), then the result can be given the type scheme "('a t, int) A.t" due to the equivalence of "'a t" and "unit".
I was going to point out the same solution that Phil notes: that adding an explicit type ascription that sets the type of the "A.mkT 2" expression to "(unit, int) A.t" allows the program to be accepted by SML/NJ and Poly/ML.