changeset 1303:c7b9a33c26c8

Hopeful fix for the Great Unification Bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 14:41:03 -0400 (2010-10-10)
parents d008c4c43a0a
children f0afe61a6f8b
files demo/crud.ur demo/crud3.ur demo/metaform.ur demo/view.ur src/elab.sml src/elab_env.sig src/elab_env.sml src/elab_err.sig src/elab_err.sml src/elab_ops.sig src/elab_ops.sml src/elab_print.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/explify.sml tests/concat.ur tests/concat.urp
diffstat 18 files changed, 126 insertions(+), 67 deletions(-) [+]
line wrap: on
line diff
--- a/demo/crud.ur	Sun Oct 10 13:07:38 2010 -0400
+++ b/demo/crud.ur	Sun Oct 10 14:41:03 2010 -0400
@@ -78,7 +78,7 @@
 
           <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 @@
                 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>
--- a/demo/crud3.ur	Sun Oct 10 13:07:38 2010 -0400
+++ b/demo/crud3.ur	Sun Oct 10 14:41:03 2010 -0400
@@ -20,7 +20,7 @@
                                            <textbox{#B}/>
                                          </subform>
                                        </xml>),
-                                       Parse = (fn p => p.A ^ p.B),
+                                       Parse = (fn p : {A : string, B : string} => p.A ^ p.B),
                                        Inject = _
                                       }
                               }
--- a/demo/metaform.ur	Sun Oct 10 13:07:38 2010 -0400
+++ b/demo/metaform.ur	Sun Oct 10 14:41:03 2010 -0400
@@ -15,11 +15,10 @@
     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}/>
--- a/demo/view.ur	Sun Oct 10 13:07:38 2010 -0400
+++ b/demo/view.ur	Sun Oct 10 14:41:03 2010 -0400
@@ -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>
--- a/src/elab.sml	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab.sml	Sun Oct 10 14:41:03 2010 -0400
@@ -78,7 +78,7 @@
        | 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
 
--- a/src/elab_env.sig	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab_env.sig	Sun Oct 10 14:41:03 2010 -0400
@@ -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
--- a/src/elab_env.sml	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab_env.sml	Sun Oct 10 14:41:03 2010 -0400
@@ -43,8 +43,6 @@
 
 (* AST utility functions *)
 
-exception SynUnif
-
 val liftKindInKind =
     U.Kind.mapB {kind = fn bound => fn k =>
                                        case k of
@@ -78,13 +76,32 @@
                                              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 @@
                                              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 @@
     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 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 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 @@
     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 @@
 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 @@
                                                 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
--- a/src/elab_err.sig	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab_err.sig	Sun Oct 10 14:41:03 2010 -0400
@@ -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 @@
            | 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
 
--- a/src/elab_err.sml	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab_err.sml	Sun Oct 10 14:41:03 2010 -0400
@@ -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 @@
          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 @@
        | 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 @@
                            [("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
--- a/src/elab_ops.sig	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab_ops.sig	Sun Oct 10 14:41:03 2010 -0400
@@ -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
 
--- a/src/elab_ops.sml	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab_ops.sml	Sun Oct 10 14:41:03 2010 -0400
@@ -97,11 +97,13 @@
                                              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 @@
                                                  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 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 @@
                                           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 @@
                                       val c = (CApp (f, v), loc)
                                   in
                                       case unconstraint c of
-                                          (CUnif (_, _, _, vR'), _) =>
+                                          (CUnif (_, _, _, _, vR'), _) =>
                                           if vR' = vR then
                                               (inc identity;
                                                hnormCon env c2)
--- a/src/elab_print.sml	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab_print.sml	Sun Oct 10 14:41:03 2010 -0400
@@ -202,10 +202,13 @@
                              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,
--- a/src/elab_util.sig	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab_util.sig	Sun Oct 10 14:41:03 2010 -0400
@@ -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 @@
 
 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}
--- a/src/elab_util.sml	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab_util.sml	Sun Oct 10 14:41:03 2010 -0400
@@ -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 @@
 
 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 @@
                            (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) =>
--- a/src/elaborate.sml	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elaborate.sml	Sun Oct 10 14:41:03 2010 -0400
@@ -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)
-
-           | (L'.CUnif (_, _, _, r), _) =>
+             else if nl2 = 0 then
+                 (unifyKinds env k1 k2;
+                  r2 := SOME c2All)
+             else
+                 err (fn _ => TooLifty (loc1, loc2))
+
+           | (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 @@
                     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 @@
 
                     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 @@
             (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 @@
                   | 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 @@
                               (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
 
--- a/src/explify.sml	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/explify.sml	Sun Oct 10 14:41:03 2010 -0400
@@ -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 (_, _, _, 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)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/concat.ur	Sun Oct 10 14:41:03 2010 -0400
@@ -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)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/concat.urp	Sun Oct 10 14:41:03 2010 -0400
@@ -0,0 +1,1 @@
+concat