Demos compile again, with manual folders

14 files changed, 168 insertions, 115 deletions

diff --git a/demo/crud.ur b/demo/crud.ur
index b365f69b..a6a65bb3 100644
--- a/demo/crud.ur
+++ b/demo/crud.ur
@@ -33,6 +33,8 @@ fun bool name = {Nam = name,
 functor Make(M : sig
                  con cols :: {(Type * Type)}
                  constraint [Id] ~ cols
+                 val fl : folder cols
+
                  val tab : sql_table ([Id = int] ++ map fstTT cols)
 
                  val title : string
@@ -50,12 +52,12 @@ functor Make(M : sig
                        (fn (fs : {T : $([Id = int] ++ map fstTT M.cols)}) => <xml>
                          <tr>
                            <td>{[fs.T.Id]}</td>
-                           {foldT2RX2 [fstTT] [colMeta] [tr]
-                                      (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
-                                                       [[nm] ~ rest] v col => <xml>
-                                                         <td>{col.Show v}</td>
-                                                       </xml>)
-                                      [M.cols] (fs.T -- #Id) M.cols}
+                           {foldRX2 [fstTT] [colMeta] [tr]
+                                    (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+                                                     [[nm] ~ rest] v col => <xml>
+                                                       <td>{col.Show v}</td>
+                                                     </xml>)
+                                    [M.cols] M.fl (fs.T -- #Id) M.cols}
                            <td>
                              <a link={upd fs.T.Id}>[Update]</a>
                              <a link={confirm fs.T.Id}>[Delete]</a>
@@ -66,12 +68,12 @@ functor Make(M : sig
           <table border={1}>
             <tr>
               <th>ID</th>
-              {foldT2RX [colMeta] [tr]
+              {foldRX [colMeta] [tr]
                         (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
                                          [[nm] ~ rest] col => <xml>
                                            <th>{cdata col.Nam}</th>
                                          </xml>)
-                        [M.cols] M.cols}
+                        [M.cols] M.fl M.cols}
             </tr>
             {rows}
           </table>
@@ -79,14 +81,14 @@ functor Make(M : sig
           <br/><hr/><br/>
 
           <form>
-            {foldT2R [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map sndTT cols)]
-                     (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
-                                      [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map sndTT rest)) => <xml>
-                                        <li> {cdata col.Nam}: {col.Widget [nm]}</li>
-                                        {useMore acc}
-                                      </xml>)
+            {foldR [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map sndTT cols)]
+                   (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+                                    [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map sndTT rest)) => <xml>
+                                      <li> {cdata col.Nam}: {col.Widget [nm]}</li>
+                                      {useMore acc}
+                                    </xml>)
                      <xml/>
-                     [M.cols] M.cols}
+                     [M.cols] M.fl M.cols}
             
             <submit action={create}/>
           </form>
@@ -95,13 +97,13 @@ functor Make(M : sig
     and create (inputs : $(map sndTT M.cols)) =
         id <- nextval seq;
         dml (insert tab
-                    (foldT2R2 [sndTT] [colMeta]
-                              [fn cols => $(map (fn t :: (Type * Type) =>
-                                                       sql_exp [] [] [] t.1) cols)]
-                              (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
-                                               [[nm] ~ rest] =>
-                               fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)})
-                              {} [M.cols] inputs M.cols
+                    (foldR2 [sndTT] [colMeta]
+                            [fn cols => $(map (fn t :: (Type * Type) =>
+                                                  sql_exp [] [] [] t.1) cols)]
+                            (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+                                             [[nm] ~ rest] =>
+                             fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)})
+                            {} [M.cols] M.fl inputs M.cols
                      ++ {Id = (SQL {[id]})}));
         ls <- list ();
         return <xml><body>
@@ -113,17 +115,17 @@ functor Make(M : sig
     and upd (id : int) =
         let
             fun save (inputs : $(map sndTT M.cols)) =
-                dml (update [map fstTT M.cols]
-                            (foldT2R2 [sndTT] [colMeta]
-                                      [fn cols => $(map (fn t :: (Type * Type) =>
-                                                               sql_exp [T = [Id = int]
-                                                                                ++ map fstTT M.cols]
-                                                                       [] [] t.1) cols)]
-                                      (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
-                                                       [[nm] ~ rest] =>
-                                       fn input col acc => acc ++ {nm =
-                                                                   @sql_inject col.Inject (col.Parse input)})
-                                      {} [M.cols] inputs M.cols)
+                dml (update [map fstTT M.cols] !
+                            (foldR2 [sndTT] [colMeta]
+                                    [fn cols => $(map (fn t :: (Type * Type) =>
+                                                          sql_exp [T = [Id = int]
+                                                                           ++ map fstTT M.cols]
+                                                                  [] [] t.1) cols)]
+                                    (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+                                                     [[nm] ~ rest] =>
+                                     fn input col acc => acc ++ {nm =
+                                                                 @sql_inject col.Inject (col.Parse input)})
+                                    {} [M.cols] M.fl inputs M.cols)
                             tab (WHERE T.Id = {[id]}));
                 ls <- list ();
                 return <xml><body>
@@ -136,16 +138,16 @@ functor Make(M : sig
             case fso : (Basis.option {Tab : $(map fstTT M.cols)}) of
                 None => return <xml><body>Not found!</body></xml>
               | Some fs => return <xml><body><form>
-                {foldT2R2 [fstTT] [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map sndTT cols)]
-                          (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
-                                           [[nm] ~ rest] (v : t.1) (col : colMeta t)
-                                           (acc : xml form [] (map sndTT rest)) =>
-                              <xml>
-                                <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
-                                {useMore acc}
-                              </xml>)
-                          <xml/>
-                          [M.cols] fs.Tab M.cols}
+                {foldR2 [fstTT] [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map sndTT cols)]
+                        (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+                                         [[nm] ~ rest] (v : t.1) (col : colMeta t)
+                                         (acc : xml form [] (map sndTT rest)) =>
+                            <xml>
+                              <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
+                              {useMore acc}
+                            </xml>)
+                        <xml/>
+                        [M.cols] M.fl fs.Tab M.cols}
 
                 <submit action={save}/>
               </form></body></xml>
diff --git a/demo/crud.urs b/demo/crud.urs
index 8c9cebcf..b240b7c1 100644
--- a/demo/crud.urs
+++ b/demo/crud.urs
@@ -16,6 +16,8 @@ val bool : string -> colMeta (bool, bool)
 functor Make(M : sig
                  con cols :: {(Type * Type)}
                  constraint [Id] ~ cols
+                 val fl : folder cols
+
                  val tab : sql_table ([Id = int] ++ map fstTT cols)
 
                  val title : string
diff --git a/demo/crud1.ur b/demo/crud1.ur
index 3849e822..65140035 100644
--- a/demo/crud1.ur
+++ b/demo/crud1.ur
@@ -9,4 +9,10 @@ open Crud.Make(struct
                                B = Crud.string "B",
                                C = Crud.float "C",
                                D = Crud.bool "D"}
+
+                   val fl = Folder.cons [#A] [_] !
+                                        (Folder.cons [#B] [_] !
+                                                     (Folder.cons [#C] [_] !
+                                                                  (Folder.cons [#D] [_] !
+                                                                               Folder.nil)))
                end)
diff --git a/demo/crud2.ur b/demo/crud2.ur
index 1db376d4..f7adf29b 100644
--- a/demo/crud2.ur
+++ b/demo/crud2.ur
@@ -31,4 +31,8 @@ open Crud.Make(struct
                                         Inject = _
                                        }
                               }
+
+                   val fl = Folder.cons [#Nam] [_] !
+                                        (Folder.cons [#Ready] [_] !
+                                                     Folder.nil)
                end)
diff --git a/demo/metaform.ur b/demo/metaform.ur
index ae1197f4..0e2e5ee3 100644
--- a/demo/metaform.ur
+++ b/demo/metaform.ur
@@ -1,5 +1,6 @@
 functor Make (M : sig
                   con fs :: {Unit}
+                  val fl : folder fs
                   val names : $(mapUT string fs)
               end) = struct
 
@@ -8,7 +9,7 @@ functor Make (M : sig
        (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] name value => <xml>
          <li> {[name]} = {[value]}</li>
        </xml>)
-       [M.fs] M.names values}
+       [M.fs] M.fl M.names values}
     </body></xml>
 
     fun main () = return <xml><body>
@@ -20,7 +21,7 @@ functor Make (M : sig
                                    {useMore acc}
                                  </xml>)
                 <xml/>
-                [M.fs] M.names}
+                [M.fs] M.fl M.names}
         <submit action={handler}/>
       </form>
     </body></xml>
diff --git a/demo/metaform.urs b/demo/metaform.urs
index 7a3fa62e..505cb906 100644
--- a/demo/metaform.urs
+++ b/demo/metaform.urs
@@ -1,5 +1,6 @@
 functor Make (M : sig
                   con fs :: {Unit}
+                  val fl : folder fs
                   val names : $(mapUT string fs)
               end) : sig
     val main : unit -> transaction page
diff --git a/demo/metaform1.ur b/demo/metaform1.ur
index c6a4664d..2f3356fa 100644
--- a/demo/metaform1.ur
+++ b/demo/metaform1.ur
@@ -1,3 +1,4 @@
 open Metaform.Make(struct
                        val names = {A = "Tic", B = "Tac", C = "Toe"}
+                       val fl = Folder.cons [#A] [()] ! (Folder.cons [#B] [()] ! (Folder.cons [#C] [()] ! Folder.nil))
                    end)
diff --git a/demo/metaform2.ur b/demo/metaform2.ur
index 430a42f0..87d40b18 100644
--- a/demo/metaform2.ur
+++ b/demo/metaform2.ur
@@ -1,5 +1,6 @@
 structure MM = Metaform.Make(struct
                                  val names = {X = "x", Y = "y"}
+                                 val fl = Folder.cons [#X] [()] ! (Folder.cons [#Y] [()] ! Folder.nil)
                              end)
 
 fun diversion () = return <xml><body>
diff --git a/demo/sum.ur b/demo/sum.ur
index 87b2967a..62954e20 100644
--- a/demo/sum.ur
+++ b/demo/sum.ur
@@ -1,7 +1,7 @@
-fun sum (fs ::: {Unit}) (fold : folder fs) (x : $(mapUT int fs)) =
+fun sum (fs ::: {Unit}) (fl : folder fs) (x : $(mapUT int fs)) =
     foldUR [int] [fn _ => int]
     (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] n acc => n + acc)
-    0 [fs] fold x
+    0 [fs] fl x
 
 fun main () = return <xml><body>
   {[sum Folder.nil {}]}<br/>
diff --git a/demo/tcSum.ur b/demo/tcSum.ur
index 53679116..e3340021 100644
--- a/demo/tcSum.ur
+++ b/demo/tcSum.ur
@@ -1,9 +1,9 @@
-fun sum (t ::: Type) (_ : num t) (fs ::: {Unit}) (x : $(mapUT t fs)) =
+fun sum (t ::: Type) (_ : num t) (fs ::: {Unit}) (fl : folder fs) (x : $(mapUT t fs)) =
     foldUR [t] [fn _ => t]
     (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] n acc => n + acc)
-    zero [fs] x
+    zero [fs] fl x
 
 fun main () = return <xml><body>
-  {[sum {A = 0, B = 1}]}<br/>
-  {[sum {C = 2.1, D = 3.2, E = 4.3}]}
+  {[sum (Folder.cons [#A] [()] ! (Folder.cons [#B] [()] ! Folder.nil)) {A = 0, B = 1}]}<br/>
+  {[sum (Folder.cons [#D] [()] ! (Folder.cons [#C] [()] ! (Folder.cons [#E] [()] ! Folder.nil))) {C = 2.1, D = 3.2, E = 4.3}]}
 </body></xml>
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index bfee2dfb..48ee4dd0 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -74,7 +74,7 @@ fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
            (f : nm :: Name -> rest :: {Unit}
                 -> [[nm] ~ rest] =>
                       tf -> tr rest -> tr ([nm] ++ rest))
-           (i : tr []) (r ::: {Unit}) (fold : folder r)=
+           (i : tr []) (r :: {Unit}) (fold : folder r)=
     fold [fn r :: {Unit} => $(mapUT tf r) -> tr r]
          (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
                           [[nm] ~ rest] r =>
@@ -85,7 +85,7 @@ fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type)
            (f : nm :: Name -> rest :: {Unit}
                 -> [[nm] ~ rest] =>
                       tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
-           (i : tr []) (r ::: {Unit}) (fold : folder r) =
+           (i : tr []) (r :: {Unit}) (fold : folder r) =
     fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r]
          (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
                           [[nm] ~ rest] r1 r2 =>
@@ -105,7 +105,7 @@ fun foldR K (tf :: K -> Type) (tr :: {K} -> Type)
            (f : nm :: Name -> t :: K -> rest :: {K}
                 -> [[nm] ~ rest] =>
                       tf t -> tr rest -> tr ([nm = t] ++ rest))
-           (i : tr []) (r ::: {K}) (fold : folder r) =
+           (i : tr []) (r :: {K}) (fold : folder r) =
     fold [fn r :: {K} => $(map tf r) -> tr r]
              (fn (nm :: Name) (t :: K) (rest :: {K}) (acc : _ -> tr rest)
                               [[nm] ~ rest] r =>
@@ -116,7 +116,7 @@ fun foldR2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (tr :: {K} -> Type)
             (f : nm :: Name -> t :: K -> rest :: {K}
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-            (i : tr []) (r ::: {K}) (fold : folder r) =
+            (i : tr []) (r :: {K}) (fold : folder r) =
     fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
          (fn (nm :: Name) (t :: K) (rest :: {K})
                           (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
@@ -143,7 +143,7 @@ fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit})
            <xml/>
 
 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
-           (q : sql_query tables exps) [tables ~ exps]
+           [tables ~ exps] (q : sql_query tables exps)
            (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                 -> xml ctx [] []) =
     query q
@@ -151,7 +151,7 @@ fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
           <xml/>
 
 fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
-            (q : sql_query tables exps) [tables ~ exps]
+            [tables ~ exps] (q : sql_query tables exps)
             (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                  -> transaction (xml ctx [] [])) =
     query q
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index a9e5b6b3..65da4a07 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -46,25 +46,25 @@ val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
              -> (nm :: Name -> rest :: {Unit}
                  -> [[nm] ~ rest] =>
                        tf -> tr rest -> tr ([nm] ++ rest))
-             -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf r) -> tr r
+             -> tr [] -> r :: {Unit} -> folder r -> $(mapUT tf r) -> tr r
 
 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
              -> (nm :: Name -> rest :: {Unit}
                  -> [[nm] ~ rest] =>
                        tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
-             -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
+             -> tr [] -> r :: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
 
 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
               -> (nm :: Name -> rest :: {Unit}
                   -> [[nm] ~ rest] =>
                         tf1 -> tf2 -> xml ctx [] [])
-              -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
+              -> r :: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
 
 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
              -> (nm :: Name -> t :: K -> rest :: {K}
                  -> [[nm] ~ rest] =>
                        tf t -> tr rest -> tr ([nm = t] ++ rest))
-             -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
+             -> tr [] -> r :: {K} -> folder r -> $(map tf r) -> tr r
 
 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
              -> tr :: ({K} -> Type)
@@ -72,34 +72,34 @@ val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
              -> tr []
-             -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
+             -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
 
 val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit}
              -> (nm :: Name -> t :: K -> rest :: {K}
                  -> [[nm] ~ rest] =>
                        tf t -> xml ctx [] [])
-             -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
+             -> r :: {K} -> folder r -> $(map tf r) -> xml ctx [] []
 
 val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
               -> (nm :: Name -> t :: K -> rest :: {K}
                   -> [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> xml ctx [] [])
-              -> r ::: {K} -> folder r
+              -> r :: {K} -> folder r
               -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
 
 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
-             -> sql_query tables exps
              -> [tables ~ exps] =>
-                   ($(exps ++ map (fn fields :: {Type} => $fields) tables)
-                    -> xml ctx [] [])
-                   -> transaction (xml ctx [] [])
+             sql_query tables exps
+             -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
+                 -> xml ctx [] [])
+             -> transaction (xml ctx [] [])
 
 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
-              -> sql_query tables exps
               -> [tables ~ exps] =>
-                    ($(exps ++ map (fn fields :: {Type} => $fields) tables)
-                     -> transaction (xml ctx [] []))
-                    -> transaction (xml ctx [] [])
+              sql_query tables exps
+              -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
+                  -> transaction (xml ctx [] []))
+              -> transaction (xml ctx [] [])
                        
 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
                   -> [tables ~ exps] =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 201b9150..c88edd44 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -839,7 +839,7 @@
              in
                  unfold (r, c)
              end
-             handle _ => (TextIO.print "Guess failure!\n"; raise ex)
+             handle _ => raise ex
      in
          case (#1 c1, #1 c2) of
              (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>
@@ -874,7 +874,28 @@
                                   ("c2All", p_con env c2All)];*)
 
          case (c1, c2) of
-             (L'.CUnit, L'.CUnit) => ()
+             (L'.CError, _) => ()
+           | (_, L'.CError) => ()
+
+           | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
+             if r1 = r2 then
+                 ()
+             else
+                 (unifyKinds env k1 k2;
+                  r1 := SOME c2All)
+
+           | (L'.CUnif (_, _, _, r), _) =>
+             if occursCon r c2All then
+                 err COccursCheckFailed
+             else
+                 r := SOME c2All
+           | (_, L'.CUnif (_, _, _, r)) =>
+             if occursCon r c1All then
+                 err COccursCheckFailed
+             else
+                 r := SOME c1All
+
+           | (L'.CUnit, L'.CUnit) => ()
 
            | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
              (unifyCons' env d1 d2;
@@ -933,29 +954,63 @@
              ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
               handle ListPair.UnequalLengths => err CIncompatible)
 
-           | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) =>
-             unifyCons' env (L'.CProj (c1, n1), loc) c2All
-           | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) =>
-             unifyCons' env c1All (L'.CProj (c2, n2), loc)
-           | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) =>
+           | (L'.CProj (c1, n1), _) =>
              let
-                 val us = map (fn k => cunif (loc, k)) ks
-             in
-                 r := SOME (L'.CTuple us, loc);
-                 unifyCons' env (List.nth (us, n - 1)) c2All
-             end
-           | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) =>
-             let
-                 val us = map (fn k => cunif (loc, k)) ks
+                 fun trySnd () =
+                     case #1 (hnormCon env c2All) of
+                         L'.CProj (c2, n2) =>
+                         let
+                             fun tryNormal () =
+                                 if n1 = n2 then
+                                     unifyCons' env c1 c2
+                                 else
+                                     err CIncompatible
+                         in
+                             case #1 (hnormCon env c2) of
+                                 L'.CUnif (_, k, _, r) =>
+                                 (case #1 (hnormKind k) of
+                                      L'.KTuple ks =>
+                                      let
+                                          val loc = #2 c2
+                                          val us = map (fn k => cunif (loc, k)) ks
+                                      in
+                                          r := SOME (L'.CTuple us, loc);
+                                          unifyCons' env c1All (List.nth (us, n2 - 1))
+                                      end
+                                    | _ => tryNormal ())
+                            | _ => tryNormal ()
+                         end
+                       | _ => err CIncompatible
              in
-                 r := SOME (L'.CTuple us, loc);
-                 unifyCons' env c1All (List.nth (us, n - 1))
+                 case #1 (hnormCon env c1) of
+                     L'.CUnif (_, k, _, r) =>
+                     (case #1 (hnormKind k) of
+                          L'.KTuple ks =>
+                          let
+                              val loc = #2 c1
+                              val us = map (fn k => cunif (loc, k)) ks
+                          in
+                              r := SOME (L'.CTuple us, loc);
+                              unifyCons' env (List.nth (us, n1 - 1)) c2All
+                          end
+                        | _ => trySnd ())
+                   | _ => trySnd ()
              end
-           | (L'.CProj (c1, n1), L'.CProj (c2, n2)) =>
-             if n1 = n2 then
-                 unifyCons' env c1 c2
-             else
-                 err CIncompatible
+
+           | (_, L'.CProj (c2, n2)) =>
+             (case #1 (hnormCon env c2) of
+                  L'.CUnif (_, k, _, r) =>
+                  (case #1 (hnormKind k) of
+                       L'.KTuple ks =>
+                       let
+                           val loc = #2 c2
+                           val us = map (fn k => cunif (loc, k)) ks
+                       in
+                           r := SOME (L'.CTuple us, loc);
+                           unifyCons' env c1All (List.nth (us, n2 - 1))
+                       end
+                     | _ => err CIncompatible)
+                | _ => err CIncompatible)
 
            | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
              (unifyKinds env dom1 dom2;
@@ -969,32 +1024,11 @@
            | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
              unifyCons' (E.pushKRel env x) c1 c2
 
-           | (L'.CError, _) => ()
-           | (_, L'.CError) => ()
-
            | (L'.CRecord _, _) => isRecord ()
            | (_, L'.CRecord _) => isRecord ()
            | (L'.CConcat _, _) => isRecord ()
            | (_, L'.CConcat _) => isRecord ()
 
-           | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
-             if r1 = r2 then
-                 ()
-             else
-                 (unifyKinds env k1 k2;
-                  r1 := SOME c2All)
-
-           | (L'.CUnif (_, _, _, r), _) =>
-             if occursCon r c2All then
-                 err COccursCheckFailed
-             else
-                 r := SOME c2All
-           | (_, L'.CUnif (_, _, _, r)) =>
-             if occursCon r c1All then
-                 err COccursCheckFailed
-             else
-                 r := SOME c1All
-
            | _ => err CIncompatible
      end
 
diff --git a/src/urweb.grm b/src/urweb.grm
index 43c9947a..1cd3e5c9 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -961,6 +961,7 @@ eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))
 
                                              val e = (EVar (["Basis"], "update", Infer), loc)
                                              val e = (ECApp (e, (CWild (KRecord (KType, loc), loc), loc)), loc)
+                                             val e = (EDisjointApp e, loc)
                                              val e = (EApp (e, (ERecord fsets, loc)), loc)
                                              val e = (EApp (e, texp), loc)
                                          in