diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2015-12-31 12:49:40 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2015-12-31 12:49:40 -0500 |
| commit | 3d24185389cef552d4b442d16d0c5ed1d8ccaf87 (patch) | |
| tree | 2a23cd48c15e038d520ee023d7d582ceac3decfb | |
| parent | 0ef442f42279b3637e91fff45c45048cd1b594a1 (diff) | |
Some bugs related to kind-checking tuples
| -rw-r--r-- | src/elaborate.sml | 41 |
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"))) |