From 948aa854af8ca5560a1eea5221c4a1f3a6901970 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 10 Oct 2010 14:41:03 -0400 Subject: Hopeful fix for the Great Unification Bug --- demo/crud.ur | 4 ++-- demo/crud3.ur | 2 +- demo/metaform.ur | 9 ++++---- demo/view.ur | 2 +- src/elab.sml | 2 +- src/elab_env.sig | 2 +- src/elab_env.sml | 40 +++++++++++++++++++++++++---------- src/elab_err.sig | 4 +++- src/elab_err.sml | 12 +++++++++-- src/elab_ops.sig | 2 ++ src/elab_ops.sml | 13 +++++++----- src/elab_print.sml | 11 ++++++---- src/elab_util.sig | 4 +++- src/elab_util.sml | 6 ++++-- src/elaborate.sml | 62 ++++++++++++++++++++++++++++++------------------------ src/explify.sml | 2 +- tests/concat.ur | 13 ++++++++++++ tests/concat.urp | 1 + 18 files changed, 125 insertions(+), 66 deletions(-) create mode 100644 tests/concat.ur create mode 100644 tests/concat.urp 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

{@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)) => + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (col : colMeta t) acc =>

{cdata col.Nam}: {col.Widget [nm]}

{useMore acc} ) @@ -128,7 +128,7 @@ functor Make(M : sig None => return Not found! | Some fs => return {@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)) =>

{cdata col.Nam}: {col.WidgetPopulated [nm] v}

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 ), - 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 {@foldUR [string] [fn cols => xml form [] (mapU string cols)] - (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name - (acc : xml form [] (mapU string rest)) => -

{[name]}:

- {useMore acc} - ) + (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name acc => +

{[name]}:

+ {useMore acc} + ) M.fl M.names} 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}} =>

{[r.X.A]}

); return 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 "" - | CUnif (_, _, _, ref (SOME c)) => p_con' par env c - | CUnif (_, k, s, _) => box [string (""] + | CUnif (nl, _, _, _, ref (SOME c)) => p_con' par env (E.mliftConInCon nl c) + | CUnif (nl, _, k, s, _) => box [string (" 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 -- cgit v1.2.3