summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2015-12-31 12:49:40 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2015-12-31 12:49:40 -0500
commit3d24185389cef552d4b442d16d0c5ed1d8ccaf87 (patch)
tree2a23cd48c15e038d520ee023d7d582ceac3decfb
parent0ef442f42279b3637e91fff45c45048cd1b594a1 (diff)
Some bugs related to kind-checking tuples
-rw-r--r--src/elaborate.sml41
1 files changed, 22 insertions, 19 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 25cce6bd..3b7c48ea 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -163,22 +163,25 @@
r := L'.KKnown k1All)
handle Subscript => err KIncompatible)
| (L'.KTupleUnif (loc, nks1, r1 as ref (L'.KUnknown f1)), L'.KTupleUnif (_, nks2, r2 as ref (L'.KUnknown f2))) =>
- let
- val nks = foldl (fn (p as (n, k1), nks) =>
- case ListUtil.search (fn (n', k2) =>
- if n' = n then
- SOME k2
- else
- NONE) nks2 of
- NONE => p :: nks
- | SOME k2 => (unifyKinds' env k1 k2;
- nks)) nks2 nks1
+ if r1 = r2 then
+ ()
+ else
+ let
+ val nks = foldl (fn (p as (n, k1), nks) =>
+ case ListUtil.search (fn (n', k2) =>
+ if n' = n then
+ SOME k2
+ else
+ NONE) nks2 of
+ NONE => p :: nks
+ | SOME k2 => (unifyKinds' env k1 k2;
+ nks)) nks2 nks1
- val k = (L'.KTupleUnif (loc, nks, ref (L'.KUnknown (fn x => f1 x andalso f2 x))), loc)
- in
- r1 := L'.KKnown k;
- r2 := L'.KKnown k
- end
+ val k = (L'.KTupleUnif (loc, nks, ref (L'.KUnknown (fn x => f1 x andalso f2 x))), loc)
+ in
+ r1 := L'.KKnown k;
+ r2 := L'.KKnown k
+ end
| _ => err KIncompatible
end
@@ -641,10 +644,10 @@
| (L'.KUnif (_, _, r), _) =>
let
val ku = kunif env loc
- val k = (L'.KTupleUnif (loc, [(n, ku)], r), loc)
+ val k = (L'.KTupleUnif (loc, [(n, ku)], ref (L'.KUnknown (fn _ => true))), loc)
in
r := L'.KKnown k;
- k
+ ku
end
| (L'.KTupleUnif (_, nks, r), _) =>
(case ListUtil.search (fn (n', k) => if n' = n then SOME k else NONE) nks of
@@ -652,10 +655,10 @@
| NONE =>
let
val ku = kunif env loc
- val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), r), loc)
+ val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), ref (L'.KUnknown (fn _ => true))), loc)
in
r := L'.KKnown k;
- k
+ ku
end)
| k => raise CUnify' (env, CKindof (k, c, "tuple")))