summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab.sml16
-rw-r--r--src/elab_env.sml22
-rw-r--r--src/elab_err.sig2
-rw-r--r--src/elab_err.sml11
-rw-r--r--src/elab_ops.sml4
-rw-r--r--src/elab_print.sml6
-rw-r--r--src/elab_util.sig7
-rw-r--r--src/elab_util.sml19
-rw-r--r--src/elaborate.sml398
-rw-r--r--src/explify.sml6
-rw-r--r--tests/capture.ur4
-rw-r--r--tests/rcapture.ur3
12 files changed, 317 insertions, 181 deletions
diff --git a/src/elab.sml b/src/elab.sml
index c042d916..15365951 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -38,12 +38,16 @@ datatype kind' =
| KTuple of kind list
| KError
- | KUnif of ErrorMsg.span * string * kind option ref
- | KTupleUnif of ErrorMsg.span * (int * kind) list * kind option ref
+ | KUnif of ErrorMsg.span * string * kunif ref
+ | KTupleUnif of ErrorMsg.span * (int * kind) list * kunif ref
| KRel of int
| KFun of string * kind
+and kunif =
+ KUnknown of kind -> bool (* Is the kind a valid unification? *)
+ | KKnown of kind
+
withtype kind = kind' located
datatype explicitness =
@@ -78,7 +82,11 @@ datatype con' =
| CProj of con * int
| CError
- | CUnif of int * ErrorMsg.span * kind * string * con option ref
+ | CUnif of int * ErrorMsg.span * kind * string * cunif ref
+
+and cunif =
+ Unknown of con -> bool (* Is the constructor a valid unification? *)
+ | Known of con
withtype con = con' located
diff --git a/src/elab_env.sml b/src/elab_env.sml
index e53c1538..ed96782e 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -484,7 +484,7 @@ fun class_name_in (c, _) =
case c of
CNamed n => SOME (ClNamed n)
| CModProj x => SOME (ClProj x)
- | CUnif (_, _, _, _, ref (SOME c)) => class_name_in c
+ | CUnif (_, _, _, _, ref (Known c)) => class_name_in c
| _ => NONE
fun isClass (env : env) c =
@@ -498,7 +498,7 @@ fun isClass (env : env) c =
fun class_head_in c =
case #1 c of
CApp (f, _) => class_head_in f
- | CUnif (_, _, _, _, ref (SOME c)) => class_head_in c
+ | CUnif (_, _, _, _, ref (Known c)) => class_head_in c
| _ => class_name_in c
exception Unify
@@ -512,16 +512,16 @@ fun unifyKinds (k1, k2) =
| (KUnit, KUnit) => ()
| (KTuple ks1, KTuple ks2) => (ListPair.appEq unifyKinds (ks1, ks2)
handle ListPair.UnequalLengths => raise Unify)
- | (KUnif (_, _, ref (SOME k1)), _) => unifyKinds (k1, k2)
- | (_, KUnif (_, _, ref (SOME k2))) => unifyKinds (k1, k2)
+ | (KUnif (_, _, ref (KKnown k1)), _) => unifyKinds (k1, k2)
+ | (_, KUnif (_, _, ref (KKnown k2))) => unifyKinds (k1, k2)
| (KRel n1, KRel n2) => if n1 = n2 then () else raise Unify
| (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2)
| _ => raise Unify
fun eqCons (c1, c2) =
case (#1 c1, #1 c2) of
- (CUnif (nl, _, _, _, ref (SOME c1)), _) => eqCons (mliftConInCon nl c1, c2)
- | (_, CUnif (nl, _, _, _, ref (SOME c2))) => eqCons (c1, mliftConInCon nl c2)
+ (CUnif (nl, _, _, _, ref (Known c1)), _) => eqCons (mliftConInCon nl c1, c2)
+ | (_, CUnif (nl, _, _, _, ref (Known c2))) => eqCons (c1, mliftConInCon nl c2)
| (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify
@@ -569,8 +569,8 @@ fun unifyCons (hnorm : con -> con) rs =
let
fun unify d (c1, c2) =
case (#1 (hnorm c1), #1 (hnorm c2)) of
- (CUnif (nl, _, _, _, ref (SOME c1)), _) => unify d (mliftConInCon nl c1, c2)
- | (_, CUnif (nl, _, _, _, ref (SOME c2))) => unify d (c1, mliftConInCon nl c2)
+ (CUnif (nl, _, _, _, ref (Known c1)), _) => unify d (mliftConInCon nl c1, c2)
+ | (_, CUnif (nl, _, _, _, ref (Known c2))) => unify d (c1, mliftConInCon nl c2)
| (CUnif _, _) => ()
@@ -663,7 +663,7 @@ fun unifySubst (rs : con list) =
exception Bad of con * con
val hasUnif = U.Con.exists {kind = fn _ => false,
- con = fn CUnif (_, _, _, _, ref NONE) => true
+ con = fn CUnif (_, _, _, _, ref (Unknown _)) => true
| _ => false}
fun startsWithUnif c =
@@ -697,9 +697,9 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) =
fun isRecord () =
let
- val rk = ref NONE
+ val rk = ref (KUnknown (fn _ => true))
val k = (KUnif (loc, "k", rk), loc)
- val r = ref NONE
+ val r = ref (Unknown (fn _ => true))
val rc = (CUnif (0, loc, k, "x", r), loc)
in
((CApp (f, rc), loc),
diff --git a/src/elab_err.sig b/src/elab_err.sig
index a66cf61f..14133d08 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -35,6 +35,7 @@ signature ELAB_ERR = sig
datatype kunify_error =
KOccursCheckFailed of Elab.kind * Elab.kind
| KIncompatible of Elab.kind * Elab.kind
+ | KScope of Elab.kind * Elab.kind
val kunifyError : ElabEnv.env -> kunify_error -> unit
@@ -59,6 +60,7 @@ signature ELAB_ERR = sig
| TooLifty of ErrorMsg.span * ErrorMsg.span
| TooUnify of Elab.con * Elab.con
| TooDeep
+ | CScope of Elab.con * Elab.con
val cunifyError : ElabEnv.env -> cunify_error -> unit
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 84c8c61f..2bf059e6 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -63,6 +63,7 @@ fun kindError env err =
datatype kunify_error =
KOccursCheckFailed of kind * kind
| KIncompatible of kind * kind
+ | KScope of kind * kind
fun kunifyError env err =
case err of
@@ -74,7 +75,10 @@ fun kunifyError env err =
eprefaces "Incompatible kinds"
[("Kind 1", p_kind env k1),
("Kind 2", p_kind env k2)]
-
+ | KScope (k1, k2) =>
+ eprefaces "Scoping prevents kind unification"
+ [("Kind 1", p_kind env k1),
+ ("Kind 2", p_kind env k2)]
fun p_con env c = P.p_con env (simplCon env c)
@@ -122,6 +126,7 @@ datatype cunify_error =
| TooLifty of ErrorMsg.span * ErrorMsg.span
| TooUnify of con * con
| TooDeep
+ | CScope of con * con
fun cunifyError env err =
case err of
@@ -167,6 +172,10 @@ fun cunifyError env err =
eprefaces' [("Replacement", p_con env c1),
("Body", p_con env c2)])
| TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
+ | CScope (c1, c2) =>
+ eprefaces "Scoping prevents constructor unification"
+ [("Have", p_con env c1),
+ ("Need", p_con env c2)]
datatype exp_error =
UnboundExp of ErrorMsg.span * string
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 0af2f4e7..dc9f69a4 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -156,7 +156,7 @@ fun reset () = (identity := 0;
fun hnormCon env (cAll as (c, loc)) =
case c of
- CUnif (nl, _, _, _, ref (SOME c)) => (#1 (hnormCon env (E.mliftConInCon nl c)), loc)
+ CUnif (nl, _, _, _, ref (Known c)) => (#1 (hnormCon env (E.mliftConInCon nl c)), loc)
| CNamed xn =>
(case E.lookupCNamed env xn of
@@ -277,7 +277,7 @@ fun hnormCon env (cAll as (c, loc)) =
let
fun cunif () =
let
- val r = ref NONE
+ val r = ref (Unknown (fn _ => true))
in
(r, (CUnif (0, loc, (KType, loc), "_", r), loc))
end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 2b8dc5f4..d292d7c5 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -54,9 +54,9 @@ fun p_kind' par env (k, _) =
string ")"]
| KError => string "<ERROR>"
- | KUnif (_, _, ref (SOME k)) => p_kind' par env k
+ | KUnif (_, _, ref (KKnown k)) => p_kind' par env k
| KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
- | KTupleUnif (_, _, ref (SOME k)) => p_kind' par env k
+ | KTupleUnif (_, _, ref (KKnown k)) => p_kind' par env k
| KTupleUnif (_, nks, _) => box [string "(",
p_list_sep (box [space, string "*", space])
(fn (n, k) => box [string (Int.toString n ^ ":"),
@@ -202,7 +202,7 @@ fun p_con' par env (c, _) =
string (Int.toString n)]
| CError => string "<ERROR>"
- | CUnif (nl, _, _, _, ref (SOME c)) => p_con' par env (E.mliftConInCon nl c)
+ | CUnif (nl, _, _, _, ref (Known c)) => p_con' par env (E.mliftConInCon nl c)
| CUnif (nl, _, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
p_kind env k,
case nl of
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 2998e7db..8a013554 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -64,6 +64,13 @@ structure Con : sig
val map : {kind : Elab.kind' -> Elab.kind',
con : Elab.con' -> Elab.con'}
-> Elab.con -> Elab.con
+ val appB : {kind : 'context -> Elab.kind' -> unit,
+ con : 'context -> Elab.con' -> unit,
+ bind : 'context * binder -> 'context}
+ -> 'context -> (Elab.con -> unit)
+ val app : {kind : Elab.kind' -> unit,
+ con : Elab.con' -> unit}
+ -> Elab.con -> unit
val existsB : {kind : 'context * Elab.kind' -> bool,
con : 'context * Elab.con' -> bool,
bind : 'context * binder -> 'context}
diff --git a/src/elab_util.sml b/src/elab_util.sml
index bf0185b1..df78616a 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -75,10 +75,10 @@ fun mapfoldB {kind, bind} =
| KError => S.return2 kAll
- | KUnif (_, _, ref (SOME k)) => mfk' ctx k
+ | KUnif (_, _, ref (KKnown k)) => mfk' ctx k
| KUnif _ => S.return2 kAll
- | KTupleUnif (_, _, ref (SOME k)) => mfk' ctx k
+ | KTupleUnif (_, _, ref (KKnown k)) => mfk' ctx k
| KTupleUnif (loc, nks, r) =>
S.map2 (ListUtil.mapfold (fn (n, k) =>
S.map2 (mfk ctx k,
@@ -217,7 +217,7 @@ fun mapfoldB {kind = fk, con = fc, bind} =
(CProj (c', n), loc))
| CError => S.return2 cAll
- | CUnif (nl, _, _, _, ref (SOME c)) => mfc' ctx (!mliftConInCon nl c)
+ | CUnif (nl, _, _, _, ref (Known c)) => mfc' ctx (!mliftConInCon nl c)
| CUnif _ => S.return2 cAll
| CKAbs (x, c) =>
@@ -256,6 +256,19 @@ fun map {kind, con} s =
S.Return () => raise Fail "ElabUtil.Con.map: Impossible"
| S.Continue (s, ()) => s
+fun appB {kind, con, bind} ctx c =
+ case mapfoldB {kind = fn ctx => fn k => fn () => (kind ctx k; S.Continue (k, ())),
+ con = fn ctx => fn c => fn () => (con ctx c; S.Continue (c, ())),
+ bind = bind} ctx c () of
+ S.Continue _ => ()
+ | S.Return _ => raise Fail "ElabUtil.Con.appB: Impossible"
+
+fun app {kind, con} s =
+ case mapfold {kind = fn k => fn () => (kind k; S.Continue (k, ())),
+ con = fn c => fn () => (con c; S.Continue (c, ()))} s () of
+ S.Return () => raise Fail "ElabUtil.Con.app: Impossible"
+ | S.Continue _ => ()
+
fun existsB {kind, con, bind} ctx c =
case mapfoldB {kind = fn ctx => fn k => fn () =>
if kind (ctx, k) then
diff --git a/src/elaborate.sml b/src/elaborate.sml
index a1da9feb..34cb12b8 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -63,6 +63,29 @@
U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
| _ => false)
+ fun validateCon env c =
+ (U.Con.appB {kind = fn env' => fn k => case k of
+ L'.KRel n => ignore (E.lookupKRel env' n)
+ | L'.KUnif (_, _, r as ref (L'.KUnknown f)) =>
+ r := L'.KUnknown (fn k => f k andalso validateKind env' k)
+ | _ => (),
+ con = fn env' => fn c => case c of
+ L'.CRel n => ignore (E.lookupCRel env' n)
+ | L'.CNamed n => ignore (E.lookupCNamed env' n)
+ | L'.CModProj (n, _, _) => ignore (E.lookupStrNamed env' n)
+ | L'.CUnif (_, _, _, _, r as ref (L'.Unknown f)) =>
+ r := L'.Unknown (fn c => f c andalso validateCon env' c)
+ | _ => (),
+ bind = fn (env', b) => case b of
+ U.Con.RelK x => E.pushKRel env' x
+ | U.Con.RelC (x, k) => E.pushCRel env' x k
+ | U.Con.NamedC (x, n, k, co) => E.pushCNamedAs env x n k co}
+ env c;
+ true)
+ handle _ => false
+
+ and validateKind env k = validateCon env (L'.CRecord (k, []), ErrorMsg.dummySpan)
+
exception KUnify' of kunify_error
fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) =
@@ -93,38 +116,49 @@
| (L'.KError, _) => ()
| (_, L'.KError) => ()
- | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All
- | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All
+ | (L'.KUnif (_, _, ref (L'.KKnown k1All)), _) => unifyKinds' env k1All k2All
+ | (_, L'.KUnif (_, _, ref (L'.KKnown k2All))) => unifyKinds' env k1All k2All
- | (L'.KTupleUnif (_, _, ref (SOME k)), _) => unifyKinds' env k k2All
- | (_, L'.KTupleUnif (_, _, ref (SOME k))) => unifyKinds' env k1All k
+ | (L'.KTupleUnif (_, _, ref (L'.KKnown k)), _) => unifyKinds' env k k2All
+ | (_, L'.KTupleUnif (_, _, ref (L'.KKnown k))) => unifyKinds' env k1All k
- | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
+ | (L'.KUnif (_, _, r1 as ref (L'.KUnknown f1)), L'.KUnif (_, _, r2 as ref (L'.KUnknown f2))) =>
if r1 = r2 then
()
else
- r1 := SOME k2All
+ (r1 := L'.KKnown k2All;
+ r2 := L'.KUnknown (fn x => f1 x andalso f2 x))
- | (L'.KUnif (_, _, r), _) =>
+ | (L'.KUnif (_, _, r as ref (L'.KUnknown f)), _) =>
if occursKind r k2All then
err KOccursCheckFailed
+ else if not (f k2All) then
+ err KScope
else
- r := SOME k2All
- | (_, L'.KUnif (_, _, r)) =>
+ r := L'.KKnown k2All
+ | (_, L'.KUnif (_, _, r as ref (L'.KUnknown f))) =>
if occursKind r k1All then
err KOccursCheckFailed
+ else if not (f k1All) then
+ err KScope
+ else
+ r := L'.KKnown k1All
+
+ | (L'.KTupleUnif (_, nks, r as ref (L'.KUnknown f)), L'.KTuple ks) =>
+ if not (f k2All) then
+ err KScope
+ else
+ ((app (fn (n, k) => unifyKinds' env k (List.nth (ks, n-1))) nks;
+ r := L'.KKnown k2All)
+ handle Subscript => err KIncompatible)
+ | (L'.KTuple ks, L'.KTupleUnif (_, nks, r as ref (L'.KUnknown f))) =>
+ if not (f k2All) then
+ err KScope
else
- r := SOME k1All
-
- | (L'.KTupleUnif (_, nks, r), L'.KTuple ks) =>
- ((app (fn (n, k) => unifyKinds' env k (List.nth (ks, n-1))) nks;
- r := SOME k2All)
- handle Subscript => err KIncompatible)
- | (L'.KTuple ks, L'.KTupleUnif (_, nks, r)) =>
- ((app (fn (n, k) => unifyKinds' env (List.nth (ks, n-1)) k) nks;
- r := SOME k1All)
- handle Subscript => err KIncompatible)
- | (L'.KTupleUnif (loc, nks1, r1), L'.KTupleUnif (_, nks2, r2)) =>
+ ((app (fn (n, k) => unifyKinds' env (List.nth (ks, n-1)) k) nks;
+ 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) =>
@@ -136,10 +170,10 @@
| SOME k2 => (unifyKinds' env k1 k2;
nks)) nks2 nks1
- val k = (L'.KTupleUnif (loc, nks, ref NONE), loc)
+ val k = (L'.KTupleUnif (loc, nks, ref (L'.KUnknown (fn x => f1 x andalso f2 x))), loc)
in
- r1 := SOME k;
- r2 := SOME k
+ r1 := L'.KKnown k;
+ r2 := L'.KKnown k
end
| _ => err KIncompatible
@@ -174,13 +208,14 @@
val char = ref cerror
val table = ref cerror
+
local
val count = ref 0
in
fun resetKunif () = count := 0
- fun kunif loc =
+ fun kunif' f loc =
let
val n = !count
val s = if n <= 26 then
@@ -189,9 +224,11 @@
"U" ^ Int.toString (n - 26)
in
count := n + 1;
- (L'.KUnif (loc, s, ref NONE), loc)
+ (L'.KUnif (loc, s, ref (L'.KUnknown f)), loc)
end
+ fun kunif env = kunif' (validateKind env)
+
end
local
@@ -200,7 +237,7 @@
fun resetCunif () = count := 0
- fun cunif (loc, k) =
+ fun cunif' f (loc, k) =
let
val n = !count
val s = if n < 26 then
@@ -209,9 +246,11 @@
"U" ^ Int.toString (n - 26)
in
count := n + 1;
- (L'.CUnif (0, loc, k, s, ref NONE), loc)
+ (L'.CUnif (0, loc, k, s, ref (L'.Unknown f)), loc)
end
+ fun cunif env = cunif' (validateCon env)
+
end
fun elabKind env (k, loc) =
@@ -222,7 +261,7 @@
| L.KRecord k => (L'.KRecord (elabKind env k), loc)
| L.KUnit => (L'.KUnit, loc)
| L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc)
- | L.KWild => kunif loc
+ | L.KWild => kunif env loc
| L.KVar s => (case E.lookupK env s of
NONE =>
@@ -238,18 +277,18 @@
fun hnormKind (kAll as (k, _)) =
case k of
- L'.KUnif (_, _, ref (SOME k)) => hnormKind k
+ L'.KUnif (_, _, ref (L'.KKnown k)) => hnormKind k
| _ => kAll
open ElabOps
- fun elabConHead (c as (_, loc)) k =
+ fun elabConHead env (c as (_, loc)) k =
let
fun unravel (k, c) =
case hnormKind k of
(L'.KFun (x, k'), _) =>
let
- val u = kunif loc
+ val u = kunif env loc
val k'' = subKindInKind (0, u) k'
in
@@ -303,8 +342,8 @@
val (c1', k1, gs1) = elabCon (env, denv) c1
val (c2', k2, gs2) = elabCon (env, denv) c2
- val ku1 = kunif loc
- val ku2 = kunif loc
+ val ku1 = kunif env loc
+ val ku2 = kunif env loc
val denv' = D.assert env denv (c1', c2')
val (c', k, gs4) = elabCon (env, denv') c
@@ -331,13 +370,13 @@
(cerror, kerror, []))
| E.Rel (n, k) =>
let
- val (c, k) = elabConHead (L'.CRel n, loc) k
+ val (c, k) = elabConHead env (L'.CRel n, loc) k
in
(c, k, [])
end
| E.Named (n, k) =>
let
- val (c, k) = elabConHead (L'.CNamed n, loc) k
+ val (c, k) = elabConHead env (L'.CNamed n, loc) k
in
(c, k, [])
end)
@@ -358,7 +397,7 @@
NONE => (conError env (UnboundCon (loc, s));
kerror)
| SOME (k, _) => k
- val (c, k) = elabConHead (L'.CModProj (n, ms, s), loc) k
+ val (c, k) = elabConHead env (L'.CModProj (n, ms, s), loc) k
in
(c, k, [])
end)
@@ -367,8 +406,8 @@
let
val (c1', k1, gs1) = elabCon (env, denv) c1
val (c2', k2, gs2) = elabCon (env, denv) c2
- val dom = kunif loc
- val ran = kunif loc
+ val dom = kunif env loc
+ val ran = kunif env loc
in
checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
checkKind env c2' k2 dom;
@@ -377,7 +416,7 @@
| L.CAbs (x, ko, t) =>
let
val k' = case ko of
- NONE => kunif loc
+ NONE => kunif env loc
| SOME k => elabKind env k
val env' = E.pushCRel env x k'
val (t', tk, gs) = elabCon (env', D.enter denv) t
@@ -401,7 +440,7 @@
| L.CRecord xcs =>
let
- val k = kunif loc
+ val k = kunif env loc
val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
let
@@ -439,7 +478,7 @@
let
val (c1', k1, gs1) = elabCon (env, denv) c1
val (c2', k2, gs2) = elabCon (env, denv) c2
- val ku = kunif loc
+ val ku = kunif env loc
val k = (L'.KRecord ku, loc)
in
checkKind env c1' k1 k;
@@ -449,8 +488,8 @@
end
| L.CMap =>
let
- val dom = kunif loc
- val ran = kunif loc
+ val dom = kunif env loc
+ val ran = kunif env loc
in
((L'.CMap (dom, ran), loc),
mapKind (dom, ran, loc),
@@ -474,13 +513,13 @@
let
val (c', k, gs) = elabCon (env, denv) c
- val k' = kunif loc
+ val k' = kunif env loc
in
if n <= 0 then
(conError env (ProjBounds (c', n));
(cerror, kerror, []))
else
- (checkKind env c' k (L'.KTupleUnif (loc, [(n, k')], ref NONE), loc);
+ (checkKind env c' k (L'.KTupleUnif (loc, [(n, k')], ref (L'.KUnknown (validateKind env))), loc);
((L'.CProj (c', n), loc), k', gs))
end
@@ -488,19 +527,19 @@
let
val k' = elabKind env k
in
- (cunif (loc, k'), k', [])
+ (cunif env (loc, k'), k', [])
end
fun kunifsRemain k =
case k of
- L'.KUnif (_, _, ref NONE) => true
- | L'.KTupleUnif (_, _, ref NONE) => true
+ L'.KUnif (_, _, ref (L'.KUnknown _)) => true
+ | L'.KTupleUnif (_, _, ref (L'.KUnknown _)) => true
| _ => false
fun cunifsRemain c =
case c of
- L'.CUnif (_, loc, k, _, r as ref NONE) =>
+ L'.CUnif (_, loc, k, _, r as ref (L'.Unknown _)) =>
(case #1 (hnormKind k) of
- L'.KUnit => (r := SOME (L'.CUnit, loc); false)
+ L'.KUnit => (r := L'.Known (L'.CUnit, loc); false)
| _ => true)
| _ => false
@@ -529,7 +568,7 @@
type record_summary = {
fields : (L'.con * L'.con) list,
- unifs : (L'.con * L'.con option ref) list,
+ unifs : (L'.con * L'.cunif ref) list,
others : L'.con list
}
@@ -598,10 +637,10 @@
(L'.KTuple ks, _) => List.nth (ks, n - 1)
| (L'.KUnif (_, _, r), _) =>
let
- val ku = kunif loc
- val k = (L'.KTupleUnif (loc, [(n, ku)], ref NONE), loc)
+ val ku = kunif env loc
+ val k = (L'.KTupleUnif (loc, [(n, ku)], r), loc)
in
- r := SOME k;
+ r := L'.KKnown k;
k
end
| (L'.KTupleUnif (_, nks, r), _) =>
@@ -609,10 +648,10 @@
SOME k => k
| NONE =>
let
- val ku = kunif loc
- val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), ref NONE), loc)
+ val ku = kunif env loc
+ val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), r), loc)
in
- r := SOME k;
+ r := L'.KKnown k;
k
end)
| k => raise CUnify' (CKindof (k, c, "tuple")))
@@ -713,11 +752,11 @@
case hnormKind (kindof env c) of
(L'.KRecord k, _) => k
| (L'.KError, _) => kerror
- | (L'.KUnif (_, _, r), _) =>
+ | (L'.KUnif (_, _, r as ref (L'.KUnknown f)), _) =>
let
- val k = kunif (#2 c)
+ val k = kunif' f (#2 c)
in
- r := SOME (L'.KRecord k, #2 c);
+ r := L'.KKnown (L'.KRecord k, #2 c);
k
end
| k => raise CUnify' (CKindof (k, c, "record"))
@@ -751,7 +790,7 @@
unifs = #unifs s1 @ #unifs s2,
others = #others s1 @ #others s2}
end
- | (L'.CUnif (nl, _, _, _, ref (SOME c)), _) => recordSummary env (E.mliftConInCon nl c)
+ | (L'.CUnif (nl, _, _, _, ref (L'.Known c)), _) => recordSummary env (E.mliftConInCon nl c)
| c' as (L'.CUnif (0, _, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
| c' => {fields = [], unifs = [], others = [c']}
in
@@ -845,35 +884,41 @@
val (unifs1, fs1, others1, unifs2, fs2, others2) =
case (unifs1, fs1, others1, unifs2, fs2, others2) of
- orig as ([(_, r)], [], [], _, _, _) =>
+ orig as ([(_, r as ref (L'.Unknown f))], [], [], _, _, _) =>
let
val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
in
- if occursCon r c then
+ if occursCon r c orelse not (f c) then
orig
else
- (r := SOME c;
+ (r := L'.Known c;
empties)
end
- | orig as (_, _, _, [(_, r)], [], []) =>
+ | orig as (_, _, _, [(_, r as ref (L'.Unknown f))], [], []) =>
let
val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
in
- if occursCon r c then
+ if occursCon r c orelse not (f c) then
orig
else
- (r := SOME c;
+ (r := L'.Known c;
empties)
end
- | orig as ([(_, r1 as ref NONE)], _, [], [(_, r2 as ref NONE)], _, []) =>
+ | orig as ([(_, r1 as ref (L'.Unknown f1))], _, [], [(_, r2 as ref (L'.Unknown f2))], _, []) =>
if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then
let
val kr = (L'.KRecord k, loc)
- val u = cunif (loc, kr)
+ val u = cunif env (loc, kr)
+
+ val c1 = (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc)
+ val c2 = (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc)
in
- r1 := SOME (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc);
- r2 := SOME (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc);
- empties
+ if not (f1 c1) orelse not (f2 c2) then
+ orig
+ else
+ (r1 := L'.Known c1;
+ r2 := L'.Known c2;
+ empties)
end
else
orig
@@ -950,10 +995,10 @@
in
(case (unifs1, fs1, others1, unifs2, fs2, others2) of
(_, [], [], [], [], []) =>
- app (fn (_, r) => r := SOME empty) unifs1
+ app (fn (_, r) => r := L'.Known empty) unifs1
| ([], [], [], _, [], []) =>
- app (fn (_, r) => r := SOME empty) unifs2
- | (_, _, _, [], [], [cr as (L'.CUnif (nl, _, _, _, r), _)]) =>
+ app (fn (_, r) => r := L'.Known empty) unifs2
+ | (_, _, _, [], [], [cr as (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _)]) =>
let
val c = summaryToCon {fields = fs1, unifs = unifs1, others = others1}
in
@@ -961,10 +1006,17 @@
(reducedSummaries := NONE;
raise CUnify' (COccursCheckFailed (cr, c)))
else
- (r := SOME (squish nl c))
+ let
+ val sq = squish nl c
+ in
+ if not (f sq) then
+ default ()
+ else
+ r := L'.Known sq
+ end
handle CantSquish => default ()
end
- | ([], [], [cr as (L'.CUnif (nl, _, _, _, r), _)], _, _, _) =>
+ | ([], [], [cr as (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _)], _, _, _) =>
let
val c = summaryToCon {fields = fs2, unifs = unifs2, others = others2}
in
@@ -972,7 +1024,14 @@
(reducedSummaries := NONE;
raise CUnify' (COccursCheckFailed (cr, c)))
else
- (r := SOME (squish nl c))
+ let
+ val sq = squish nl c
+ in
+ if not (f sq) then
+ default ()
+ else
+ r := L'.Known sq
+ end
handle CantSquish => default ()
end
| _ => default ())
@@ -992,15 +1051,15 @@
let
val v' = case dom of
(L'.KUnit, _) => (L'.CUnit, loc)
- | _ => cunif (loc, dom)
+ | _ => cunif env (loc, dom)
in
unifyCons env loc v (L'.CApp (f, v'), loc);
unifyCons env loc r (L'.CRecord (dom, [(x, v')]), loc)
end
| L'.CRecord (_, (x, v) :: rest) =>
let
- val r1 = cunif (loc, (L'.KRecord dom, loc))
- val r2 = cunif (loc, (L'.KRecord dom, loc))
+ val r1 = cunif env (loc, (L'.KRecord dom, loc))
+ val r2 = cunif env (loc, (L'.KRecord dom, loc))
in
unfold (r1, (L'.CRecord (ran, [(x, v)]), loc));
unfold (r2, (L'.CRecord (ran, rest), loc));
@@ -1008,15 +1067,22 @@
end
| L'.CConcat (c1', c2') =>
let
- val r1 = cunif (loc, (L'.KRecord dom, loc))
- val r2 = cunif (loc, (L'.KRecord dom, loc))
+ val r1 = cunif env (loc, (L'.KRecord dom, loc))
+ val r2 = cunif env (loc, (L'.KRecord dom, loc))
in
unfold (r1, c1');
unfold (r2, c2');
unifyCons env loc r (L'.CConcat (r1, r2), loc)
end
- | L'.CUnif (0, _, _, _, ur) =>
- ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc)
+ | L'.CUnif (0, _, _, _, ur as ref (L'.Unknown rf)) =>
+ let
+ val c' = (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc)
+ in
+ if not (rf c') then
+ cunifyError env (CScope (c, c'))
+ else
+ ur := L'.Known c'
+ end
| _ => raise ex
in
unfold (r, c)
@@ -1063,14 +1129,14 @@
onFail ()
in
case #1 (hnormCon env c2) of
- L'.CUnif (0, _, k, _, r) =>
+ L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
(case #1 (hnormKind k) of
L'.KTuple ks =>
let
val loc = #2 c2
- val us = map (fn k => cunif (loc, k)) ks
+ val us = map (fn k => cunif' f (loc, k)) ks
in
- r := SOME (L'.CTuple us, loc);
+ r := L'.Known (L'.CTuple us, loc);
unifyCons' env loc c1All (List.nth (us, n2 - 1))
end
| _ => tryNormal ())
@@ -1079,14 +1145,14 @@
| _ => onFail ()
in
case #1 (hnormCon env c1) of
- L'.CUnif (0, _, k, _, r) =>
+ L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
(case #1 (hnormKind k) of
L'.KTuple ks =>
let
val loc = #2 c1
- val us = map (fn k => cunif (loc, k)) ks
+ val us = map (fn k => cunif' f (loc, k)) ks
in
- r := SOME (L'.CTuple us, loc);
+ r := L'.Known (L'.CTuple us, loc);
unifyCons' env loc (List.nth (us, n1 - 1)) c2All
end
| _ => trySnd ())
@@ -1095,14 +1161,14 @@
fun projSpecial2 (c2, n2, onFail) =
case #1 (hnormCon env c2) of
- L'.CUnif (0, _, k, _, r) =>
+ L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
(case #1 (hnormKind k) of
L'.KTuple ks =>
let
val loc = #2 c2
- val us = map (fn k => cunif (loc, k)) ks
+ val us = map (fn k => cunif' f (loc, k)) ks
in
- r := SOME (L'.CTuple us, loc);
+ r := L'.Known (L'.CTuple us, loc);
unifyCons' env loc c1All (List.nth (us, n2 - 1))
end
| _ => onFail ())
@@ -1123,40 +1189,64 @@
(L'.CError, _) => ()
| (_, L'.CError) => ()
- | (L'.CUnif (nl1, loc1, k1, _, r1), L'.CUnif (nl2, loc2, k2, _, r2)) =>
+ | (L'.CUnif (nl1, loc1, k1, _, r1 as ref (L'.Unknown f1)), L'.CUnif (nl2, loc2, k2, _, r2 as ref (L'.Unknown f2))) =>
if r1 = r2 andalso nl1 = nl2 then
()
else if nl1 = 0 then
(unifyKinds env k1 k2;
- r1 := SOME c2All)
+ if f1 c2All then
+ r1 := L'.Known c2All
+ else
+ err CScope)
else if nl2 = 0 then
(unifyKinds env k1 k2;
- r2 := SOME c1All)
+ if f2 c1All then
+ r2 := L'.Known c1All
+ else
+ err CScope)
else
err (fn _ => TooLifty (loc1, loc2))
- | (L'.CUnif (0, _, _, _, r), _) =>
+ | (L'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) =>
if occursCon r c2All then
err COccursCheckFailed
+ else if f c2All then
+ r := L'.Known c2All
else
- r := SOME c2All
- | (_, L'.CUnif (0, _, _, _, r)) =>
+ err CScope
+ | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) =>
if occursCon r c1All then
err COccursCheckFailed
+ else if f c1All then
+ r := L'.Known c1All
else
- r := SOME c1All
+ err CScope
- | (L'.CUnif (nl, _, _, _, r), _) =>
+ | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) =>
if occursCon r c2All then
err COccursCheckFailed
else
- (r := SOME (squish nl c2All)
+ (let
+ val sq = squish nl c2All
+ in
+ if f sq then
+ r := L'.Known sq
+ else
+ err CScope
+ end
handle CantSquish => err (fn _ => TooDeep))
- | (_, L'.CUnif (nl, _, _, _, r)) =>
+ | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) =>
if occursCon r c1All then
err COccursCheckFailed
else
- (r := SOME (squish nl c1All)
+ (let
+ val sq = squish nl c1All
+ in
+ if f sq then
+ r := L'.Known sq
+ else
+ err CScope
+ end
handle CantSquish => err (fn _ => TooDeep))
| (L'.CRecord _, _) => isRecord ()
@@ -1169,7 +1259,7 @@
| (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
(unifyCons' env loc d1 d2;
- unifyCons' env loc r1 r2)
+ unifyCons' env loc r1 r2)
| (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
if expl1 <> expl2 then
err CExplicitness
@@ -1295,7 +1385,7 @@
case hnormCon env t of
(L'.TKFun (x, t'), _) =>
let
- val u = kunif loc
+ val u = kunif env loc
val t'' = subKindInCon (0, u) t'
in
@@ -1307,7 +1397,7 @@
case hnormCon env t of
(L'.TKFun (x, t'), _) =>
let
- val u = kunif loc
+ val u = kunif env loc
val t'' = subKindInCon (0, u) t'
in
@@ -1315,7 +1405,7 @@
end
| (L'.TCFun (L'.Implicit, x, k, t'), _) =>
let
- val u = cunif (loc, k)
+ val u = cunif env (loc, k)
val t'' = subConInCon env (0, u) t'
in
@@ -1393,7 +1483,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
| (NONE, NONE) =>
let
val k = (L'.KType, loc)
- val unifs = map (fn _ => cunif (loc, k)) xs
+ val unifs = map (fn _ => cunif env (loc, k)) xs
val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
in
(((L'.PCon (dk, pc, unifs, NONE), loc), dn),
@@ -1404,7 +1494,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
val k = (L'.KType, loc)
- val unifs = map (fn _ => cunif (loc, k)) xs
+ val unifs = map (fn _ => cunif env (loc, k)) xs
val nxs = length unifs - 1
val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i,
E.mliftConInCon (nxs - i) u) t) t unifs
@@ -1416,7 +1506,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
end
in
case p of
- L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))),
+ L.PWild => (((L'.PWild, loc), cunif env (loc, (L'.KType, loc))),
(env, bound))
| L.PVar x =>
let
@@ -1424,7 +1514,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
(expError env (DuplicatePatternVariable (loc, x));
terror)
else
- cunif (loc, (L'.KType, loc))
+ cunif env (loc, (L'.KType, loc))
in
(((L'.PVar (x, t), loc), t),
(E.pushERel env x t, SS.add (bound, x)))
@@ -1473,7 +1563,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc)
val c =
if flex then
- (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc)
+ (L'.CConcat (c, cunif env (loc, (L'.KRecord k, loc))), loc)
else
c
in
@@ -1778,7 +1868,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 (nl, _, _, _, ref (SOME c)) => normClassConstraint env (E.mliftConInCon nl c)
+ | L'.CUnif (nl, _, _, _, ref (L'.Known c)) => normClassConstraint env (E.mliftConInCon nl c)
| _ => unmodCon env (c, loc)
fun findHead e e' =
@@ -1887,7 +1977,7 @@ fun ndelVal (r : needed, k) =
fun chaseUnifs c =
case #1 c of
- L'.CUnif (_, _, _, _, ref (SOME c)) => chaseUnifs c
+ L'.CUnif (_, _, _, _, ref (L'.Known c)) => chaseUnifs c
| _ => c
fun elabExp (env, denv) (eAll as (e, loc)) =
@@ -1937,7 +2027,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
| L.EWild =>
let
val r = ref NONE
- val c = cunif (loc, (L'.KType, loc))
+ val c = cunif env (loc, (L'.KType, loc))
in
((L'.EUnif r, loc), c, [TypeClass (env, c, r, loc)])
end
@@ -1948,8 +2038,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (e2', t2, gs2) = elabExp (env, denv) e2
- val dom = cunif (loc, ktype)
- val ran = cunif (loc, ktype)
+ val dom = cunif env (loc, ktype)
+ val ran = cunif env (loc, ktype)
val t = (L'.TFun (dom, ran), loc)
val () = checkCon env e1' t1 t
@@ -1966,7 +2056,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
| L.EAbs (x, to, e) =>
let
val (t', gs1) = case to of
- NONE => (cunif (loc, ktype), [])
+ NONE => (cunif env (loc, ktype), [])
| SOME t =>
let
val (t', tk, gs) = elabCon (env, denv) t
@@ -2042,8 +2132,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (c1', k1, gs1) = elabCon (env, denv) c1
val (c2', k2, gs2) = elabCon (env, denv) c2
- val ku1 = kunif loc
- val ku2 = kunif loc
+ val ku1 = kunif env loc
+ val ku2 = kunif env loc
val denv' = D.assert env denv (c1', c2')
val (e', t, gs3) = elabExp (env, denv') e
@@ -2057,11 +2147,11 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
let
val (e', t, gs1) = elabExp (env, denv) e
- val k1 = kunif loc
- val c1 = cunif (loc, (L'.KRecord k1, loc))
- val k2 = kunif loc
- val c2 = cunif (loc, (L'.KRecord k2, loc))
- val t' = cunif (loc, ktype)
+ val k1 = kunif env loc
+ val c1 = cunif env (loc, (L'.KRecord k1, loc))
+ val k2 = kunif env loc
+ val c2 = cunif env (loc, (L'.KRecord k2, loc))
+ val t' = cunif env (loc, ktype)
val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc)
val gs2 = D.prove env denv (c1, c2, loc)
in
@@ -2115,8 +2205,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (e', et, gs1) = elabExp (env, denv) e
val (c', ck, gs2) = elabCon (env, denv) c
- val ft = cunif (loc, ktype)
- val rest = cunif (loc, ktype_record)
+ val ft = cunif env (loc, ktype)
+ val rest = cunif env (loc, ktype_record)
val first = (L'.CRecord (ktype, [(c', ft)]), loc)
val () = checkCon env e' et
(L'.TRecord (L'.CConcat (first, rest), loc), loc);
@@ -2130,8 +2220,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (e1', e1t, gs1) = elabExp (env, denv) e1
val (e2', e2t, gs2) = elabExp (env, denv) e2
- val r1 = cunif (loc, ktype_record)
- val r2 = cunif (loc, ktype_record)
+ val r1 = cunif env (loc, ktype_record)
+ val r2 = cunif env (loc, ktype_record)
val () = checkCon env e1' e1t (L'.TRecord r1, loc)
val () = checkCon env e2' e2t (L'.TRecord r2, loc)
@@ -2147,8 +2237,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (e', et, gs1) = elabExp (env, denv) e
val (c', ck, gs2) = elabCon (env, denv) c
- val ft = cunif (loc, ktype)
- val rest = cunif (loc, ktype_record)
+ val ft = cunif env (loc, ktype)
+ val rest = cunif env (loc, ktype_record)
val first = (L'.CRecord (ktype, [(c', ft)]), loc)
val () = checkCon env e' et
@@ -2165,7 +2255,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (e', et, gs1) = elabExp (env, denv) e
val (c', ck, gs2) = elabCon (env, denv) c
- val rest = cunif (loc, ktype_record)
+ val rest = cunif env (loc, ktype_record)
val () = checkCon env e' et
(L'.TRecord (L'.CConcat (c', rest), loc), loc)
@@ -2180,7 +2270,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
| L.ECase (e, pes) =>
let
val (e', et, gs1) = elabExp (env, denv) e
- val result = cunif (loc, (L'.KType, loc))
+ val result = cunif env (loc, (L'.KType, loc))
val (pes', gs) = ListUtil.foldlMap
(fn ((p, e), gs) =>
let
@@ -2255,7 +2345,7 @@ and elabEdecl denv (dAll as (d, loc), (env, gs)) =
(fn ((x, co, e), gs) =>
let
val (c', _, gs1) = case co of
- NONE => (cunif (loc, ktype), ktype, [])
+ NONE => (cunif env (loc, ktype), ktype, [])
| SOME c => elabCon (env, denv) c
in
((x, c', e), enD gs1 @ gs)
@@ -2339,7 +2429,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
| L.SgiCon (x, ko, c) =>
let
val k' = case ko of
- NONE => kunif loc
+ NONE => kunif env loc
| SOME k => elabKind env k
val (c', ck, gs') = elabCon (env, denv) c
@@ -2479,8 +2569,8 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
val (c', ck, gs') = elabCon (env, denv) c
- val pkey = cunif (loc, cstK)
- val visible = cunif (loc, cstK)
+ val pkey = cunif env (loc, cstK)
+ val visible = cunif env (loc, cstK)
val (env', ds, uniques) =
case (#1 pe, #1 ce) of
(L.EVar (["Basis"], "no_primary_key", _), L.EVar (["Basis"], "no_constraint", _)) =>
@@ -2556,8 +2646,8 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
val denv = D.assert env denv (c1', c2')
in
- checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
- checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
+ checkKind env c1' k1 (L'.KRecord (kunif env loc), loc);
+ checkKind env c2' k2 (L'.KRecord (kunif env loc), loc);
([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2))
end
@@ -3421,9 +3511,9 @@ and wildifyStr env (str, sgn) =
end
| L'.KError => NONE
- | L'.KUnif (_, _, ref (SOME k)) => decompileKind k
+ | L'.KUnif (_, _, ref (L'.KKnown k)) => decompileKind k
| L'.KUnif _ => NONE
- | L'.KTupleUnif (_, _, ref (SOME k)) => decompileKind k
+ | L'.KTupleUnif (_, _, ref (L'.KKnown k)) => decompileKind k
| L'.KTupleUnif _ => NONE
| L'.KRel _ => NONE
@@ -3472,7 +3562,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 (nl, _, _, _, ref (SOME c)) => decompileCon env (E.mliftConInCon nl c)
+ | L'.CUnif (nl, _, _, _, ref (L'.Known c)) => decompileCon env (E.mliftConInCon nl c)
| L'.CApp (f, x) =>
(case (decompileCon env f, decompileCon env x) of
@@ -3599,7 +3689,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
L.DCon (x, ko, c) =>
let
val k' = case ko of
- NONE => kunif loc
+ NONE => kunif env loc
| SOME k => elabKind env k
val (c', ck, gs') = elabCon (env, denv) c
@@ -3723,7 +3813,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
| L.DVal (x, co, e) =>
let
val (c', _, gs1) = case co of
- NONE => (cunif (loc, ktype), ktype, [])
+ NONE => (cunif env (loc, ktype), ktype, [])
| SOME c => elabCon (env, denv) c
val (e', et, gs2) = elabExp (env, denv) e
@@ -3751,7 +3841,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
(fn ((x, co, e), gs) =>
let
val (c', _, gs1) = case co of
- NONE => (cunif (loc, ktype), ktype, [])
+ NONE => (cunif env (loc, ktype), ktype, [])
| SOME c => elabCon (env, denv) c
val c' = normClassConstraint env c'
in
@@ -3868,8 +3958,8 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
val denv' = D.assert env denv (c1', c2')
in
- checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
- checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
+ checkKind env c1' k1 (L'.KRecord (kunif env loc), loc);
+ checkKind env c2' k2 (L'.KRecord (kunif env loc), loc);
([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ gs))
end
@@ -3959,8 +4049,8 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
val (c', k, gs') = elabCon (env, denv) c
- val pkey = cunif (loc, cstK)
- val uniques = cunif (loc, cstK)
+ val pkey = cunif env (loc, cstK)
+ val uniques = cunif env (loc, cstK)
val ct = tableOf ()
val ct = (L'.CApp (ct, c'), loc)
@@ -3995,8 +4085,8 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
val (e', t, gs') = elabExp (env, denv) e
val k = (L'.KRecord (L'.KType, loc), loc)
- val fs = cunif (loc, k)
- val ts = cunif (loc, (L'.KRecord k, loc))
+ val fs = cunif env (loc, k)
+ val ts = cunif env (loc, (L'.KRecord k, loc))
val tf = (L'.CApp ((L'.CMap (k, k), loc),
(L'.CAbs ("_", k, (L'.CRecord ((L'.KType, loc), []), loc)), loc)), loc)
val ts = (L'.CApp (tf, ts), loc)
@@ -4048,7 +4138,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
val (e1', t1, gs1) = elabExp (env, denv) e1
val (e2', t2, gs2) = elabExp (env, denv) e2
- val targ = cunif (loc, (L'.KType, loc))
+ val targ = cunif env (loc, (L'.KType, loc))
val t1' = (L'.CModProj (!basis_r, [], "task_kind"), loc)
val t1' = (L'.CApp (t1', targ), loc)
diff --git a/src/explify.sml b/src/explify.sml
index 5081d33b..3c922a44 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -42,9 +42,9 @@ fun explifyKind (k, loc) =
| L.KTuple ks => (L'.KTuple (map explifyKind ks), loc)
| L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc)
- | L.KUnif (_, _, ref (SOME k)) => explifyKind k
+ | L.KUnif (_, _, ref (L.KKnown k)) => explifyKind k
| L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
- | L.KTupleUnif (loc, _, ref (SOME k)) => explifyKind k
+ | L.KTupleUnif (loc, _, ref (L.KKnown k)) => explifyKind k
| L.KTupleUnif _ => raise Fail ("explifyKind: KTupleUnif at " ^ EM.spanToString loc)
| L.KRel n => (L'.KRel n, loc)
@@ -76,7 +76,7 @@ fun explifyCon (c, loc) =
| L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc)
| L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
- | L.CUnif (nl, _, _, _, ref (SOME c)) => explifyCon (ElabEnv.mliftConInCon nl c)
+ | L.CUnif (nl, _, _, _, ref (L.Known c)) => explifyCon (ElabEnv.mliftConInCon nl c)
| L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
| L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc)
diff --git a/tests/capture.ur b/tests/capture.ur
new file mode 100644
index 00000000..0eb3d8b5
--- /dev/null
+++ b/tests/capture.ur
@@ -0,0 +1,4 @@
+val y = []
+
+type foo = int
+val z : list {F : foo} = y
diff --git a/tests/rcapture.ur b/tests/rcapture.ur
new file mode 100644
index 00000000..782efcd9
--- /dev/null
+++ b/tests/rcapture.ur
@@ -0,0 +1,3 @@
+fun frob x = x
+
+fun foo [a] (x : a) = frob x
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-20 20:21:29 +0000