summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--demo/crud.ur4
-rw-r--r--demo/crud3.ur2
-rw-r--r--demo/metaform.ur9
-rw-r--r--demo/view.ur2
-rw-r--r--src/elab.sml2
-rw-r--r--src/elab_env.sig2
-rw-r--r--src/elab_env.sml40
-rw-r--r--src/elab_err.sig4
-rw-r--r--src/elab_err.sml12
-rw-r--r--src/elab_ops.sig2
-rw-r--r--src/elab_ops.sml13
-rw-r--r--src/elab_print.sml11
-rw-r--r--src/elab_util.sig4
-rw-r--r--src/elab_util.sml6
-rw-r--r--src/elaborate.sml62
-rw-r--r--src/explify.sml2
-rw-r--r--tests/concat.ur13
-rw-r--r--tests/concat.urp1
18 files changed, 125 insertions, 66 deletions
diff --git a/demo/crud.ur b/demo/crud.ur
index 2fc82c1b..4d2753ea 100644
--- a/demo/crud.ur
+++ b/demo/crud.ur
@@ -78,7 +78,7 @@ functor Make(M : sig
<form>
{@foldR [colMeta] [fn cols => xml form [] (map snd cols)]
- (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map snd rest)) => <xml>
+ (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (col : colMeta t) acc => <xml>
<li> {cdata col.Nam}: {col.Widget [nm]}</li>
{useMore acc}
</xml>)
@@ -128,7 +128,7 @@ functor Make(M : sig
None => return <xml><body>Not found!</body></xml>
| Some fs => return <xml><body><form>
{@foldR2 [fst] [colMeta] [fn cols => xml form [] (map snd cols)]
- (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (v : t.1) (col : colMeta t)
+ (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] v (col : colMeta t)
(acc : xml form [] (map snd rest)) =>
<xml>
<li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
diff --git a/demo/crud3.ur b/demo/crud3.ur
index c336af30..5be035dd 100644
--- a/demo/crud3.ur
+++ b/demo/crud3.ur
@@ -20,7 +20,7 @@ open Crud.Make(struct
<textbox{#B}/>
</subform>
</xml>),
- Parse = (fn p => p.A ^ p.B),
+ Parse = (fn p : {A : string, B : string} => p.A ^ p.B),
Inject = _
}
}
diff --git a/demo/metaform.ur b/demo/metaform.ur
index 729b7d08..c6a6e54b 100644
--- a/demo/metaform.ur
+++ b/demo/metaform.ur
@@ -15,11 +15,10 @@ functor Make (M : sig
fun main () = return <xml><body>
<form>
{@foldUR [string] [fn cols => xml form [] (mapU string cols)]
- (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name
- (acc : xml form [] (mapU string rest)) => <xml>
- <li> {[name]}: <textbox{nm}/></li>
- {useMore acc}
- </xml>)
+ (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name acc => <xml>
+ <li> {[name]}: <textbox{nm}/></li>
+ {useMore acc}
+ </xml>)
<xml/>
M.fl M.names}
<submit action={handler}/>
diff --git a/demo/view.ur b/demo/view.ur
index 84c179f4..0dcb42fa 100644
--- a/demo/view.ur
+++ b/demo/view.ur
@@ -1,7 +1,7 @@
table t : { A : int }
view v = SELECT t.A AS A FROM t WHERE t.A > 7
-fun list [u] (_ : fieldsOf u [A = int]) (title : string) (x : u) =
+fun list [u] (_ : fieldsOf u [A = int]) (title : string) (x : u) : transaction xbody =
xml <- queryX (SELECT * FROM x)
(fn r : {X : {A : int}} => <xml><li>{[r.X.A]}</li></xml>);
return <xml>
diff --git a/src/elab.sml b/src/elab.sml
index dcb15502..97acec31 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -78,7 +78,7 @@ datatype con' =
| CProj of con * int
| CError
- | CUnif of ErrorMsg.span * kind * string * con option ref
+ | CUnif of int * ErrorMsg.span * kind * string * con option ref
withtype con = con' located
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 769fea58..662d7071 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -27,8 +27,8 @@
signature ELAB_ENV = sig
- exception SynUnif
val liftConInCon : int -> Elab.con -> Elab.con
+ val mliftConInCon : int -> Elab.con -> Elab.con
val liftConInExp : int -> Elab.exp -> Elab.exp
val liftExpInExp : int -> Elab.exp -> Elab.exp
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 16596622..bb731c08 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -43,8 +43,6 @@ exception UnboundNamed of int
(* AST utility functions *)
-exception SynUnif
-
val liftKindInKind =
U.Kind.mapB {kind = fn bound => fn k =>
case k of
@@ -78,13 +76,32 @@ val liftConInCon =
c
else
CRel (xn + 1)
- (*| CUnif _ => raise SynUnif*)
+ | CUnif (nl, loc, k, s, r) => CUnif (nl+1, loc, k, s, r)
| _ => c,
bind = fn (bound, U.Con.RelC _) => bound + 1
| (bound, _) => bound}
val lift = liftConInCon 0
+fun mliftConInCon by c =
+ if by = 0 then
+ c
+ else
+ U.Con.mapB {kind = fn _ => fn k => k,
+ con = fn bound => fn c =>
+ case c of
+ CRel xn =>
+ if xn < bound then
+ c
+ else
+ CRel (xn + by)
+ | CUnif (nl, loc, k, s, r) => CUnif (nl+by, loc, k, s, r)
+ | _ => c,
+ bind = fn (bound, U.Con.RelC _) => bound + 1
+ | (bound, _) => bound} 0 c
+
+val () = U.mliftConInCon := mliftConInCon
+
val liftKindInExp =
U.Exp.mapB {kind = fn bound => fn k =>
case k of
@@ -108,6 +125,7 @@ val liftConInExp =
c
else
CRel (xn + 1)
+ | CUnif (nl, loc, k, s, r) => CUnif (nl+1, loc, k, s, r)
| _ => c,
exp = fn _ => fn e => e,
bind = fn (bound, U.Exp.RelC _) => bound + 1
@@ -466,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 (SOME c)) => class_name_in c
| _ => NONE
fun isClass (env : env) c =
@@ -480,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 (SOME c)) => class_head_in c
| _ => class_name_in c
exception Unify
@@ -502,8 +520,8 @@ fun unifyKinds (k1, k2) =
fun eqCons (c1, c2) =
case (#1 c1, #1 c2) of
- (CUnif (_, _, _, ref (SOME c1)), _) => eqCons (c1, c2)
- | (_, CUnif (_, _, _, ref (SOME c2))) => eqCons (c1, c2)
+ (CUnif (nl, _, _, _, ref (SOME c1)), _) => eqCons (mliftConInCon nl c1, c2)
+ | (_, CUnif (nl, _, _, _, ref (SOME c2))) => eqCons (c1, mliftConInCon nl c2)
| (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify
@@ -545,8 +563,8 @@ fun unifyCons rs =
let
fun unify d (c1, c2) =
case (#1 c1, #1 c2) of
- (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2)
- | (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2)
+ (CUnif (nl, _, _, _, ref (SOME c1)), _) => unify d (mliftConInCon nl c1, c2)
+ | (_, CUnif (nl, _, _, _, ref (SOME c2))) => unify d (c1, mliftConInCon nl c2)
| (CUnif _, _) => ()
@@ -633,7 +651,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 NONE) => true
| _ => false}
fun startsWithUnif c =
@@ -670,7 +688,7 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) =
val rk = ref NONE
val k = (KUnif (loc, "k", rk), loc)
val r = ref NONE
- val rc = (CUnif (loc, k, "x", r), loc)
+ val rc = (CUnif (0, loc, k, "x", r), loc)
in
((CApp (f, rc), loc),
fn () => (if consEq (rc, x) then
diff --git a/src/elab_err.sig b/src/elab_err.sig
index f6277488..fbe55a5b 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -56,6 +56,8 @@ signature ELAB_ERR = sig
| CExplicitness of Elab.con * Elab.con
| CKindof of Elab.kind * Elab.con * string
| CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con) option
+ | TooLifty of ErrorMsg.span * ErrorMsg.span
+ | TooUnify 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 80de9497..f8a16294 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -112,7 +112,6 @@ fun conError env err =
eprefaces' [("Constructor", p_con env c),
("Kind", p_kind env k)])
-
datatype cunify_error =
CKind of kind * kind * kunify_error
| COccursCheckFailed of con * con
@@ -120,6 +119,8 @@ datatype cunify_error =
| CExplicitness of con * con
| CKindof of kind * con * string
| CRecordFailure of con * con * (con * con * con) option
+ | TooLifty of ErrorMsg.span * ErrorMsg.span
+ | TooUnify of con * con
fun cunifyError env err =
case err of
@@ -154,6 +155,13 @@ fun cunifyError env err =
[("Field", p_con env nm),
("Value 1", p_con env t1),
("Value 2", p_con env t2)]))
+ | TooLifty (loc1, loc2) =>
+ (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings";
+ eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))])
+ | TooUnify (c1, c2) =>
+ (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";
+ eprefaces' [("Replacement", p_con env c1),
+ ("Body", p_con env c2)])
datatype exp_error =
UnboundExp of ErrorMsg.span * string
diff --git a/src/elab_ops.sig b/src/elab_ops.sig
index adf69696..ed4c7d68 100644
--- a/src/elab_ops.sig
+++ b/src/elab_ops.sig
@@ -27,6 +27,8 @@
signature ELAB_OPS = sig
+ exception SubUnif
+
val liftKindInKind : int -> Elab.kind -> Elab.kind
val subKindInKind : int * Elab.kind -> Elab.kind -> Elab.kind
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 6465668f..15d8e106 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -97,11 +97,13 @@ fun liftConInCon by =
c
else
CRel (xn + by)
- (*| CUnif _ => raise SynUnif*)
+ | CUnif (nl, loc, k, s, r) => CUnif (nl+by, loc, k, s, r)
| _ => c,
bind = fn (bound, U.Con.RelC _) => bound + 1
| (bound, _) => bound}
+exception SubUnif
+
fun subConInCon' rep =
U.Con.mapB {kind = fn _ => fn k => k,
con = fn (by, xn) => fn c =>
@@ -111,7 +113,8 @@ fun subConInCon' rep =
EQUAL => #1 (liftConInCon by 0 rep)
| GREATER => CRel (xn' - 1)
| LESS => c)
- (*| CUnif _ => raise SynUnif*)
+ | CUnif (0, _, _, _, _) => raise SubUnif
+ | CUnif (n, loc, k, s, r) => CUnif (n-1, loc, k, s, r)
| _ => c,
bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1)
| (ctx, _) => ctx}
@@ -153,7 +156,7 @@ fun reset () = (identity := 0;
fun hnormCon env (cAll as (c, loc)) =
case c of
- CUnif (_, _, _, ref (SOME c)) => hnormCon env c
+ CUnif (nl, _, _, _, ref (SOME c)) => hnormCon env (E.mliftConInCon nl c)
| CNamed xn =>
(case E.lookupCNamed env xn of
@@ -276,7 +279,7 @@ fun hnormCon env (cAll as (c, loc)) =
let
val r = ref NONE
in
- (r, (CUnif (loc, (KType, loc), "_", r), loc))
+ (r, (CUnif (0, loc, (KType, loc), "_", r), loc))
end
val (vR, v) = cunif ()
@@ -284,7 +287,7 @@ fun hnormCon env (cAll as (c, loc)) =
val c = (CApp (f, v), loc)
in
case unconstraint c of
- (CUnif (_, _, _, vR'), _) =>
+ (CUnif (_, _, _, _, vR'), _) =>
if vR' = vR then
(inc identity;
hnormCon env c2)
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 279c7231..2b8dc5f4 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -202,10 +202,13 @@ fun p_con' par env (c, _) =
string (Int.toString n)]
| CError => string "<ERROR>"
- | CUnif (_, _, _, ref (SOME c)) => p_con' par env c
- | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
- p_kind env k,
- string ">"]
+ | CUnif (nl, _, _, _, ref (SOME c)) => p_con' par env (E.mliftConInCon nl c)
+ | CUnif (nl, _, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
+ p_kind env k,
+ case nl of
+ 0 => box []
+ | _ => string ("+" ^ Int.toString nl),
+ string ">"]
| CKAbs (x, c) => box [string x,
space,
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 934779ff..dc0f25e8 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -29,6 +29,8 @@ signature ELAB_UTIL = sig
val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind
+val mliftConInCon : (int -> Elab.con -> Elab.con) ref
+
structure Kind : sig
val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
bind : 'context * string -> 'context}
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 33ed599c..d297ccbc 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -118,6 +118,8 @@ fun exists f k =
end
+val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con)
+
structure Con = struct
datatype binder =
@@ -215,7 +217,7 @@ fun mapfoldB {kind = fk, con = fc, bind} =
(CProj (c', n), loc))
| CError => S.return2 cAll
- | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
+ | CUnif (nl, _, _, _, ref (SOME c)) => mfc' ctx (!mliftConInCon nl c)
| CUnif _ => S.return2 cAll
| CKAbs (x, c) =>
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
diff --git a/src/explify.sml b/src/explify.sml
index cf6c491c..5081d33b 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -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 (_, _, _, ref (SOME c)) => explifyCon c
+ | L.CUnif (nl, _, _, _, ref (SOME 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/concat.ur b/tests/concat.ur
new file mode 100644
index 00000000..1330a21d
--- /dev/null
+++ b/tests/concat.ur
@@ -0,0 +1,13 @@
+functor Make(M : sig
+ con ts :: {(Type * Type)}
+ val tab : sql_table (map fst ts) []
+ val cols : $(map (fn p => p.2 -> string) ts)
+ end) = struct
+end
+
+table t : {A : string}
+
+open Make(struct
+ val tab = t
+ val cols = {A = fn p : {B : string, C : string} => p.B ^ p.C}
+ end)
diff --git a/tests/concat.urp b/tests/concat.urp
new file mode 100644
index 00000000..442b05b4
--- /dev/null
+++ b/tests/concat.urp
@@ -0,0 +1 @@
+concat
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 23:44:57 +0000