summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml62
1 files changed, 34 insertions, 28 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 2cc01eda..37ca4b25 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -207,7 +207,7 @@
"U" ^ Int.toString (n - 26)
in
count := n + 1;
- (L'.CUnif (loc, k, s, ref NONE), loc)
+ (L'.CUnif (0, loc, k, s, ref NONE), loc)
end
end
@@ -495,7 +495,7 @@
| _ => false
fun cunifsRemain c =
case c of
- L'.CUnif (loc, _, _, ref NONE) => SOME loc
+ L'.CUnif (_, loc, _, _, ref NONE) => SOME loc
| _ => NONE
val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
@@ -516,13 +516,11 @@
fun occursCon r =
U.Con.exists {kind = fn _ => false,
- con = fn L'.CUnif (_, _, _, r') => r = r'
+ con = fn L'.CUnif (_, _, _, _, r') => r = r'
| _ => false}
exception CUnify' of cunify_error
- exception SynUnif = E.SynUnif
-
type record_summary = {
fields : (L'.con * L'.con) list,
unifs : (L'.con * L'.con option ref) list,
@@ -588,7 +586,7 @@
| k => raise CUnify' (CKindof (k, c, "tuple")))
| L'.CError => kerror
- | L'.CUnif (_, k, _, _) => k
+ | L'.CUnif (_, _, k, _, _) => k
| L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc)
| L'.CKApp (c, k) =>
@@ -644,7 +642,7 @@
| k => raise CUnify' (CKindof (k, c, "tuple")))*)
| L'.CError => false
- | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit
+ | L'.CUnif (_, _, k, _, _) => #1 k = L'.KUnit
| L'.CKAbs _ => false
| L'.CKApp _ => false
@@ -701,8 +699,8 @@
unifs = #unifs s1 @ #unifs s2,
others = #others s1 @ #others s2}
end
- | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c
- | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
+ | (L'.CUnif (nl, _, _, _, ref (SOME c)), _) => recordSummary env (E.mliftConInCon nl c)
+ | c' as (L'.CUnif (0, _, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
| c' => {fields = [], unifs = [], others = [c']}
in
sum
@@ -735,8 +733,8 @@
and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =
let
(*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)),
- ("#1", p_summary env s1),
- ("#2", p_summary env s2)]*)
+ ("#1", p_summary env s1),
+ ("#2", p_summary env s2)]*)
fun eatMatching p (ls1, ls2) =
let
@@ -922,7 +920,7 @@
unfold (r2, c2');
unifyCons env loc r (L'.CConcat (r1, r2), loc)
end
- | L'.CUnif (_, _, _, ur) =>
+ | L'.CUnif (0, _, _, _, ur) =>
ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc)
| _ => raise ex
in
@@ -970,7 +968,7 @@
onFail ()
in
case #1 (hnormCon env c2) of
- L'.CUnif (_, k, _, r) =>
+ L'.CUnif (0, _, k, _, r) =>
(case #1 (hnormKind k) of
L'.KTuple ks =>
let
@@ -986,7 +984,7 @@
| _ => onFail ()
in
case #1 (hnormCon env c1) of
- L'.CUnif (_, k, _, r) =>
+ L'.CUnif (0, _, k, _, r) =>
(case #1 (hnormKind k) of
L'.KTuple ks =>
let
@@ -1002,7 +1000,7 @@
fun projSpecial2 (c2, n2, onFail) =
case #1 (hnormCon env c2) of
- L'.CUnif (_, k, _, r) =>
+ L'.CUnif (0, _, k, _, r) =>
(case #1 (hnormKind k) of
L'.KTuple ks =>
let
@@ -1035,19 +1033,24 @@
| (L'.CConcat _, _) => isRecord ()
| (_, L'.CConcat _) => isRecord ()
- | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
- if r1 = r2 then
+ | (L'.CUnif (nl1, loc1, k1, _, r1), L'.CUnif (nl2, loc2, k2, _, r2)) =>
+ if r1 = r2 andalso nl1 = nl2 then
()
- else
+ else if nl1 = 0 then
(unifyKinds env k1 k2;
r1 := SOME c2All)
+ else if nl2 = 0 then
+ (unifyKinds env k1 k2;
+ r2 := SOME c2All)
+ else
+ err (fn _ => TooLifty (loc1, loc2))
- | (L'.CUnif (_, _, _, r), _) =>
+ | (L'.CUnif (0, _, _, _, r), _) =>
if occursCon r c2All then
err COccursCheckFailed
else
r := SOME c2All
- | (_, L'.CUnif (_, _, _, r)) =>
+ | (_, L'.CUnif (0, _, _, _, r)) =>
if occursCon r c1All then
err COccursCheckFailed
else
@@ -1167,6 +1170,11 @@
| _ => false)
| _ => false
+ fun subConInCon env x y =
+ ElabOps.subConInCon x y
+ handle SubUnif => (cunifyError env (TooUnify (#2 x, y));
+ cerror)
+
fun elabHead (env, denv) infer (e as (_, loc)) t =
let
fun unravelKind (t, e) =
@@ -1195,7 +1203,7 @@
let
val u = cunif (loc, k)
- val t'' = subConInCon (0, u) t'
+ val t'' = subConInCon env (0, u) t'
in
unravel (t'', (L'.ECApp (e, u), loc))
end
@@ -1282,7 +1290,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
val k = (L'.KType, loc)
val unifs = map (fn _ => cunif (loc, k)) xs
val nxs = length unifs - 1
- val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs
+ val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i, u) t) t unifs
val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
in
ignore (checkPatCon env p' pt t);
@@ -1469,7 +1477,7 @@ fun exhaustive (env, t, ps, loc) =
val (t1, args) = unapp (hnormCon env q1, [])
val t1 = hnormCon env t1
- fun doSub t = foldl (fn (arg, t) => subConInCon (0, arg) t) t args
+ fun doSub t = foldl (fn (arg, t) => subConInCon env (0, arg) t) t args
fun dtype (dtO, names) =
let
@@ -1653,7 +1661,7 @@ fun normClassConstraint env (c, loc) =
(L'.TFun (c1, c2), loc)
end
| L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc)
- | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c
+ | L'.CUnif (nl, _, _, _, ref (SOME c)) => normClassConstraint env (E.mliftConInCon nl c)
| _ => unmodCon env (c, loc)
fun findHead e e' =
@@ -1863,9 +1871,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
| L'.TCFun (_, x, k, eb) =>
let
val () = checkKind env c' ck k
- val eb' = subConInCon (0, c') eb
- handle SynUnif => (expError env (Unif ("substitution", loc, eb));
- cerror)
+ val eb' = subConInCon env (0, c') eb
val ef = (L'.ECApp (e', c'), loc)
val (ef, eb', gs3) =
@@ -3303,7 +3309,7 @@ and wildifyStr env (str, sgn) =
(SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc)
| _ => NONE)
| L'.CUnit => SOME (L.CUnit, loc)
- | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c
+ | L'.CUnif (nl, _, _, _, ref (SOME c)) => decompileCon env (E.mliftConInCon nl c)
| _ => NONE
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-24 22:28:59 +0000