Mercurial > urweb
changeset 1639:6c00d8af6239
Add a new scoping check for unification variables, to fix a type inference bug
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 18 Dec 2011 11:29:13 -0500 |
| parents | 3bf727a08db8 |
| children | dc986eb6113c |
| files | src/elab.sml src/elab_env.sml src/elab_err.sig src/elab_err.sml src/elab_ops.sml src/elab_print.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/explify.sml tests/capture.ur tests/rcapture.ur |
| diffstat | 12 files changed, 328 insertions(+), 192 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Sat Dec 17 20:42:39 2011 -0500 +++ b/src/elab.sml Sun Dec 18 11:29:13 2011 -0500 @@ -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 @@ | 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 @@ | 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
--- a/src/elab_env.sml Sat Dec 17 20:42:39 2011 -0500 +++ b/src/elab_env.sml Sun Dec 18 11:29:13 2011 -0500 @@ -484,7 +484,7 @@ 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 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 @@ | (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 @@ 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 @@ 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 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),
--- a/src/elab_err.sig Sat Dec 17 20:42:39 2011 -0500 +++ b/src/elab_err.sig Sun Dec 18 11:29:13 2011 -0500 @@ -35,6 +35,7 @@ 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 @@ | 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
--- a/src/elab_err.sml Sat Dec 17 20:42:39 2011 -0500 +++ b/src/elab_err.sml Sun Dec 18 11:29:13 2011 -0500 @@ -63,6 +63,7 @@ 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 @@ 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 @@ | 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 @@ 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
--- a/src/elab_ops.sml Sat Dec 17 20:42:39 2011 -0500 +++ b/src/elab_ops.sml Sun Dec 18 11:29:13 2011 -0500 @@ -156,7 +156,7 @@ 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 @@ let fun cunif () = let - val r = ref NONE + val r = ref (Unknown (fn _ => true)) in (r, (CUnif (0, loc, (KType, loc), "_", r), loc)) end
--- a/src/elab_print.sml Sat Dec 17 20:42:39 2011 -0500 +++ b/src/elab_print.sml Sun Dec 18 11:29:13 2011 -0500 @@ -54,9 +54,9 @@ 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 @@ 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
--- a/src/elab_util.sig Sat Dec 17 20:42:39 2011 -0500 +++ b/src/elab_util.sig Sun Dec 18 11:29:13 2011 -0500 @@ -64,6 +64,13 @@ 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}
--- a/src/elab_util.sml Sat Dec 17 20:42:39 2011 -0500 +++ b/src/elab_util.sml Sun Dec 18 11:29:13 2011 -0500 @@ -75,10 +75,10 @@ | 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 @@ (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 @@ 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
--- a/src/elaborate.sml Sat Dec 17 20:42:39 2011 -0500 +++ b/src/elaborate.sml Sun Dec 18 11:29:13 2011 -0500 @@ -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'.KTupleUnif (_, _, ref (SOME k)), _) => unifyKinds' env k k2All - | (_, L'.KTupleUnif (_, _, ref (SOME k))) => unifyKinds' env k1All k - - | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) => + | (L'.KUnif (_, _, ref (L'.KKnown k1All)), _) => unifyKinds' env k1All k2All + | (_, L'.KUnif (_, _, ref (L'.KKnown k2All))) => unifyKinds' env k1All k2All + + | (L'.KTupleUnif (_, _, ref (L'.KKnown k)), _) => unifyKinds' env k k2All + | (_, L'.KTupleUnif (_, _, ref (L'.KKnown k))) => unifyKinds' env k1All k + + | (L'.KUnif (_, _, r1 as ref (L'.KUnknown f1)), L'.KUnif (_, _, r2 as ref (L'.KUnknown f2))) => if r1 = r2 then () else - r1 := SOME k2All - - | (L'.KUnif (_, _, r), _) => + (r1 := L'.KKnown k2All; + r2 := L'.KUnknown (fn x => f1 x andalso f2 x)) + + | (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 := 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)) => + 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 + ((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 + 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 + err CScope + + | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) => if occursCon r c2All then err COccursCheckFailed else - r := SOME c2All - | (_, L'.CUnif (0, _, _, _, r)) => + (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 as ref (L'.Unknown f))) => if occursCon r c1All then err COccursCheckFailed else - r := SOME c1All - - | (L'.CUnif (nl, _, _, _, r), _) => - if occursCon r c2All then - err COccursCheckFailed - else - (r := SOME (squish nl c2All) - handle CantSquish => err (fn _ => TooDeep)) - | (_, L'.CUnif (nl, _, _, _, r)) => - 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 @@ | (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 @@ 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 @@ 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 @@ (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 @@ 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 @@ (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 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 @@ | 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 @@ 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 @@ | 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ | 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 @@ (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 @@ | 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 @@ 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 @@ 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 @@ 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 @@ (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 @@ 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 @@ | 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 @@ (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 @@ 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 @@ 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 @@ 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 @@ 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)
--- a/src/explify.sml Sat Dec 17 20:42:39 2011 -0500 +++ b/src/explify.sml Sun Dec 18 11:29:13 2011 -0500 @@ -42,9 +42,9 @@ | 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 @@ | 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)