Many thanks Matthew for the clarification. Subtle :-)

## Advertising

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

_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml