# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1286739434 14400
# Node ID f0afe61a6f8b296a4c68a8b07231d136647716da
# Parent  c7b9a33c26c8ca792b1b6da44b9710b3c7089d35
Tweaking unification fix to apply to demo/more

diff -r c7b9a33c26c8 -r f0afe61a6f8b demo/more/dbgrid.ur
--- a/demo/more/dbgrid.ur	Sun Oct 10 14:41:03 2010 -0400
+++ b/demo/more/dbgrid.ur	Sun Oct 10 15:37:14 2010 -0400
@@ -38,7 +38,7 @@
              NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
            | Nullable of metaBase (actual, input, filter)
 
-    con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) =>
+    con meta = fn global_actual_input_filter =>
                   {Initialize : transaction global_actual_input_filter.1,
                    Handlers : global_actual_input_filter.1
                               -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
@@ -48,25 +48,26 @@
     fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
                                                                                      (editableState ts) =
        let
-           fun doMr mr = {Header = name,
-                          Project = fn r => mr.Initialize r.nm,
-                          Update = fn r s =>
-                                      vo <- current (mr.Parse s);
-                                      return (case vo of
-                                                  None => r
-                                                | Some v => r -- nm ++ {nm = v}),
-                          Display = mr.Display,
-                          Edit = mr.Edit,
-                          Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo),
-                          CreateFilter = mr.CreateFilter,
-                          DisplayFilter = mr.DisplayFilter,
-                          Filter = fn i r => mr.Filter i r.nm,
-                          Sort = Some (fn r1 r2 => mr.Sort r1.nm r2.nm)} 
+           fun doMr (mr : metaBase (ts.2, ts.3, ts.4)) : colMeta' ([nm = ts.2] ++ rest) ts.3 ts.4 =
+               {Header = name,
+                Project = fn r => mr.Initialize r.nm,
+                Update = fn r s =>
+                            vo <- current (mr.Parse s);
+                            return (case vo of
+                                        None => r
+                                      | Some v => r -- nm ++ {nm = v}),
+                Display = mr.Display,
+                Edit = mr.Edit,
+                Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo),
+                CreateFilter = mr.CreateFilter,
+                DisplayFilter = mr.DisplayFilter,
+                Filter = fn i r => mr.Filter i r.nm,
+                Sort = Some (fn r1 r2 => mr.Sort r1.nm r2.nm)} 
        in
            {Initialize = m.Initialize,
             Handlers = fn data => case m.Handlers data of
-                                  NonNull (mr, _) => doMr mr
-                                | Nullable mr => doMr mr}
+                                      NonNull (mr, _) => doMr mr
+                                    | Nullable mr => doMr mr}
        end
         
     con readOnlyState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
diff -r c7b9a33c26c8 -r f0afe61a6f8b demo/more/dlist.ur
--- a/demo/more/dlist.ur	Sun Oct 10 14:41:03 2010 -0400
+++ b/demo/more/dlist.ur	Sun Oct 10 15:37:14 2010 -0400
@@ -119,7 +119,8 @@
                    end}/>
 </xml>
 
-fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter =
+fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] [])
+    : option int -> list (t * position) -> xml (ctx ++ body) [] [] =
     let
         fun renderFlat' len ls =
             case len of
@@ -233,13 +234,13 @@
                                  None => elems
                                | Some pos => skip pos elems
                      in
-                         return (renderFlat f r.Filter len elems)
+                         return (renderFlat f len elems)
                      end}/>
 </xml>
 
 fun delete pos = pos
 
-fun elements' [t] (dl'' : dlist'' t) =
+fun elements' [t] (dl'' : dlist'' t) : signal (list t) =
     case dl'' of
         Nil => return []
       | Cons (x, dl'') =>
@@ -247,13 +248,13 @@
         tl <- elements' dl'';
         return (x :: tl)
 
-fun elements [t] (dl : dlist t) =
+fun elements [t] (dl : dlist t) : signal (list t) =
     dl' <- signal dl;
     case dl' of
         Empty => return []
       | Nonempty {Head = hd, ...} => elements' hd
 
-fun size' [t] (dl'' : dlist'' t) =
+fun size' [t] (dl'' : dlist'' t) : signal int =
     case dl'' of
         Nil => return 0
       | Cons (x, dl'') =>
@@ -261,13 +262,13 @@
         n <- size' dl'';
         return (n + 1)
 
-fun size [t] (dl : dlist t) =
+fun size [t] (dl : dlist t) : signal int =
     dl' <- signal dl;
     case dl' of
         Empty => return 0
       | Nonempty {Head = hd, ...} => size' hd
 
-fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) =
+fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) : signal int =
     case dl'' of
         Nil => return 0
       | Cons (x, dl'') =>
@@ -276,7 +277,7 @@
         n <- numPassing' f dl'';
         return (if b then n + 1 else n)
 
-fun numPassing [t] (f : t -> signal bool) (dl : dlist t) =
+fun numPassing [t] (f : t -> signal bool) (dl : dlist t) : signal int =
     dl' <- signal dl;
     case dl' of
         Empty => return 0
diff -r c7b9a33c26c8 -r f0afe61a6f8b demo/more/grid.ur
--- a/demo/more/grid.ur	Sun Oct 10 14:41:03 2010 -0400
+++ b/demo/more/grid.ur	Sun Oct 10 15:37:14 2010 -0400
@@ -49,16 +49,18 @@
     fun make (row : M.row) [input] [filter] (m : colMeta' M.row input filter) : transaction input = m.Project row
 
     fun makeAll cols row = @@Monad.exec [transaction] _ [map snd3 M.cols]
-                               (@map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
-                                 (fn [p] data meta => make row(meta.Handlers data))
-                                 M.folder cols M.cols)
-                               (@@Folder.mp [_] [_] M.folder)
+                             (@map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
+                               (fn [p] data meta => make row (meta.Handlers data))
+                               M.folder cols M.cols)
+                             (@@Folder.mp [_] [_] M.folder)
+
+    type listT = {Row : source M.row,
+                  Cols : source ($(map snd3 M.cols)),
+                  Updating : source bool,
+                  Selected : source bool}
 
     type grid = {Cols : $(map fst3 M.cols),
-                 Rows : Dlist.dlist {Row : source M.row,
-                                     Cols : source ($(map snd3 M.cols)),
-                                     Updating : source bool,
-                                     Selected : source bool},
+                 Rows : Dlist.dlist listT,
                  Selection : source bool,
                  Filters : $(map thd3 M.cols),
                  Sort : source (option (M.row -> M.row -> bool)),
@@ -250,11 +252,12 @@
                                                     return (f r1 r2)) f)}
                       grid.Rows}
 
-            <dyn signal={rows <- Dlist.foldl (fn row => @Monad.mapR2 _ [aggregateMeta M.row] [id] [id]
-                                                         (fn [nm :: Name] [t :: Type] meta acc =>
-                                                             Monad.mp (fn v => meta.Step v acc)
-                                                                      (signal row.Row))
-                                                         M.aggFolder M.aggregates)
+            <dyn signal={rows <- Dlist.foldl (fn row : listT =>
+                                                 @Monad.mapR2 _ [aggregateMeta M.row] [id] [id]
+                                                  (fn [nm :: Name] [t :: Type] meta acc =>
+                                                      Monad.mp (fn v => meta.Step v acc)
+                                                               (signal row.Row))
+                                                  M.aggFolder M.aggregates)
                                  (@mp [aggregateMeta M.row] [id]
                                   (fn [t] meta => meta.Initial)
                                   M.aggFolder M.aggregates) grid.Rows;
diff -r c7b9a33c26c8 -r f0afe61a6f8b demo/more/grid0.ur
--- a/demo/more/grid0.ur	Sun Oct 10 14:41:03 2010 -0400
+++ b/demo/more/grid0.ur	Sun Oct 10 15:37:14 2010 -0400
@@ -13,8 +13,8 @@
                          A = {New = return 0,
                               Inj = _}}
 
-              val cols = {Id = Direct.readOnly [#Id] ! "Id" Direct.int,
-                          A = Direct.editable [#A] ! "A" Direct.int}
+              val cols = {Id = Direct.readOnly [#Id] "Id" Direct.int,
+                          A = Direct.editable [#A] "A" Direct.int}
 
               val aggregates = {}
 
diff -r c7b9a33c26c8 -r f0afe61a6f8b demo/more/orm.ur
--- a/demo/more/orm.ur	Sun Oct 10 14:41:03 2010 -0400
+++ b/demo/more/orm.ur	Sun Oct 10 15:37:14 2010 -0400
@@ -1,13 +1,14 @@
 con link = fn col_parent :: (Type * Type) => col_parent.1 -> transaction (option col_parent.2)
-fun noParent [t ::: Type] (_ : t) = return None
+fun noParent [t ::: Type] (_ : t) : transaction (option unit) = return None
 
 con meta = fn (col :: Type, parent :: Type) => {
 	      Link : link (col, parent),
 	      Inj : sql_injectable col
 	      }
 
-fun local [t :: Type] (inj : sql_injectable t) = {Link = noParent,
-                                                  Inj = inj}
+fun local [t :: Type] (inj : sql_injectable t) : meta (t, unit) =
+    {Link = noParent,
+     Inj = inj}
 
 functor Table(M : sig
                   con cols :: {(Type * Type)}
@@ -31,19 +32,19 @@
     val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}),
               Inj = inj}
 
-    fun ensql [avail] (r : row') : $(map (sql_exp avail [] []) fs') =
+    fun ensql [avail ::_] (r : row') : $(map (sql_exp avail [] []) fs') =
         @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1]
          (fn [ts] meta v => @sql_inject meta.Inj v)
          M.folder M.cols r
 
     fun create (r : row') =
         id <- nextval s;
-        dml (insert t ({Id = sql_inject id} ++ ensql r));
+        dml (insert t ({Id = sql_inject id} ++ ensql [[]] r));
         return ({Id = id} ++ r)
 
     fun delete r = dml (DELETE FROM t WHERE t.Id = {[r.Id]})
 
-    fun save r = dml (update [fs'] (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]}))
+    fun save r = dml (update [fs'] (ensql [[T = [Id = int] ++ map fst M.cols]] (r -- #Id)) t (WHERE T.Id = {[r.Id]}))
 
     fun lookup id =
         ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]});
diff -r c7b9a33c26c8 -r f0afe61a6f8b lib/ur/string.ur
--- a/lib/ur/string.ur	Sun Oct 10 14:41:03 2010 -0400
+++ b/lib/ur/string.ur	Sun Oct 10 15:37:14 2010 -0400
@@ -57,7 +57,7 @@
         mp' (length s - 1) ""
     end
 
-fun newlines [ctx] [[Body] ~ ctx] s : xml ([Body] ++ ctx) [] [] =
+fun newlines [ctx] [[Body] ~ ctx] (s : string) : xml ([Body] ++ ctx) [] [] =
     case split s #"\n" of
         None => cdata s
       | Some (s1, s2) => <xml>{[s1]}<br/>{newlines s2}</xml>
diff -r c7b9a33c26c8 -r f0afe61a6f8b src/elaborate.sml
--- a/src/elaborate.sml	Sun Oct 10 14:41:03 2010 -0400
+++ b/src/elaborate.sml	Sun Oct 10 15:37:14 2010 -0400
@@ -655,6 +655,24 @@
 
  val delayedExhaustives = ref ([] : (E.env * L'.con * L'.pat list * ErrorMsg.span) list)
 
+ exception CantSquish
+
+ fun squish by =
+     U.Con.mapB {kind = fn _ => fn k => k,
+                 con = fn bound => fn c =>
+                                      case c of
+                                          L'.CRel xn =>
+                                          if xn < bound then
+                                              c
+                                          else if bound <= xn andalso xn < bound + by then
+                                              raise CantSquish
+                                          else
+                                              L'.CRel (xn - by)
+                                        | L'.CUnif _ => raise CantSquish
+                                        | _ => c,
+                 bind = fn (bound, U.Con.RelC _) => bound + 1
+                         | (bound, _) => bound} 0
+
  fun unifyRecordCons env (loc, c1, c2) =
      let
          fun rkindof c =
@@ -1056,6 +1074,19 @@
              else
                  r := SOME c1All
 
+           | (L'.CUnif (nl, _, _, _, r), _) =>
+             if occursCon r c2All then
+                 err COccursCheckFailed
+             else
+                 (r := SOME (squish nl c2All)
+                  handle CantSquish => err CIncompatible)
+           | (_, L'.CUnif (nl, _, _, _, r)) =>
+             if occursCon r c1All then
+                 err COccursCheckFailed
+             else
+                 (r := SOME (squish nl c1All)
+                  handle CantSquish => err CIncompatible)
+
            | (L'.CUnit, L'.CUnit) => ()
 
            | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
@@ -1290,7 +1321,8 @@
                     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 env (nxs - i, u) t) t unifs
+                    val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i,
+                                                                              E.mliftConInCon (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);