[MLton-commit] r6229

[Matthew Fluet]

Fixed bug in type inference of flexible records.  This would later
cause the compiler to raise the TypeError exception when type checking
the XML program after the defunctorize pass.

The following program exhibits the bug:

fun f (a, b) = (#value a) < (#value b)

fun g (array1 (* : {value:nat, offset:'a1} array *), 
       array2 (* : {value:nat, offset:'a2} array *),
       record1 : {value:nat, offset:'b},
       record2 : {value:nat, offset:'c}) =
   let
      val left (* : {value:nat, ...} *) = Array.sub (array1, 0)
      val right (* : {value:nat, ...} *) = Array.sub (array1, 1)
      val small (* : {value:nat, ...} *) = 
         if f (left, right)
           then Array.sub (array2, 0)
           else Array.sub (array2, 1)
   in
      (f (record1, small),
       f (small, record2))
   end

After elaborating "fun f (a, b) = ...", f is assigned the type scheme:
  {value:int, gen1:...} * {value:int, gen2:...} -> bool
where gen1 and gen2 denote (distinct) generalizable flex records, each
with their own spine.

After elaborating "val left = ..." and "val right = ...", left and
right are assigned (the same) unification variable, which is otherwise
unconstrained.

In elaborating "f (left, right)", we instantiate the type scheme of f,
realizing the two generalizable flex records as flex records.  We then
unify the flex records with left and with right.  Since left and right
have the same unification variable, this effectively unifies the two
flex records, which unifies the two spines.  This is correct, as we
now know that the spines of the two record arguments to f must be the
same.  However, the generalizable fields may be generalized to
different types in the two arguments.  But, Spine.unify causes the two
spines for the record arguments to be equal according to Spine.equals.
This causes problems for computing the type arguments to an
application of f, because we use Spine.equals to find the flexible
record type that was derived from the generalizeable flex record at
scheme instantiation.  Nothing goes wrong with "f (left, right)",
because left and right have the same type, so the instantiation of the
offset field type will be the same.  However, with "f (record1,
small)" the instantiations of the offset field type will be different
('b for record1, and 'a2 for small).  The spine unification caused the
lookup of the type argument from the generalizable fields of the first
record to see the types of the second record, leading to the XML type
error:
  Type error: actual and formal not of same type
  actual: ('a_4092 * word32) * (word32 * word32)
  formal: (word32 * word32) * (word32 * word32)

The fix was to give Spine.t's an identity separate from the
DisjointSet.t used to ensure that spines had the same sets of fields.
The spine identity is now used for Spine.equals in the lookup.


----------------------------------------------------------------------

U   mlton/trunk/doc/changelog
U   mlton/trunk/mlton/elaborate/type-env.fun

----------------------------------------------------------------------

Modified: mlton/trunk/doc/changelog
===================================================================
--- mlton/trunk/doc/changelog	2007-11-29 15:30:10 UTC (rev 6228)
+++ mlton/trunk/doc/changelog	2007-11-29 20:08:19 UTC (rev 6229)
@@ -1,5 +1,10 @@
 Here are the changes from version 20070826 to version YYYYMMDD.
 
+* 2007-11-29
+   - Fixed bug in type inference of flexible records.  This would
+     later cause the compiler to raise the TypeError exception.
+     Thanks to Wesley Terpstra for the bug report.
+
 * 2007-11-28
    - Fixed bug in cross-compilation of gdtoa library.  Thanks to
      Wesley Terpstra for the bug report and patch.

Modified: mlton/trunk/mlton/elaborate/type-env.fun
===================================================================
--- mlton/trunk/mlton/elaborate/type-env.fun	2007-11-29 15:30:10 UTC (rev 6228)
+++ mlton/trunk/mlton/elaborate/type-env.fun	2007-11-29 20:08:19 UTC (rev 6229)
@@ -316,15 +316,23 @@
       val unify: t * t -> unit
    end =
    struct
-      datatype t = T of {fields: Field.t list ref,
-                         more: bool ref} Set.t
+      datatype t = T of {id: int,
+                         body: {fields: Field.t list ref,
+                                more: bool ref} Set.t}
 
-      fun new fields = T (Set.singleton {fields = ref fields,
-                                         more = ref true})
+      local
+         val r: int ref = ref 0
+      in
+         fun newId () = (Int.inc r; !r)
+      end
+      
+      fun new fields = T {id = newId (),
+                          body = Set.singleton {fields = ref fields,
+                                                more = ref true}}
 
-      fun equals (T s, T s') = Set.equals (s, s')
+      fun equals (T {id = id1,...}, T {id = id2,...}) = id1 = id2
 
-      fun layout (T s) =
+      fun layout (T {body = s,...}) =
          let
             val {fields, more} = Set.! s
          in
@@ -332,23 +340,25 @@
                            ("more", Bool.layout (!more))]
          end
 
-      fun canAddFields (T s) = ! (#more (Set.! s))
-      fun fields (T s) = ! (#fields (Set.! s))
+      fun canAddFields (T {body = s,...}) = ! (#more (Set.! s))
+      fun fields (T {body = s,...}) = ! (#fields (Set.! s))
 
       fun ensureFieldValue ({fields, more}, f) =
          List.contains (!fields, f, Field.equals)
          orelse (!more andalso (List.push (fields, f); true))
 
-      fun ensureField (T s, f) = ensureFieldValue (Set.! s, f)
+      fun ensureField (T {body = s,...}, f) = ensureFieldValue (Set.! s, f)
 
-      fun noMoreFields (T s) = #more (Set.! s) := false
+      fun noMoreFields (T {body = s,...}) = #more (Set.! s) := false
 
-      fun unify (T s, T s') =
+      fun unify (T {body = s1,...}, T {body = s2,...}) =
          let
-            val {fields = fs, more = m} = Set.! s
-            val {more = m', ...} = Set.! s'
-            val _ = Set.union (s, s')
-            val _ = Set.:= (s, {fields = fs, more = ref (!m andalso !m')})
+            val {fields = fs1, more = m1} = Set.! s1
+            val {fields = fs2, more = m2} = Set.! s2
+            val _ = Set.union (s1, s2)
+            val fs = List.union (!fs1, !fs2, Field.equals)
+            val m = !m1 andalso !m2
+            val _ = Set.:= (s1, {fields = ref fs, more = ref m})
          in
             ()
          end