Many thanks Matthew for the clarification. Subtle :-)
Since datatype declarations declare both a type operator and constructors, I think the explanation deserves to appear in http://mlton.org/EqualityTypeVariable, last part. The last two declarations declare identical type operators, but not identical constructors, right ?
Bernard.
On 9/17/16 1:42 PM, Matthew Fluet wrote:
I think that the reasoning is that the type function induced by a datatype (which maps the type variables to the fresh type name) is ignorant of equality type variables, but the type schemes induced by the constructors do respect equality type variables.
Thus, with
datatype ('a, ''b) t = A of 'a | B of ''b
both
fun f (x: (int, real) t) = x
and
val l : ((int, real) t) list = []
type check (with MLton), since "(int, real) t" can always be successfully elaborated.
As noted previously,
val t1 = B 1.0
does not type check, because the type scheme of C cannot be instantiated with "real", a non-equality type.
At first, I was surprised by the following
val t2 : (int, real) t = A 1
which does not type check; in MLton, we report:
Pattern and expression disagree. pattern: (_, [<non-equality>]) t expression: (_, [<equality>]) t in: t2: (int, real) t = A 1
But, this is fine --- the type annotation on the pattern successfully elaborates, but type inference of the expression (constructor A applied to 1) yields "(int, ''B) t" for some fresh unification type variable ''B and this unification type variable is an equality type variable and cannot be unified with "real".
-Matthew