Make summary unification more conservative; infer implicit arguments after applications

20 files changed, 429 insertions, 381 deletions

diff --git a/CHANGELOG b/CHANGELOG
index d62e732a..16172985 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -2,6 +2,7 @@
 Next
 ========
 
+- Automatic insertion of implicit arguments in more positions
 - Reifying expressions as URLs and redirecting to them explicitly
 - More syntactic sugar for SQL
 - Typing of SQL queries no longer exposes which tables were used in joins but
diff --git a/demo/batchFun.ur b/demo/batchFun.ur
index c75cbb07..3f0317a8 100644
--- a/demo/batchFun.ur
+++ b/demo/batchFun.ur
@@ -45,14 +45,14 @@ functor Make(M : sig
 
     fun add r =
         dml (insert t
-                    (foldR2 [fst] [colMeta]
-                            [fn cols => $(map (fn t :: (Type * Type) =>
-                                                  sql_exp [] [] [] t.1) cols)]
-                            (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
-                                             [[nm] ~ rest] input col acc =>
-                                acc ++ {nm = @sql_inject col.Inject input})
-                            {} [M.cols] M.fl (r -- #Id) M.cols
-                            ++ {Id = (SQL {[r.Id]})}))
+                    (@foldR2 [fst] [colMeta]
+                      [fn cols => $(map (fn t :: (Type * Type) =>
+                                            sql_exp [] [] [] t.1) cols)]
+                      (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
+                                       [[nm] ~ rest] input col acc =>
+                          acc ++ {nm = @sql_inject col.Inject input})
+                      {} M.fl (r -- #Id) M.cols
+                      ++ {Id = (SQL {[r.Id]})}))
 
     fun doBatch ls =
         case ls of
@@ -72,11 +72,11 @@ functor Make(M : sig
                   | Cons (r, ls) => <xml>
                     <tr>
                       <td>{[r.Id]}</td>
-                      {foldRX2 [colMeta] [fst] [_]
-                               (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
-                                                [[nm] ~ rest] m v =>
-                                   <xml><td>{m.Show v}</td></xml>)
-                               [M.cols] M.fl M.cols (r -- #Id)}
+                      {@foldRX2 [colMeta] [fst] [_]
+                        (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
+                                         [[nm] ~ rest] m v =>
+                            <xml><td>{m.Show v}</td></xml>)
+                        M.fl M.cols (r -- #Id)}
                       {if withDel then
                            <xml><td><button value="Delete" onclick={rpc (del r.Id)}/></td></xml>
                        else
@@ -88,11 +88,11 @@ functor Make(M : sig
             <xml><dyn signal={ls <- signal lss; return <xml><table>
               <tr>
                 <th>Id</th>
-                {foldRX [colMeta] [_]
-                        (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
-                                         [[nm] ~ rest] m =>
-                            <xml><th>{[m.Nam]}</th></xml>)
-                        [M.cols] M.fl M.cols}
+                {@foldRX [colMeta] [_]
+                  (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
+                                   [[nm] ~ rest] m =>
+                      <xml><th>{[m.Nam]}</th></xml>)
+                  M.fl M.cols}
               </tr>
               {show' ls}
             </table></xml>}/></xml>
@@ -103,25 +103,25 @@ functor Make(M : sig
         batched <- source Nil;
 
         id <- source "";
-        inps <- foldR [colMeta] [fn r => transaction ($(map snd r))]
-                (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m acc =>
-                    s <- m.NewState;
-                    r <- acc;
-                    return ({nm = s} ++ r))
-                (return {})
-                [M.cols] M.fl M.cols;
-
+        inps <- @foldR [colMeta] [fn r => transaction ($(map snd r))]
+                 (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m acc =>
+                     s <- m.NewState;
+                     r <- acc;
+                     return ({nm = s} ++ r))
+                 (return {})
+                 M.fl M.cols;
+        
         let
             fun add () =
                 id <- get id;
-                vs <- foldR2 [colMeta] [snd] [fn r => transaction ($(map fst r))]
-                             (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
-                                              [[nm] ~ rest] m s acc =>
-                                 v <- m.ReadState s;
-                                 r <- acc;
-                                 return ({nm = v} ++ r))
-                             (return {})
-                             [M.cols] M.fl M.cols inps;
+                vs <- @foldR2 [colMeta] [snd] [fn r => transaction ($(map fst r))]
+                       (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
+                                        [[nm] ~ rest] m s acc =>
+                           v <- m.ReadState s;
+                           r <- acc;
+                           return ({nm = v} ++ r))
+                       (return {})
+                       M.fl M.cols inps;
                 ls <- get batched;
 
                 set batched (Cons ({Id = readError id} ++ vs, ls))
@@ -144,11 +144,11 @@ functor Make(M : sig
 
               <table>
                 <tr> <th>Id:</th> <td><ctextbox source={id}/></td> </tr>
-                {foldRX2 [colMeta] [snd] [_]
-                 (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
-                                  [[nm] ~ rest] m s =>
-                     <xml><tr> <th>{[m.Nam]}:</th> <td>{m.Widget s}</td> </tr></xml>)
-                 [M.cols] M.fl M.cols inps}
+                {@foldRX2 [colMeta] [snd] [_]
+                  (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
+                                   [[nm] ~ rest] m s =>
+                      <xml><tr> <th>{[m.Nam]}:</th> <td>{m.Widget s}</td> </tr></xml>)
+                  M.fl M.cols inps}
                 <tr> <th/> <td><button value="Batch it" onclick={add ()}/></td> </tr>
               </table>
 
diff --git a/demo/crud.ur b/demo/crud.ur
index 21c85d8f..bccc3822 100644
--- a/demo/crud.ur
+++ b/demo/crud.ur
@@ -50,12 +50,12 @@ functor Make(M : sig
                        (fn (fs : {T : $([Id = int] ++ map fst M.cols)}) => <xml>
                          <tr>
                            <td>{[fs.T.Id]}</td>
-                           {foldRX2 [fst] [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}
+                           {@foldRX2 [fst] [colMeta] [tr]
+                             (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
+                                              [[nm] ~ rest] v col => <xml>
+                                                <td>{col.Show v}</td>
+                                              </xml>)
+                             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 +66,12 @@ functor Make(M : sig
           <table border={1}>
             <tr>
               <th>ID</th>
-              {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.fl M.cols}
+              {@foldRX [colMeta] [tr]
+                (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
+                                 [[nm] ~ rest] col => <xml>
+                                   <th>{cdata col.Nam}</th>
+                                 </xml>)
+                M.fl M.cols}
             </tr>
             {rows}
           </table>
@@ -79,14 +79,14 @@ functor Make(M : sig
           <br/><hr/><br/>
 
           <form>
-            {foldR [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map snd cols)]
-                   (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
-                                    [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map snd rest)) => <xml>
-                                      <li> {cdata col.Nam}: {col.Widget [nm]}</li>
-                                      {useMore acc}
-                                    </xml>)
-                     <xml/>
-                     [M.cols] M.fl M.cols}
+            {@foldR [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map snd cols)]
+              (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
+                               [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map snd rest)) => <xml>
+                                 <li> {cdata col.Nam}: {col.Widget [nm]}</li>
+                                 {useMore acc}
+                               </xml>)
+              <xml/>
+              M.fl M.cols}
             
             <submit action={create}/>
           </form>
@@ -95,13 +95,13 @@ functor Make(M : sig
     and create (inputs : $(map snd M.cols)) =
         id <- nextval seq;
         dml (insert tab
-                    (foldR2 [snd] [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
+                    (@foldR2 [snd] [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.fl inputs M.cols
                      ++ {Id = (SQL {[id]})}));
         ls <- list ();
         return <xml><body>
@@ -113,17 +113,17 @@ functor Make(M : sig
     and upd (id : int) =
         let
             fun save (inputs : $(map snd M.cols)) =
-                dml (update [map fst M.cols] !
-                            (foldR2 [snd] [colMeta]
-                                    [fn cols => $(map (fn t :: (Type * Type) =>
-                                                          sql_exp [T = [Id = int]
-                                                                           ++ map fst 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)
+                dml (update [map fst M.cols]
+                            (@foldR2 [snd] [colMeta]
+                              [fn cols => $(map (fn t :: (Type * Type) =>
+                                                    sql_exp [T = [Id = int]
+                                                                     ++ map fst 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.fl inputs M.cols)
                             tab (WHERE T.Id = {[id]}));
                 ls <- list ();
                 return <xml><body>
@@ -136,16 +136,16 @@ functor Make(M : sig
             case fso : (Basis.option {Tab : $(map fst M.cols)}) of
                 None => return <xml><body>Not found!</body></xml>
               | Some fs => return <xml><body><form>
-                {foldR2 [fst] [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map snd cols)]
-                        (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
-                                         [[nm] ~ rest] (v : t.1) (col : colMeta t)
-                                         (acc : xml form [] (map snd rest)) =>
-                            <xml>
-                              <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
-                              {useMore acc}
-                            </xml>)
-                        <xml/>
-                        [M.cols] M.fl fs.Tab M.cols}
+                {@foldR2 [fst] [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map snd cols)]
+                  (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
+                                   [[nm] ~ rest] (v : t.1) (col : colMeta t)
+                                   (acc : xml form [] (map snd rest)) =>
+                      <xml>
+                        <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
+                        {useMore acc}
+                      </xml>)
+                  <xml/>
+                  M.fl fs.Tab M.cols}
 
                 <submit action={save}/>
               </form></body></xml>
diff --git a/demo/metaform.ur b/demo/metaform.ur
index 54bf0fc7..606b3863 100644
--- a/demo/metaform.ur
+++ b/demo/metaform.ur
@@ -5,23 +5,23 @@ functor Make (M : sig
               end) = struct
 
     fun handler values = return <xml><body>
-      {foldURX2 [string] [string] [body]
-       (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name value => <xml>
-         <li> {[name]} = {[value]}</li>
-       </xml>)
-       [M.fs] M.fl M.names values}
+      {@foldURX2 [string] [string] [body]
+        (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name value => <xml>
+          <li> {[name]} = {[value]}</li>
+        </xml>)
+        M.fl M.names values}
     </body></xml>
 
     fun main () = return <xml><body>
       <form>
-        {foldUR [string] [fn cols :: {Unit} => xml form [] (mapU string cols)]
-                (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name
-                                 (acc : xml form [] (mapU string rest)) => <xml>
-                                   <li> {[name]}: <textbox{nm}/></li>
-                                   {useMore acc}
-                                 </xml>)
-                <xml/>
-                [M.fs] M.fl M.names}
+        {@foldUR [string] [fn cols :: {Unit} => xml form [] (mapU string cols)]
+          (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name
+                           (acc : xml form [] (mapU string rest)) => <xml>
+                             <li> {[name]}: <textbox{nm}/></li>
+                             {useMore acc}
+                           </xml>)
+          <xml/>
+          M.fl M.names}
         <submit action={handler}/>
       </form>
     </body></xml>
diff --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur
index fe77f21b..b6cd94ae 100644
--- a/demo/more/dbgrid.ur
+++ b/demo/more/dbgrid.ur
@@ -384,31 +384,31 @@ functor Make(M : sig
                        val wholeRow = @Folder.concat ! M.keyFolder M.rowFolder
 
                        fun ensql [env] (r : $(M.key ++ M.row)) =
-                           map2 [rawMeta] [id] [sql_exp env [] []]
-                           (fn [t] meta v => @sql_inject meta.Inj v)
-                           [_] wholeRow M.raw r
+                           @map2 [rawMeta] [id] [sql_exp env [] []]
+                            (fn [t] meta v => @sql_inject meta.Inj v)
+                            wholeRow M.raw r
 
                        val new =
-                           row <- Monad.mapR [rawMeta] [id]
-                                              (fn [nm :: Name] [t :: Type] meta => meta.New)
-                                              [_] wholeRow M.raw;
+                           row <- @Monad.mapR _ [rawMeta] [id]
+                                   (fn [nm :: Name] [t :: Type] meta => meta.New)
+                                   wholeRow M.raw;
                            dml (insert M.tab (ensql row));
                            return row
 
                        fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] bool =
-                         foldR2 [rawMeta] [id]
-                                [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool]
-                                (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
-                                    (meta : rawMeta t) (v : t)
-                                    (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool)
-                                    [rest :: {Type}] [rest ~ [nm = t] ++ key] =>
-                                    (WHERE T.{nm} = {@sql_inject meta.Inj v} AND {exp [[nm = t] ++ rest] !}))
-                                (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
-                                [_] M.keyFolder (M.raw --- map rawMeta M.row) r
-                                [_] !
+                         @foldR2 [rawMeta] [id]
+                          [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool]
+                          (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
+                                           (meta : rawMeta t) (v : t)
+                                           (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool)
+                                           [rest :: {Type}] [rest ~ [nm = t] ++ key] =>
+                              (WHERE T.{nm} = {@sql_inject meta.Inj v} AND {exp [[nm = t] ++ rest] !}))
+                          (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
+                          M.keyFolder (M.raw --- map rawMeta M.row) r
+                          [_] !
 
                        fun save key row =
-                           dml (update [M.key ++ M.row] !
+                           dml (update [M.key ++ M.row]
                                        (ensql row)
                                        M.tab
                                        (selector key))
diff --git a/demo/more/grid.ur b/demo/more/grid.ur
index 170c6f2c..7540ca27 100644
--- a/demo/more/grid.ur
+++ b/demo/more/grid.ur
@@ -49,9 +49,9 @@ functor Make(M : sig
     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)
+                               (@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 grid = {Cols : $(map fst3 M.cols),
@@ -80,14 +80,14 @@ functor Make(M : sig
         Monad.ignore (Dlist.append rows r)
 
     val grid =
-        cols <- Monad.mapR [colMeta M.row] [fst3]
-                           (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize)
-                           [_] M.folder M.cols;
+        cols <- @Monad.mapR _ [colMeta M.row] [fst3]
+                 (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize)
+                 M.folder M.cols;
 
-        filters <- Monad.mapR2 [colMeta M.row] [fst3] [thd3]
-                               (fn [nm :: Name] [p :: (Type * Type * Type)] meta state =>
-                                   (meta.Handlers state).CreateFilter)
-                               [_] M.folder M.cols cols;
+        filters <- @Monad.mapR2 _ [colMeta M.row] [fst3] [thd3]
+                    (fn [nm :: Name] [p :: (Type * Type * Type)] meta state =>
+                        (meta.Handlers state).CreateFilter)
+                    M.folder M.cols cols;
 
         rows <- Dlist.create;
         sel <- source False;
@@ -109,30 +109,30 @@ functor Make(M : sig
 
     fun myFilter grid all =
         row <- signal all.Row;
-        foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]
-               (fn [nm :: Name] [p :: (Type * Type * Type)]
-                                [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
-                                meta state filter combinedFilter row =>
-                   previous <- combinedFilter row;
-                   this <- (meta.Handlers state).Filter filter row;
-                   return (previous && this))
-               (fn _ => return True)
-               [_] M.folder M.cols grid.Cols grid.Filters row
+        @foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]
+         (fn [nm :: Name] [p :: (Type * Type * Type)]
+                          [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
+                          meta state filter combinedFilter row =>
+             previous <- combinedFilter row;
+             this <- (meta.Handlers state).Filter filter row;
+             return (previous && this))
+         (fn _ => return True)
+         M.folder M.cols grid.Cols grid.Filters row
 
     fun render (grid : grid) = <xml>
       <table class={tabl}>
         <tr class={tr}>
           <th/> <th/> <th><button value="No sort" onclick={set grid.Sort None}/></th>
-          {foldRX2 [fst3] [colMeta M.row] [_]
-                   (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
-                                    data (meta : colMeta M.row p) =>
-                       <xml><th class={th}>
-                         {case (meta.Handlers data).Sort of
-                              None => txt (meta.Handlers data).Header
-                            | sort => <xml><button value={(meta.Handlers data).Header}
-                                                             onclick={set grid.Sort sort}/></xml>}
-                       </th></xml>)
-                   [_] M.folder grid.Cols M.cols}
+          {@foldRX2 [fst3] [colMeta M.row] [_]
+            (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
+                             data (meta : colMeta M.row p) =>
+                <xml><th class={th}>
+                  {case (meta.Handlers data).Sort of
+                       None => txt (meta.Handlers data).Header
+                     | sort => <xml><button value={(meta.Handlers data).Header}
+                                                      onclick={set grid.Sort sort}/></xml>}
+                </th></xml>)
+            M.folder grid.Cols M.cols}
         </tr>
 
         {Dlist.render (fn {Row = rowS, Cols = colsS, Updating = ud, Selected = sd} pos =>
@@ -152,18 +152,18 @@ functor Make(M : sig
                                   
                               val save =
                                   cols <- get colsS;
-                                  errors <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => option string]
-                                                         (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}]
-                                                                          [[nm] ~ rest] data meta v errors =>
-                                                             b <- current ((meta.Handlers data).Validate v);
-                                                             return (if b then
-                                                                         errors
-                                                                     else
-                                                                         case errors of
-                                                                             None => Some ((meta.Handlers data).Header)
-                                                                           | Some s => Some ((meta.Handlers data).Header
-                                                                                             ^ ", " ^ s)))
-                                                         None [_] M.folder grid.Cols M.cols cols;
+                                  errors <- @Monad.foldR3 _ [fst3] [colMeta M.row] [snd3] [fn _ => option string]
+                                             (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}]
+                                                              [[nm] ~ rest] data meta v errors =>
+                                                 b <- current ((meta.Handlers data).Validate v);
+                                                 return (if b then
+                                                             errors
+                                                         else
+                                                             case errors of
+                                                                 None => Some ((meta.Handlers data).Header)
+                                                               | Some s => Some ((meta.Handlers data).Header
+                                                                                 ^ ", " ^ s)))
+                                             None M.folder grid.Cols M.cols cols;
 
                                   case errors of
                                       Some s => alert ("Can't save because the following columns have invalid values:\n"
@@ -171,12 +171,12 @@ functor Make(M : sig
                                     | None =>
                                       set ud False;
                                       row <- get rowS;
-                                      row' <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => M.row]
-                                                           (fn [nm :: Name] [t :: (Type * Type * Type)]
-                                                                            [rest :: {(Type * Type * Type)}]
-                                                                            [[nm] ~ rest] data meta v row' =>
-                                                               (meta.Handlers data).Update row' v)
-                                                           row [_] M.folder grid.Cols M.cols cols;
+                                      row' <- @Monad.foldR3 _ [fst3] [colMeta M.row] [snd3] [fn _ => M.row]
+                                               (fn [nm :: Name] [t :: (Type * Type * Type)]
+                                                                [rest :: {(Type * Type * Type)}]
+                                                                [[nm] ~ rest] data meta v row' =>
+                                                   (meta.Handlers data).Update row' v)
+                                               row M.folder grid.Cols M.cols cols;
                                       rpc (M.save (M.keyOf row) row');
                                       set rowS row';
 
@@ -208,29 +208,29 @@ functor Make(M : sig
                                 </td>
 
                                 <dyn signal={cols <- signal colsS;
-                                             return (foldRX3 [fst3] [colMeta M.row] [snd3] [_]
-                                                             (fn [nm :: Name] [t :: (Type * Type * Type)]
-                                                                              [rest :: {(Type * Type * Type)}]
-                                                                              [[nm] ~ rest] data meta v =>
-                                                                 <xml><td class={td}>
-                                                                   <dyn signal={b <- signal ud;
-                                                                                return (if b then
-                                                                                            (meta.Handlers data).Edit v
-                                                                                        else
-                                                                                            (meta.Handlers data).Display
-                                                                                                                v)}/>
-                                                                   <dyn signal={b <- signal ud;
-                                                                                if b then
-                                                                                    valid <-
-                                                                                    (meta.Handlers data).Validate v;
-                                                                                    return (if valid then
-                                                                                                <xml/>
-                                                                                            else
-                                                                                                <xml>!</xml>)
-                                                                                else
-                                                                                    return <xml/>}/>
-                                                                 </td></xml>)
-                                                             [_] M.folder grid.Cols M.cols cols)}/>
+                                             return (@foldRX3 [fst3] [colMeta M.row] [snd3] [_]
+                                                      (fn [nm :: Name] [t :: (Type * Type * Type)]
+                                                                       [rest :: {(Type * Type * Type)}]
+                                                                       [[nm] ~ rest] data meta v =>
+                                                          <xml><td class={td}>
+                                                            <dyn signal={b <- signal ud;
+                                                                         return (if b then
+                                                                                     (meta.Handlers data).Edit v
+                                                                                 else
+                                                                                     (meta.Handlers data).Display
+                                                                                                         v)}/>
+                                                            <dyn signal={b <- signal ud;
+                                                                         if b then
+                                                                             valid <-
+                                                                             (meta.Handlers data).Validate v;
+                                                                             return (if valid then
+                                                                                         <xml/>
+                                                                                     else
+                                                                                         <xml>!</xml>)
+                                                                         else
+                                                                             return <xml/>}/>
+                                                          </td></xml>)
+                                                      M.folder grid.Cols M.cols cols)}/>
                                 </tr></xml>
                           end)
                       {StartPosition = case M.pageLength of
@@ -250,27 +250,27 @@ functor Make(M : sig
                                                     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)
-                                 (mp [aggregateMeta M.row] [id]
+            <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)
+                                 (@mp [aggregateMeta M.row] [id]
                                   (fn [t] meta => meta.Initial)
-                                  [_] M.aggFolder M.aggregates) grid.Rows;
+                                  M.aggFolder M.aggregates) grid.Rows;
                          return <xml><tr>
                            <th colspan={3}>Aggregates</th>
-                           {foldRX2 [aggregateMeta M.row] [id] [_]
-                                    (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc =>
-                                        <xml><td class={agg}>{meta.Display acc}</td></xml>)
-                                    [_] M.aggFolder M.aggregates rows}
+                           {@foldRX2 [aggregateMeta M.row] [id] [_]
+                             (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc =>
+                                 <xml><td class={agg}>{meta.Display acc}</td></xml>)
+                             M.aggFolder M.aggregates rows}
                          </tr></xml>}/>
 
               <tr><th colspan={3}>Filters</th>
-                {foldRX3 [colMeta M.row] [fst3] [thd3] [_]
-                 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
-                                  meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>)
-                 [_] M.folder M.cols grid.Cols grid.Filters}
+                {@foldRX3 [colMeta M.row] [fst3] [thd3] [_]
+                  (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
+                                   meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>)
+                  M.folder M.cols grid.Cols grid.Filters}
               </tr>
           </table>
 
diff --git a/demo/more/grid1.ur b/demo/more/grid1.ur
index 1eb5e596..2e58bdb7 100644
--- a/demo/more/grid1.ur
+++ b/demo/more/grid1.ur
@@ -35,13 +35,13 @@ open Make(struct
                                                fun render r = r.A
                                            end)
 
-              val cols = {Id = Direct.readOnly [#Id] ! "Id" Direct.int,
-                          A = Direct.editable [#A] ! "A" Direct.int,
-                          B = Direct.editable [#B] ! "B" Direct.string,
-                          C = Direct.editable [#C] ! "C" Direct.bool,
-                          D = Direct.editable [#D] ! "D" F.meta,
-                          E = Direct.editable [#E] ! "E" (Direct.nullable Direct.int),
-                          F = Direct.editable [#F] ! "F" (Direct.nullable F.meta),
+              val cols = {Id = Direct.readOnly [#Id] "Id" Direct.int,
+                          A = Direct.editable [#A] "A" Direct.int,
+                          B = Direct.editable [#B] "B" Direct.string,
+                          C = Direct.editable [#C] "C" Direct.bool,
+                          D = Direct.editable [#D] "D" F.meta,
+                          E = Direct.editable [#E] "E" (Direct.nullable Direct.int),
+                          F = Direct.editable [#F] "F" (Direct.nullable F.meta),
                           DA = computed "2A" (fn r => 2 * r.A),
                           Link = computedHtml "Link" (fn r => <xml><a link={page (r.A, r.B)}>Go</a></xml>)}
 
diff --git a/demo/more/orm.ur b/demo/more/orm.ur
index 620db9ad..d9f57f3b 100644
--- a/demo/more/orm.ur
+++ b/demo/more/orm.ur
@@ -32,9 +32,9 @@ functor Table(M : sig
               Inj = inj}
 
     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
+        @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;
@@ -43,7 +43,7 @@ functor Table(M : sig
 
     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 (r -- #Id)) t (WHERE T.Id = {[r.Id]}))
 
     fun lookup id =
         ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]});
@@ -59,20 +59,20 @@ functor Table(M : sig
                    {Col : {Exp : sql_exp [T = fs] [] [] col,
                            Inj : sql_injectable col},
                     Parent : $fs -> transaction (option parent)}
-    val cols = foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] =>
-                                $(map (meta' (map fst (before ++ after))) before)]
-               (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}]
-                                [[nm] ~ before] (meta : meta ts)
-                                (acc : after :: {(Type * Type)} -> [before ~ after] =>
-                                 $(map (meta' (map fst (before ++ after))) before))
-                                [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] =>
-                   {nm = {Col = {Exp = sql_field [#T] [nm],
-                                 Inj = meta.Inj},
-                          Parent = fn r => meta.Link r.nm}}
-                       ++ acc [[nm = ts] ++ after] !)
-               (fn [after :: {(Type * Type)}] [[] ~ after] => {})
-               [_] M.folder M.cols
-               [[Id = (id, row)]] !
+    val cols = @foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] =>
+                                 $(map (meta' (map fst (before ++ after))) before)]
+                (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}]
+                                 [[nm] ~ before] (meta : meta ts)
+                                 (acc : after :: {(Type * Type)} -> [before ~ after] =>
+                                  $(map (meta' (map fst (before ++ after))) before))
+                                 [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] =>
+                    {nm = {Col = {Exp = sql_field [#T] [nm],
+                                  Inj = meta.Inj},
+                           Parent = fn r => meta.Link r.nm}}
+                        ++ acc [[nm = ts] ++ after] !)
+                (fn [after :: {(Type * Type)}] [[] ~ after] => {})
+                M.folder M.cols
+                [[Id = (id, row)]] !
 
     type filter = sql_exp [T = fs] [] [] bool
     fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f})
@@ -80,12 +80,12 @@ functor Table(M : sig
 
     fun bin (b : t ::: Type -> sql_binary t t bool) [t] (c : col t) (v : t) =
         sql_binary b c.Exp (@sql_inject c.Inj v)
-    val eq = bin @@sql_eq
-    val ne = bin @@sql_ne
-    val lt = bin @@sql_lt
-    val le = bin @@sql_le
-    val gt = bin @@sql_gt
-    val ge = bin @@sql_ge
+    val eq = @@bin @@sql_eq
+    val ne = @@bin @@sql_ne
+    val lt = @@bin @@sql_lt
+    val le = @@bin @@sql_le
+    val gt = @@bin @@sql_gt
+    val ge = @@bin @@sql_ge
 
     fun bb (b : sql_binary bool bool bool) (f1 : filter) (f2 : filter) =
         sql_binary b f1 f2
diff --git a/demo/more/orm1.ur b/demo/more/orm1.ur
index bbbe2b00..b5ba29ac 100644
--- a/demo/more/orm1.ur
+++ b/demo/more/orm1.ur
@@ -1,13 +1,13 @@
 open Orm
 
 structure T = Table(struct
-                        val cols = {A = local [int] _,
-                                    B = local [string] _}
+                        val cols = {A = local [int],
+                                    B = local [string]}
                     end)
 
 structure S = Table(struct
                         val cols = {C = T.id,
-                                    D = local [float] _}
+                                    D = local [float]}
                     end)
 
 fun action () =
diff --git a/demo/more/versioned.ur b/demo/more/versioned.ur
index bc9911e3..8579559e 100644
--- a/demo/more/versioned.ur
+++ b/demo/more/versioned.ur
@@ -24,33 +24,33 @@ functor Make(M : sig
                          Eq : eq t}
 
     fun keyRecd (r : $(M.key ++ M.data)) =
-        map2 [sql_injectable] [id] [sql_exp [] [] []]
-             (fn [t] => @sql_inject)
-             [_] M.keyFolder M.key (r --- M.data)
+        @map2 [sql_injectable] [id] [sql_exp [] [] []]
+         (fn [t] => @sql_inject)
+         M.keyFolder M.key (r --- M.data)
 
     fun insert r =
         vr <- nextval s;
         dml (Basis.insert t
                           ({Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)}
                                ++ keyRecd r
-                               ++ map2 [dmeta] [id]
+                               ++ @map2 [dmeta] [id]
                                [fn t => sql_exp [] [] [] (option t)]
                                (fn [t] x v => @sql_inject (@sql_option_prim x.Inj)
                                                (Some v))
-                               [_] M.dataFolder M.data (r --- M.key)))
+                               M.dataFolder M.data (r --- M.key)))
 
     fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool =
-        foldR2 [sql_injectable] [id] [fn before => after :: {Type} -> [before ~ after]
-                                         => sql_exp [T = before ++ after] [] [] bool]
-               (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before]
-                                (inj : sql_injectable t) (v : t)
-                   (e : after :: {Type} -> [before ~ after]
-                    => sql_exp [T = before ++ after] [] [] bool)
-                   [after :: {Type}] [[nm = t] ++ before ~ after] =>
-                   (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !}))
-               (fn [after :: {Type}] [[] ~ after] => (SQL TRUE))
-               [_] M.keyFolder M.key r
-               [_] !
+        @foldR2 [sql_injectable] [id] [fn before => after :: {Type} -> [before ~ after]
+                                          => sql_exp [T = before ++ after] [] [] bool]
+         (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before]
+                          (inj : sql_injectable t) (v : t)
+                          (e : after :: {Type} -> [before ~ after]
+                           => sql_exp [T = before ++ after] [] [] bool)
+                          [after :: {Type}] [[nm = t] ++ before ~ after] =>
+             (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !}))
+         (fn [after :: {Type}] [[] ~ after] => (SQL TRUE))
+         M.keyFolder M.key r
+         [_] !
 
     datatype bound =
              NoBound
@@ -61,13 +61,13 @@ functor Make(M : sig
         let
             fun current' vro r =
                 let
-                    val complete = foldR [option] [fn ts => option $ts]
-                                   (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r]
-                                                    v r =>
-                                       case (v, r) of
-                                           (Some v, Some r) => Some ({nm = v} ++ r)
-                                         | _ => None)
-                                   (Some {}) [_] M.dataFolder r
+                    val complete = @foldR [option] [fn ts => option $ts]
+                                    (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r]
+                                                     v r =>
+                                        case (v, r) of
+                                            (Some v, Some r) => Some ({nm = v} ++ r)
+                                          | _ => None)
+                                    (Some {}) M.dataFolder r
                 in
                     case complete of
                         Some r => return (Some r)
@@ -88,19 +88,19 @@ functor Make(M : sig
                                 None => return None
                               | Some r' =>
                                 let
-                                    val r = map2 [option] [option] [option]
-                                            (fn [t ::: Type] old new =>
-                                                case old of
-                                                    None => new
-                                                  | Some _ => old)
-                                            [_] M.dataFolder r (r'.T -- #Version)
+                                    val r = @map2 [option] [option] [option]
+                                             (fn [t ::: Type] old new =>
+                                                 case old of
+                                                     None => new
+                                                   | Some _ => old)
+                                             M.dataFolder r (r'.T -- #Version)
                                 in
                                     current' (Lt r'.T.Version) r
                                 end
                         end
                 end
         in
-            current' vro (map0 [option] (fn [t :: Type] => None : option t) [_] M.dataFolder)
+            current' vro (@map0 [option] (fn [t :: Type] => None : option t) M.dataFolder)
         end
 
     val current = seek NoBound
@@ -113,14 +113,14 @@ functor Make(M : sig
           | Some cur =>
             vr <- nextval s;
             let
-                val r' = map3 [dmeta] [id] [id] [fn t => sql_exp [] [] [] (option t)]
-                              (fn [t] (meta : dmeta t) old new =>
-                                  @sql_inject (@sql_option_prim meta.Inj)
-                                   (if @@eq [_] meta.Eq old new then
-                                        None
-                                    else
-                                        Some new))
-                              [_] M.dataFolder M.data cur (r --- M.key)
+                val r' = @map3 [dmeta] [id] [id] [fn t => sql_exp [] [] [] (option t)]
+                          (fn [t] (meta : dmeta t) old new =>
+                              @sql_inject (@sql_option_prim meta.Inj)
+                               (if @@eq [_] meta.Eq old new then
+                                    None
+                                else
+                                    Some new))
+                          M.dataFolder M.data cur (r --- M.key)
                 val r' = {Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)}
                              ++ keyRecd r
                              ++ r'
diff --git a/demo/sum.ur b/demo/sum.ur
index 483cbf0a..c8d42887 100644
--- a/demo/sum.ur
+++ b/demo/sum.ur
@@ -1,7 +1,7 @@
 fun sum [fs ::: {Unit}] (fl : folder fs) (x : $(mapU int fs)) =
-    foldUR [int] [fn _ => int]
-    (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] n acc => n + acc)
-    0 [fs] fl x
+    @foldUR [int] [fn _ => int]
+     (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] n acc => n + acc)
+     0 fl x
 
 fun main () = return <xml><body>
   {[sum {}]}<br/>
diff --git a/demo/tcSum.ur b/demo/tcSum.ur
index 57e61c38..0026d506 100644
--- a/demo/tcSum.ur
+++ b/demo/tcSum.ur
@@ -1,7 +1,7 @@
 fun sum [t] (_ : num t) [fs ::: {Unit}] (fl : folder fs) (x : $(mapU t fs)) =
-    foldUR [t] [fn _ => t]
-    (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] n acc => n + acc)
-    zero [fs] fl x
+    @foldUR [t] [fn _ => t]
+     (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] n acc => n + acc)
+     zero fl x
 
 fun main () = return <xml><body>
   {[sum {A = 0, B = 1}]}<br/>
diff --git a/lib/ur/monad.ur b/lib/ur/monad.ur
index efba7546..e15da523 100644
--- a/lib/ur/monad.ur
+++ b/lib/ur/monad.ur
@@ -1,10 +1,10 @@
 fun exec [m ::: Type -> Type] (_ : monad m) [ts ::: {Type}] r (fd : folder ts) =
-    foldR [m] [fn ts => m $ts]
-    (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc =>
-        this <- action;
-        others <- acc;
-        return ({nm = this} ++ others))
-    (return {}) [ts] fd r
+    @foldR [m] [fn ts => m $ts]
+     (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc =>
+         this <- action;
+         others <- acc;
+         return ({nm = this} ++ others))
+     (return {}) fd r
 
 fun ignore [m ::: Type -> Type] (_ : monad m) [t] (v : m t) = x <- v; return ()
 
@@ -16,40 +16,40 @@ fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type]
           (f : nm :: Name -> t :: K -> rest :: {K}
                -> [[nm] ~ rest] =>
            tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
-          (i : tr []) [r :: {K}] (fl : folder r) =
-    Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
-             (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
-                              (acc : _ -> m (tr rest)) r =>
-                 acc' <- acc (r -- nm);
-                 f [nm] [t] [rest] ! r.nm acc')
-             (fn _ => return i)
-             [_] fl
+          (i : tr []) [r ::: {K}] (fl : folder r) =
+    @Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
+                      (acc : _ -> m (tr rest)) r =>
+         acc' <- acc (r -- nm);
+         f [nm] [t] [rest] ! r.nm acc')
+     (fn _ => return i)
+     fl
 
 fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
            (f : nm :: Name -> t :: K -> rest :: {K}
                 -> [[nm] ~ rest] =>
             tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
-           (i : tr []) [r :: {K}] (fl : folder r) =
-    Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
-       (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
-                        (acc : _ -> _ -> m (tr rest)) r1 r2 =>
-           acc' <- acc (r1 -- nm) (r2 -- nm);
-           f [nm] [t] [rest] ! r1.nm r2.nm acc')
-       (fn _ _ => return i)
-       [_] fl
+           (i : tr []) [r ::: {K}] (fl : folder r) =
+    @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
+                      (acc : _ -> _ -> m (tr rest)) r1 r2 =>
+         acc' <- acc (r1 -- nm) (r2 -- nm);
+         f [nm] [t] [rest] ! r1.nm r2.nm acc')
+     (fn _ _ => return i)
+     fl
 
 fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
            (f : nm :: Name -> t :: K -> rest :: {K}
                 -> [[nm] ~ rest] =>
             tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
-           (i : tr []) [r :: {K}] (fl : folder r) =
-    Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
-       (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
-                        (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
-           acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
-           f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc')
-       (fn _ _ _ => return i)
-       [_] fl
+           (i : tr []) [r ::: {K}] (fl : folder r) =
+    @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
+                      (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
+         acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
+         f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc')
+     (fn _ _ _ => return i)
+     fl
 
 fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type]
          (f : nm :: Name -> t :: K -> tf t -> m (tr t)) =
diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs
index 9ad9262d..698a4b5b 100644
--- a/lib/ur/monad.urs
+++ b/lib/ur/monad.urs
@@ -14,7 +14,7 @@ val foldR : K --> m ::: (Type -> Type) -> monad m
                 -> [[nm] ~ rest] =>
                 tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
             -> tr []
-            -> r :: {K} -> folder r -> $(map tf r) -> m (tr r)
+            -> r ::: {K} -> folder r -> $(map tf r) -> m (tr r)
 
 val foldR2 : K --> m ::: (Type -> Type) -> monad m
              -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
@@ -23,7 +23,7 @@ val foldR2 : K --> m ::: (Type -> Type) -> monad m
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
              -> tr []
-             -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r)
+             -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r)
 
 val foldR3 : K --> m ::: (Type -> Type) -> monad m
              -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
@@ -32,16 +32,16 @@ val foldR3 : K --> m ::: (Type -> Type) -> monad m
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
              -> tr []
-             -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
+             -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
 
 val mapR : K --> m ::: (Type -> Type) -> monad m
            -> tf :: (K -> Type)
            -> tr :: (K -> Type)
            -> (nm :: Name -> t :: K -> tf t -> m (tr t))
-           -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r))
+           -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tr r))
 
 val mapR2 : K --> m ::: (Type -> Type) -> monad m
             -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
             -> tr :: (K -> Type)
             -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t))
-            -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
+            -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index e4e33940..b6f6349a 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -9,7 +9,7 @@ con folder = K ==> fn r :: {K} =>
 fun fold [K] [tf :: {K} -> Type]
          (f : (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
                tf r -> tf ([nm = v] ++ r)))
-         (i : tf []) [r :: {K}] (fl : folder r) = fl [tf] f i
+         (i : tf []) [r ::: {K}] (fl : folder r) = fl [tf] f i
 
 structure Folder = struct
     fun nil [K] [tf :: {K} -> Type]
@@ -92,27 +92,27 @@ fun read_option [t ::: Type] (_ : read t) =
 fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) =
     cdata (show v)
 
-fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r :: {K}] (fl : folder r) =
+fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf r)]
     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc =>
         acc ++ {nm = f [t]})
     {}
 
-fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r :: {K}] (fl : folder r) =
+fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r)]
     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
         acc (r -- nm) ++ {nm = f r.nm})
     (fn _ => {})
 
 fun map2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type]
-         (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r :: {K}] (fl : folder r) =
+         (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r)]
     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
         acc (r1 -- nm) (r2 -- nm) ++ {nm = f r1.nm r2.nm})
     (fn _ _ => {})
 
 fun map3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tf :: K -> Type]
-         (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r :: {K}] (fl : folder r) =
+         (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)]
     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
         acc (r1 -- nm) (r2 -- nm) (r3 -- nm) ++ {nm = f r1.nm r2.nm r3.nm})
@@ -122,7 +122,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}] (fl : folder r) =
+           (i : tr []) [r ::: {Unit}] (fl : folder r) =
     fl [fn r :: {Unit} => $(mapU tf r) -> tr r]
        (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r =>
            f [nm] [rest] ! r.nm (acc (r -- nm)))
@@ -132,7 +132,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}] (fl : folder r) =
+           (i : tr []) [r ::: {Unit}] (fl : folder r) =
     fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r]
        (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r1 r2 =>
            f [nm] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
@@ -142,16 +142,16 @@ fun foldURX2 [tf1 :: Type] [tf2 :: Type] [ctx :: {Unit}]
            (f : nm :: Name -> rest :: {Unit}
                 -> [[nm] ~ rest] =>
                       tf1 -> tf2 -> xml ctx [] []) =
-    foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
-            (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
-                <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>)
-            <xml/>
+    @@foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+      (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
+          <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>)
+      <xml/>
 
 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}] (fl : folder r) =
+           (i : tr []) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf r) -> tr r]
        (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r =>
            f [nm] [t] [rest] ! r.nm (acc (r -- nm)))
@@ -161,7 +161,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}] (fl : folder r) =
+            (i : tr []) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
        (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
                         (acc : _ -> _ -> tr rest) r1 r2 =>
@@ -172,7 +172,7 @@ fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {
             (f : nm :: Name -> t :: K -> rest :: {K}
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
-            (i : tr []) [r :: {K}] (fl : folder r) =
+            (i : tr []) [r ::: {K}] (fl : folder r) =
     fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r]
        (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
                         (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 =>
@@ -183,30 +183,30 @@ fun foldRX [K] [tf :: K -> Type] [ctx :: {Unit}]
             (f : nm :: Name -> t :: K -> rest :: {K}
                  -> [[nm] ~ rest] =>
                        tf t -> xml ctx [] []) =
-    foldR [tf] [fn _ => xml ctx [] []]
-          (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
-              <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
-          <xml/>
+    @@foldR [tf] [fn _ => xml ctx [] []]
+      (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
+          <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
+      <xml/>
 
 fun foldRX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}]
              (f : nm :: Name -> t :: K -> rest :: {K}
                   -> [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> xml ctx [] []) =
-    foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
-           (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
-                            r1 r2 acc =>
-               <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
-           <xml/>
+    @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+      (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+                       r1 r2 acc =>
+          <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
+      <xml/>
 
 fun foldRX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}]
              (f : nm :: Name -> t :: K -> rest :: {K}
                   -> [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) =
-    foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
-           (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
-                            r1 r2 r3 acc =>
-               <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
-           <xml/>
+    @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
+      (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+                       r1 r2 r3 acc =>
+          <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
+      <xml/>
 
 fun queryL [tables] [exps] [tables ~ exps] (q : sql_query tables exps) =
     query q
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index 11547ace..d23b3e01 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -6,7 +6,7 @@ val fold : K --> tf :: ({K} -> Type)
            -> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
                tf r -> tf ([nm = v] ++ r))
            -> tf []
-           -> r :: {K} -> folder r -> tf r
+           -> r ::: {K} -> folder r -> tf r
 
 structure Folder : sig
     val nil : K --> folder (([]) :: {K})
@@ -47,40 +47,40 @@ val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
 
 val map0 : K --> tf :: (K -> Type)
            -> (t :: K -> tf t)
-           -> r :: {K} -> folder r -> $(map tf r)
+           -> r ::: {K} -> folder r -> $(map tf r)
 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
          -> (t ::: K -> tf1 t -> tf2 t)
-         -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
+         -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
 val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type)
            -> (t ::: K -> tf1 t -> tf2 t -> tf t)
-           -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
+           -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
 val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type)
            -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t)
-           -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
+           -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
 
 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
              -> (nm :: Name -> rest :: {Unit}
                  -> [[nm] ~ rest] =>
                        tf -> tr rest -> tr ([nm] ++ rest))
-             -> tr [] -> r :: {Unit} -> folder r -> $(mapU tf r) -> tr r
+             -> tr [] -> r ::: {Unit} -> folder r -> $(mapU 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 -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r
+             -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU 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 -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] []
+              -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU 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)
@@ -88,7 +88,7 @@ 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 foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
              -> tr :: ({K} -> Type)
@@ -96,26 +96,26 @@ val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type
                  -> [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
              -> tr []
-             -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
+             -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 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 foldRX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit}
               -> (nm :: Name -> t :: K -> rest :: {K}
                   -> [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> tf3 t -> xml ctx [] [])
-              -> r :: {K} -> folder r
+              -> r ::: {K} -> folder r
               -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] []
 
 val queryL : tables ::: {{Type}} -> exps ::: {Type}
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 2a237c50..f1ddd83e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -693,6 +693,13 @@
  and consNeq env (c1, c2) =
      case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of
          (L'.CName x1, L'.CName x2) => x1 <> x2
+       | (L'.CName _, L'.CRel _) => true
+       | (L'.CRel _, L'.CName _) => true
+       | (L'.CRel n1, L'.CRel n2) => n1 <> n2
+       | (L'.CRel _, L'.CNamed _) => true
+       | (L'.CNamed _, L'.CRel _) => true
+       | (L'.CRel _, L'.CModProj _) => true
+       | (L'.CModProj _, L'.CRel _) => true
        | _ => false
 
  and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =
@@ -1619,6 +1626,34 @@ fun normClassConstraint env (c, loc) =
       | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c
       | _ => unmodCon env (c, loc)
 
+fun findHead e e' =
+    let
+        fun findHead (e, _) =
+            case e of
+                L.EVar (_, _, infer) =>
+                let
+                    fun findHead' (e, _) =
+                        case e of
+                            L'.ENamed _ => true
+                          | L'.EModProj _ => true
+                          | L'.EApp (e, _) => findHead' e
+                          | L'.ECApp (e, _) => findHead' e
+                          | L'.EKApp (e, _) => findHead' e
+                          | _ => false
+                in
+                    if findHead' e' then
+                        SOME infer
+                    else
+                        NONE
+                end
+              | L.EApp (e, _) => findHead e
+              | L.ECApp (e, _) => findHead e
+              | L.EDisjointApp e => findHead e
+              | _ => NONE
+    in
+        findHead e
+    end
+
 fun elabExp (env, denv) (eAll as (e, loc)) =
     let
         (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
@@ -1674,15 +1709,23 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
           | L.EApp (e1, e2) =>
             let
                 val (e1', t1, gs1) = elabExp (env, denv) e1
+
                 val (e2', t2, gs2) = elabExp (env, denv) e2
 
                 val dom = cunif (loc, ktype)
                 val ran = cunif (loc, ktype)
                 val t = (L'.TFun (dom, ran), loc)
+
+                val () = checkCon env e1' t1 t
+                val () = checkCon env e2' t2 dom
+
+                val ef = (L'.EApp (e1', e2'), loc)
+                val (ef, et, gs3) =
+                    case findHead e1 e1' of
+                        NONE => (ef, ran, [])
+                      | SOME infer => elabHead (env, denv) infer ef ran
             in
-                checkCon env e1' t1 t;
-                checkCon env e2' t2 dom;
-                ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2)
+                (ef, et, gs1 @ gs2 @ gs3)
             end
           | L.EAbs (x, to, e) =>
             let
@@ -1705,6 +1748,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
           | L.ECApp (e, c) =>
             let
                 val (e', et, gs1) = elabExp (env, denv) e
+
                 val oldEt = et
                 val (c', ck, gs2) = elabCon (env, denv) c
                 val (et', _) = hnormCon env et
@@ -1717,6 +1761,12 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                         val eb' = subConInCon (0, c') eb
                             handle SynUnif => (expError env (Unif ("substitution", loc, eb));
                                                cerror)
+
+                        val ef = (L'.ECApp (e', c'), loc)
+                        val (ef, eb', gs3) =
+                            case findHead e e' of
+                                NONE => (ef, eb', [])
+                              | SOME infer => elabHead (env, denv) infer ef eb'
                     in
                         (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll),
                                                ("et", p_con env oldEt),
@@ -1724,7 +1774,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                                                ("eb", p_con (E.pushCRel env x k) eb),
                                                ("c", p_con env c'),
                                                ("eb'", p_con env eb')];*)
-                        ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2)
+                        (ef, eb', gs1 @ enD gs2 @ gs3)
                     end
 
                   | _ =>
diff --git a/src/urweb.grm b/src/urweb.grm
index 00c39b52..93ff7321 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -540,9 +540,8 @@ cst    : UNIQUE tnames                  (let
                                              val e = (EVar (["Basis"], "unique", Infer), loc)
                                              val e = (ECApp (e, #1 (#1 tnames)), loc)
                                              val e = (ECApp (e, (CRecord (#2 tnames), loc)), loc)
-                                             val e = (EDisjointApp e, loc)
                                          in
-                                             (EDisjointApp e, loc)
+                                             e
                                          end)
 
        | CHECK sqlexp                   (let
@@ -562,9 +561,6 @@ cst    : UNIQUE tnames                  (let
                                                                val e = (EVar (["Basis"], "mat_cons", Infer), loc)
                                                                val e = (ECApp (e, nm1), loc)
                                                                val e = (ECApp (e, nm2), loc)
-                                                               val e = (EDisjointApp e, loc)
-                                                               val e = (EDisjointApp e, loc)
-                                                               val e = (EApp (e, (EWild, loc)), loc)
                                                            in
                                                                (EApp (e, mat), loc)
                                                            end)
@@ -634,7 +630,7 @@ pkopt  :                                (EVar (["Basis"], "no_primary_key", Infe
        | PRIMARY KEY tnames             (let
                                              val loc = s (PRIMARYleft, tnamesright)
 
-                                             val e = (EVar (["Basis"], "primary_key", Infer), loc)
+                                             val e = (EVar (["Basis"], "primary_key", TypesOnly), loc)
                                              val e = (ECApp (e, #1 (#1 tnames)), loc)
                                              val e = (ECApp (e, (CRecord (#2 tnames), loc)), loc)
                                              val e = (EDisjointApp e, loc)
@@ -1192,7 +1188,6 @@ 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
@@ -1335,11 +1330,8 @@ xmlOne : NOTAGS                         (EApp ((EVar (["Basis"], "cdata", Infer)
                                                  if et = "form" then
                                                      (EApp ((EVar (["Basis"], "form", Infer), pos),
                                                             xmlOpt), pos)
-                                                 else if et = "subform" then
-                                                     (EApp ((EDisjointApp (#2 (#1 tag)), pos),
-                                                            xmlOpt), pos)
-                                                 else if et = "subforms" then
-                                                     (EApp ((EDisjointApp (#2 (#1 tag)), pos),
+                                                 else if et = "subform" orelse et = "subforms" then
+                                                     (EApp (#2 (#1 tag),
                                                             xmlOpt), pos)
                                                  else if et = "entry" then
                                                      (EApp ((EVar (["Basis"], "entry", Infer), pos),
@@ -1504,7 +1496,6 @@ query1 : SELECT dopt select FROM tables wopt gopt hopt
                                              val e = (EVar (["Basis"], "sql_query1", Infer), loc)
                                              val e = (ECApp (e, (CRecord (map (fn nm => (nm, (CUnit, loc))) empties),
                                                                  loc)), loc)
-                                             val e = (EDisjointApp e, loc)
                                              val re = (ERecord [((CName "Distinct", loc),
                                                                  dopt),
                                                                 ((CName "From", loc),
diff --git a/tests/impl.ur b/tests/impl.ur
index 5304598c..4a2e7a09 100644
--- a/tests/impl.ur
+++ b/tests/impl.ur
@@ -1,15 +1,18 @@
-val id = fn t :: Type => fn x : t => x
+fun id [t :: Type] (x : t) = x
 val id_self = id [t :: Type -> t -> t] id
 
-val idi = fn t ::: Type => fn x : t => x
-val idi_self = idi idi
+fun idi [t ::: Type] (x : t) = x
+val idi_self = idi @@idi
 
-val picker = fn na :: Name => fn a ::: Type => fn nb :: Name => fn b ::: Type => fn fs ::: {Type} =>
-        fn r : $([na = a, nb = b] ++ fs) => {na = r.na, nb = r.nb}
+fun picker [na :: Name] [a ::: Type] [nb :: Name] [b ::: Type] [fs ::: {Type}] [[na] ~ [nb]] [[na, nb] ~ fs]
+        (r : $([na = a, nb = b] ++ fs)) = {na = r.na, nb = r.nb}
 val getem = picker [#A] [#C] {A = 0, B = 1.0, C = "hi", D = {}}
 val getem2 = picker [#A] [_] {A = 0, B = 1.0, C = "hi", D = {}}
 val getem3 = picker [#A] [_::Name] {A = 0, B = 1.0, C = "hi", D = {}}
 
-val picker_ohmy = fn na ::: Name => fn a ::: Type => fn nb ::: Name => fn b ::: Type => fn fs ::: {Type} =>
-        fn r : $([na = a, nb = b] ++ fs) => {na = r.na, nb = r.nb}
+fun picker_ohmy [na ::: Name] [a ::: Type] [nb ::: Name] [b ::: Type] [fs ::: {Type}] [[na] ~ [nb]] [[na, nb] ~ fs]
+        (r : $([na = a, nb = b] ++ fs)) = {na = r.na, nb = r.nb}
 val getem_ohmy = picker_ohmy {A = 0, B = 1.0, C = "hi", D = {}}
+
+fun proj [fs] [t] [nm :: Name] [[nm] ~ fs] (r : $([nm = t] ++ fs)) = r.nm
+val one = proj [#A] {A = 1, B = True}
diff --git a/tests/impl.urp b/tests/impl.urp
new file mode 100644
index 00000000..0ca72e15
--- /dev/null
+++ b/tests/impl.urp
@@ -0,0 +1,3 @@
+debug
+
+impl