# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1406923896 14400
# Node ID 459ccbf8cd08e7eb9c4e7ac1d51a7392b1833d2e
# Parent  4d64af730e353bed2ee9da3427ee4c66887deb69
When unifying constructor-level unification variables, also unify their kinds

diff -r 4d64af730e35 -r 459ccbf8cd08 src/elaborate.sml
--- a/src/elaborate.sml	Fri Aug 01 15:44:17 2014 -0400
+++ b/src/elaborate.sml	Fri Aug 01 16:11:36 2014 -0400
@@ -1226,26 +1226,29 @@
              else
                  err (fn _ => TooLifty (loc1, loc2))
 
-           | (L'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) =>
-             if occursCon r c2All then
-                 maybeIsRecord c2
-             else if f c2All then
-                 r := L'.Known c2All
-             else
-                 err CScope
-           | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) =>
-             if occursCon r c1All then
-                 maybeIsRecord c1
-             else if f c1All then
-                 r := L'.Known c1All
-             else
-                 err CScope
-
-           | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) =>
+           | (L'.CUnif (0, _, k1, _, r as ref (L'.Unknown f)), _) =>
+             (unifyKinds env k1 (kindof env c2All);
+              if occursCon r c2All then
+                  maybeIsRecord c2
+              else if f c2All then
+                  r := L'.Known c2All
+              else
+                  err CScope)
+           | (_, L'.CUnif (0, _, k2, _, r as ref (L'.Unknown f))) =>
+             (unifyKinds env (kindof env c1All) k2;
+              if occursCon r c1All then
+                  maybeIsRecord c1
+              else if f c1All then
+                  r := L'.Known c1All
+              else
+                  err CScope)
+
+           | (L'.CUnif (nl, _, k1, _, r as ref (L'.Unknown f)), _) =>
              if occursCon r c2All then
                  maybeIsRecord c2
              else
-                 (let
+                 (unifyKinds env k1 (kindof env c2All);
+                  let
                       val sq = squish nl c2All
                   in
                       if f sq then
@@ -1254,11 +1257,12 @@
                           err CScope
                   end
                   handle CantSquish => err (fn _ => TooDeep))
-           | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) =>
+           | (_, L'.CUnif (nl, _, k2, _, r as ref (L'.Unknown f))) =>
              if occursCon r c1All then
                  maybeIsRecord c1
              else
-                 (let
+                 (unifyKinds env (kindof env c1All) k2;
+                  let
                       val sq = squish nl c1All
                   in
                       if f sq then
diff -r 4d64af730e35 -r 459ccbf8cd08 tests/wackyunif.ur
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/wackyunif.ur	Fri Aug 01 16:11:36 2014 -0400
@@ -0,0 +1,2 @@
+val concatX [ctx] [use] : _ -> _ ctx use _ =
+    List.foldl join <xml/>
diff -r 4d64af730e35 -r 459ccbf8cd08 tests/wackyunif.urp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/wackyunif.urp	Fri Aug 01 16:11:36 2014 -0400
@@ -0,0 +1,2 @@
+$/list
+wackyunif