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



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

Reply via email to