Subquery expressions

5 files changed, 96 insertions, 86 deletions

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 98e620df..98390555 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -274,8 +274,8 @@ val check : fs ::: {Type}
 
 (*** Queries *)
 
-con sql_query :: {{Type}} -> {Type} -> Type
-con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
+con sql_query :: {{Type}} -> {{Type}} -> {Type} -> Type
+con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
 
 con sql_subset :: {{Type}} -> {{Type}} -> Type
 val sql_subset : keep_drop :: {({Type} * {Type})}
@@ -290,78 +290,82 @@ val sql_subset_concat : big1 ::: {{Type}} -> little1 ::: {{Type}}
     -> sql_subset big2 little2
     -> sql_subset (big1 ++ big2) (little1 ++ little2)
 
-con sql_from_items :: {{Type}} -> Type
+con sql_from_items :: {{Type}} -> {{Type}} -> Type
 
-val sql_from_table : t ::: Type -> fs ::: {Type}
+val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type}
                      -> fieldsOf t fs -> name :: Name
-                     -> t -> sql_from_items [name = fs]
-val sql_from_comma : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
+                     -> t -> sql_from_items free [name = fs]
+val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
                      -> [tabs1 ~ tabs2]
-    => sql_from_items tabs1 -> sql_from_items tabs2
-       -> sql_from_items (tabs1 ++ tabs2)
-val sql_inner_join : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
-                     -> [tabs1 ~ tabs2]
-    => sql_from_items tabs1 -> sql_from_items tabs2
-       -> sql_exp (tabs1 ++ tabs2) [] [] bool
-       -> sql_from_items (tabs1 ++ tabs2)
+    => sql_from_items free tabs1 -> sql_from_items free tabs2
+       -> sql_from_items free (tabs1 ++ tabs2)
+val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
+                     -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
+    => sql_from_items free tabs1 -> sql_from_items free tabs2
+       -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool
+       -> sql_from_items free (tabs1 ++ tabs2)
 
 class nullify :: Type -> Type -> Type
 val nullify_option : t ::: Type -> nullify (option t) (option t)
 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
 
-val sql_left_join : tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
-                     -> [tabs1 ~ tabs2]
+val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
+                     -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
     => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
-       -> sql_from_items tabs1 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2)
-       -> sql_exp (tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
-       -> sql_from_items (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
+       -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
+       -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
+       -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
 
-val sql_right_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
-                     -> [tabs1 ~ tabs2]
+val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
+                     -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
     => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
-       -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items tabs2
-       -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
-       -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
+       -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2
+       -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
+       -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
 
-val sql_full_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
-                     -> [tabs1 ~ tabs2]
+val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
+                     -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
     => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
-       -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1)
-       -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2)
-       -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
-       -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
+       -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1)
+       -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
+       -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
+       -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
 
-val sql_query1 : tables ::: {{Type}}
+val sql_query1 : free ::: {{Type}}
+                 -> tables ::: {{Type}}
                  -> grouped ::: {{Type}}
                  -> selectedFields ::: {{Type}}
                  -> selectedExps ::: {Type}
                  -> empties :: {Unit}
-                 -> [empties ~ selectedFields]
+                 -> [free ~ tables]
+                 => [free ~ grouped]
+                 => [empties ~ selectedFields]
                  => {Distinct : bool,
-                     From : sql_from_items tables,
-                     Where : sql_exp tables [] [] bool,
+                     From : sql_from_items free tables,
+                     Where : sql_exp (free ++ tables) [] [] bool,
                      GroupBy : sql_subset tables grouped,
-                     Having : sql_exp grouped tables [] bool,
+                     Having : sql_exp (free ++ grouped) tables [] bool,
                      SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
-                     SelectExps : $(map (sql_exp grouped tables [])
+                     SelectExps : $(map (sql_exp (free ++ grouped) tables [])
                                             selectedExps) }
-                 -> sql_query1 tables selectedFields selectedExps
+                 -> sql_query1 free tables selectedFields selectedExps
 
 type sql_relop 
 val sql_union : sql_relop
 val sql_intersect : sql_relop
 val sql_except : sql_relop
-val sql_relop : tables1 ::: {{Type}}
+val sql_relop : free ::: {{Type}}
+                -> tables1 ::: {{Type}}
                 -> tables2 ::: {{Type}}
                 -> selectedFields ::: {{Type}}
                 -> selectedExps ::: {Type}
                 -> sql_relop
-                -> sql_query1 tables1 selectedFields selectedExps
-                -> sql_query1 tables2 selectedFields selectedExps
-                -> sql_query1 [] selectedFields selectedExps
-val sql_forget_tables : tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
-                        -> sql_query1 tables selectedFields selectedExps
-                        -> sql_query1 [] selectedFields selectedExps
+                -> sql_query1 free tables1 selectedFields selectedExps
+                -> sql_query1 free tables2 selectedFields selectedExps
+                -> sql_query1 free [] selectedFields selectedExps
+val sql_forget_tables : free ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
+                        -> sql_query1 free tables selectedFields selectedExps
+                        -> sql_query1 free [] selectedFields selectedExps
 
 type sql_direction
 val sql_asc : sql_direction
@@ -382,14 +386,16 @@ type sql_offset
 val sql_no_offset : sql_offset
 val sql_offset : int -> sql_offset
 
-val sql_query : tables ::: {{Type}}
+val sql_query : free ::: {{Type}}
+                -> tables ::: {{Type}}
                 -> selectedFields ::: {{Type}}
                 -> selectedExps ::: {Type}
-                -> {Rows : sql_query1 tables selectedFields selectedExps,
-                    OrderBy : sql_order_by tables selectedExps,
+                -> [free ~ tables]
+                => {Rows : sql_query1 free tables selectedFields selectedExps,
+                    OrderBy : sql_order_by (free ++ tables) selectedExps,
                     Limit : sql_limit,
                     Offset : sql_offset}
-                -> sql_query selectedFields selectedExps
+                -> sql_query free selectedFields selectedExps
 
 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
                 -> fieldType ::: Type -> agg ::: {{Type}}
@@ -495,12 +501,16 @@ val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} ->
                    -> sql_exp tables agg exps t
                    -> sql_exp tables agg exps (option t)
 
+val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type
+                   -> sql_query tables [] [nm = t]
+                   -> sql_exp tables agg exps t
+
 (*** Executing queries *)
 
 val query : tables ::: {{Type}} -> exps ::: {Type}
             -> [tables ~ exps] =>
                   state ::: Type
-                  -> sql_query tables exps
+                  -> sql_query [] tables exps
                   -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                       -> state
                       -> transaction state)
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index bca5f4ba..bccbc82a 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -244,7 +244,7 @@ fun app [m] (_ : monad m) [a] f =
     end
 
 fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
-             [tables ~ exps] (q : sql_query tables exps)
+             [tables ~ exps] (q : sql_query [] tables exps)
              (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
     ls <- query q
                 (fn fs acc => return (f fs :: acc))
@@ -252,7 +252,7 @@ fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
     return (rev ls)
 
 fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
-             [tables ~ exps] (q : sql_query tables exps)
+             [tables ~ exps] (q : sql_query [] tables exps)
              (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) =
     ls <- query q
                 (fn fs acc => v <- f fs; return (v :: acc))
@@ -260,7 +260,7 @@ fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
     return (rev ls)
 
 fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
-             [tables ~ exps] (q : sql_query tables exps)
+             [tables ~ exps] (q : sql_query [] tables exps)
              (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) =
     ls <- query q
                 (fn fs acc => v <- f fs;
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index c5e41816..00c95053 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -51,19 +51,19 @@ val app : m ::: (Type -> Type) -> monad m -> a ::: Type
 
 val mapQuery : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
                -> [tables ~ exps] =>
-    sql_query tables exps
+    sql_query [] tables exps
     -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> t)
     -> transaction (list t)
 
 val mapQueryM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
                -> [tables ~ exps] =>
-    sql_query tables exps
+    sql_query [] tables exps
     -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t)
     -> transaction (list t)
 
 val mapQueryPartialM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
                -> [tables ~ exps] =>
-    sql_query tables exps
+    sql_query [] tables exps
     -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t))
     -> transaction (list t)
 
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 617423db..ae6cb74a 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -215,21 +215,21 @@ fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {
           <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
       <xml/>
 
-fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [t = fs] [])
+fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [t = fs] [])
            (f : $fs -> state -> transaction state) (i : state) =
     query q (fn r => f r.t) i
 
-fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [t = fs] [])
+fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [t = fs] [])
             (f : $fs -> state -> state) (i : state) =
     query q (fn r s => return (f r.t s)) i
 
-fun queryL [tables] [exps] [tables ~ exps] (q : sql_query tables exps) =
+fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] tables exps) =
     query q
     (fn r ls => return (r :: ls))
     []
 
 fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
-           [tables ~ exps] (q : sql_query tables exps)
+           [tables ~ exps] (q : sql_query [] tables exps)
            (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                 -> transaction unit) =
     query q
@@ -237,7 +237,7 @@ fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
           ()
 
 fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-           [tables ~ exps] (q : sql_query tables exps)
+           [tables ~ exps] (q : sql_query [] tables exps)
            (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                 -> xml ctx inp []) =
     query q
@@ -245,14 +245,14 @@ fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Ty
           <xml/>
 
 fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-            (q : sql_query [nm = fs] [])
+            (q : sql_query [] [nm = fs] [])
             (f : $fs -> xml ctx inp []) =
     query q
           (fn fs acc => return <xml>{acc}{f fs.nm}</xml>)
           <xml/>
 
 fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-            [tables ~ exps] (q : sql_query tables exps)
+            [tables ~ exps] (q : sql_query [] tables exps)
             (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                  -> transaction (xml ctx inp [])) =
     query q
@@ -262,7 +262,7 @@ fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {T
           <xml/>
 
 fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-             (q : sql_query [nm = fs] [])
+             (q : sql_query [] [nm = fs] [])
              (f : $fs -> transaction (xml ctx inp [])) =
     query q
           (fn fs acc =>
@@ -271,7 +271,7 @@ fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
           <xml/>
 
 fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-             (q : sql_query [] exps)
+             (q : sql_query [] [] exps)
              (f : $exps -> transaction (xml ctx inp [])) =
     query q
           (fn fs acc =>
@@ -281,42 +281,42 @@ fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
 
 fun hasRows [tables ::: {{Type}}] [exps ::: {Type}]
             [tables ~ exps]
-            (q : sql_query tables exps) =
+            (q : sql_query [] tables exps) =
     query q
           (fn _ _ => return True)
           False
 
 fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}]
                 [tables ~ exps]
-                (q : sql_query tables exps) =
+                (q : sql_query [] tables exps) =
     query q
           (fn fs _ => return (Some fs))
           None
 
-fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [nm = fs] []) =
+fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) =
     query q
           (fn fs _ => return (Some fs.nm))
           None
 
-fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query (mapU [] tabs) [nm = t]) =
+fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] (mapU [] tabs) [nm = t]) =
     query q
           (fn fs _ => return (Some fs.nm))
           None
 
 fun oneRow [tables ::: {{Type}}] [exps ::: {Type}]
-           [tables ~ exps] (q : sql_query tables exps) =
+           [tables ~ exps] (q : sql_query [] tables exps) =
     o <- oneOrNoRows q;
     return (case o of
                 None => error <xml>Query returned no rows</xml>
               | Some r => r)
 
-fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [nm = fs] []) =
+fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) =
     o <- oneOrNoRows q;
     return (case o of
                 None => error <xml>Query returned no rows</xml>
               | Some r => r.nm)
 
-fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query (mapU [] tabs) [nm = t]) =
+fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] (mapU [] tabs) [nm = t]) =
     o <- oneOrNoRows q;
     return (case o of
                 None => error <xml>Query returned no rows</xml>
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index 312f230a..7ddc6bee 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -126,91 +126,91 @@ val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
 
 val queryL : tables ::: {{Type}} -> exps ::: {Type}
              -> [tables ~ exps] =>
-                  sql_query tables exps
+                  sql_query [] tables exps
                   -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables))
 
 val query1 : t ::: Name -> fs ::: {Type} -> state ::: Type
-             -> sql_query [t = fs] []
+             -> sql_query [] [t = fs] []
              -> ($fs -> state -> transaction state)
              -> state
              -> transaction state
 
 val query1' : t ::: Name -> fs ::: {Type} -> state ::: Type
-              -> sql_query [t = fs] []
+              -> sql_query [] [t = fs] []
               -> ($fs -> state -> state)
               -> state
               -> transaction state
 
 val queryI : tables ::: {{Type}} -> exps ::: {Type}
              -> [tables ~ exps] =>
-             sql_query tables exps
+             sql_query [] tables exps
              -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                  -> transaction unit)
              -> transaction unit
 
 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
              -> [tables ~ exps] =>
-             sql_query tables exps
+             sql_query [] tables exps
              -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                  -> xml ctx inp [])
              -> transaction (xml ctx inp [])
 
 val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
-              -> sql_query [nm = fs] []
+              -> sql_query [] [nm = fs] []
               -> ($fs -> xml ctx inp [])
               -> transaction (xml ctx inp [])
 
 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
               -> [tables ~ exps] =>
-              sql_query tables exps
+              sql_query [] tables exps
               -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
                   -> transaction (xml ctx inp []))
               -> transaction (xml ctx inp [])
 val queryX1' : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
-              -> sql_query [nm = fs] []
+              -> sql_query [] [nm = fs] []
               -> ($fs -> transaction (xml ctx inp []))
               -> transaction (xml ctx inp [])
 val queryXE' : exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
-              -> sql_query [] exps
+              -> sql_query [] [] exps
               -> ($exps -> transaction (xml ctx inp []))
               -> transaction (xml ctx inp [])
 
 val hasRows : tables ::: {{Type}} -> exps ::: {Type}
               -> [tables ~ exps] =>
-    sql_query tables exps
+    sql_query [] tables exps
     -> transaction bool
 
 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
                   -> [tables ~ exps] =>
-                  sql_query tables exps
+                  sql_query [] tables exps
                   -> transaction
                          (option
                               $(exps
                                     ++ map (fn fields :: {Type} => $fields) tables))
 
 val oneOrNoRows1 : nm ::: Name -> fs ::: {Type}
-                   -> sql_query [nm = fs] []
+                   -> sql_query [] [nm = fs] []
                    -> transaction (option $fs)
 
 val oneOrNoRowsE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
                     -> [tabs ~ [nm]] =>
-    sql_query (mapU [] tabs) [nm = t]
+    sql_query [] (mapU [] tabs) [nm = t]
     -> transaction (option t)
 
 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
              -> [tables ~ exps] =>
-             sql_query tables exps
+             sql_query [] tables exps
              -> transaction
                     $(exps
                           ++ map (fn fields :: {Type} => $fields) tables)
 
 val oneRow1 : nm ::: Name -> fs ::: {Type}
-    -> sql_query [nm = fs] []
+    -> sql_query [] [nm = fs] []
     -> transaction $fs
 
 val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
                -> [tabs ~ [nm]] =>
-    sql_query (mapU [] tabs) [nm = t]
+    sql_query [] (mapU [] tabs) [nm = t]
     -> transaction t
 
 val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us