Lighter-weight encoding of window function use

15 files changed, 417 insertions, 394 deletions

diff --git a/demo/batchFun.ur b/demo/batchFun.ur
index 69a68423..d69d68af 100644
--- a/demo/batchFun.ur
+++ b/demo/batchFun.ur
@@ -46,7 +46,7 @@ functor Make(M : sig
     fun add r =
         dml (insert t
                     (@foldR2 [fst] [colMeta]
-                      [fn cols => $(map (fn t => sql_exp [] [] [] disallow_window t.1) cols)]
+                      [fn cols => $(map (fn t => sql_exp [] [] [] t.1) cols)]
                       (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] input col acc =>
                           acc ++ {nm = @sql_inject col.Inject input})
                       {} M.fl (r -- #Id) M.cols
diff --git a/demo/crud.ur b/demo/crud.ur
index 0222e30f..4d2753ea 100644
--- a/demo/crud.ur
+++ b/demo/crud.ur
@@ -93,7 +93,7 @@ functor Make(M : sig
         id <- nextval seq;
         dml (insert tab
                     (@foldR2 [snd] [colMeta]
-                      [fn cols => $(map (fn t => sql_exp [] [] [] disallow_window t.1) cols)]
+                      [fn cols => $(map (fn t => sql_exp [] [] [] t.1) cols)]
                       (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] =>
                        fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)})
                       {} M.fl inputs M.cols
@@ -110,7 +110,7 @@ functor Make(M : sig
             fun save (inputs : $(map snd M.cols)) =
                 dml (update [map fst M.cols]
                             (@foldR2 [snd] [colMeta]
-                              [fn cols => $(map (fn t => sql_exp [T = [Id = int] ++ map fst M.cols] [] [] disallow_window t.1) cols)]
+                              [fn cols => $(map (fn t => sql_exp [T = [Id = int] ++ map fst M.cols] [] [] t.1) cols)]
                               (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] =>
                                fn input col acc => acc ++ {nm =
                                                            @sql_inject col.Inject (col.Parse input)})
diff --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur
index 13092db6..fc593533 100644
--- a/demo/more/dbgrid.ur
+++ b/demo/more/dbgrid.ur
@@ -385,7 +385,7 @@ functor Make(M : sig
                        val wholeRow = @Folder.concat ! M.keyFolder M.rowFolder
 
                        fun ensql [env] (r : $(M.key ++ M.row)) =
-                           @map2 [rawMeta] [ident] [sql_exp env [] [] disallow_window]
+                           @map2 [rawMeta] [ident] [sql_exp env [] []]
                             (fn [t] meta v => @sql_inject meta.Inj v)
                             wholeRow M.raw r
 
@@ -396,12 +396,12 @@ functor Make(M : sig
                            dml (insert M.tab (ensql row));
                            return row
 
-                       fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] disallow_window bool =
+                       fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] bool =
                          @foldR2 [rawMeta] [ident]
-                          [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] disallow_window bool]
+                          [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] [] [] disallow_window bool)
+                                           (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))
diff --git a/demo/more/orm.ur b/demo/more/orm.ur
index 2e1fc2e0..468281f7 100644
--- a/demo/more/orm.ur
+++ b/demo/more/orm.ur
@@ -32,8 +32,8 @@ functor Table(M : sig
     val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}),
               Inj = inj}
 
-    fun ensql [avail ::_] (r : row') : $(map (sql_exp avail [] [] disallow_window) fs') =
-        @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] disallow_window ts.1]
+    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
 
@@ -53,11 +53,11 @@ functor Table(M : sig
 
     val list = resultsOut (SELECT * FROM t)
 
-    con col = fn t => {Exp : sql_exp [T = fs] [] [] disallow_window t,
+    con col = fn t => {Exp : sql_exp [T = fs] [] [] t,
                        Inj : sql_injectable t}
     val idCol = {Exp = sql_field [#T] [#Id], Inj = _}
     con meta' = fn (fs :: {Type}) (col :: Type, parent :: Type) =>
-                   {Col : {Exp : sql_exp [T = fs] [] [] disallow_window col,
+                   {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] =>
@@ -75,7 +75,7 @@ functor Table(M : sig
                 M.folder M.cols
                 [[Id = (id, row)]] !
 
-    type filter = sql_exp [T = fs] [] [] disallow_window bool
+    type filter = sql_exp [T = fs] [] [] bool
     fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f})
     fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f})
 
diff --git a/demo/more/versioned.ur b/demo/more/versioned.ur
index 5da8704c..d08ebcb0 100644
--- a/demo/more/versioned.ur
+++ b/demo/more/versioned.ur
@@ -24,7 +24,7 @@ functor Make(M : sig
                          Eq : eq t}
 
     fun keyRecd (r : $(M.key ++ M.data)) =
-        @map2 [sql_injectable] [ident] [sql_exp [] [] [] disallow_window]
+        @map2 [sql_injectable] [ident] [sql_exp [] [] []]
          (fn [t] => @sql_inject)
          M.keyFolder M.key (r --- M.data)
 
@@ -34,18 +34,18 @@ functor Make(M : sig
                           ({Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)}
                                ++ keyRecd r
                                ++ @map2 [dmeta] [ident]
-                               [fn t => sql_exp [] [] [] disallow_window (option t)]
+                               [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)))
 
-    fun keyExp (r : $M.key) : sql_exp [T = all] [] [] disallow_window bool =
+    fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool =
         @foldR2 [sql_injectable] [ident] [fn before => after :: {Type} -> [before ~ after]
-                                          => sql_exp [T = before ++ after] [] [] disallow_window bool]
+                                          => 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] [] [] disallow_window bool)
+                           => 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))
@@ -113,7 +113,7 @@ functor Make(M : sig
           | Some cur =>
             vr <- nextval s;
             let
-                val r' = @map3 [dmeta] [ident] [ident] [fn t => sql_exp [] [] [] disallow_window (option t)]
+                val r' = @map3 [dmeta] [ident] [ident] [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
diff --git a/doc/manual.tex b/doc/manual.tex
index 7f8b01c2..589177dd 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1595,7 +1595,7 @@ $$\begin{array}{l}
 
 The last kind of constraint is a \texttt{CHECK} constraint, which attaches a boolean invariant over a row's contents.  It is defined using the $\mt{sql\_exp}$ type family, which we discuss in more detail below.
 $$\begin{array}{l}
-  \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{disallow\_window} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; []
+  \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; []
 \end{array}$$
 
 Section \ref{tables} shows the expanded syntax of the $\mt{table}$ declaration and signature item that includes constraints.  There is no other way to use constraints with SQL in Ur/Web.
@@ -1662,11 +1662,11 @@ $$\begin{array}{l}
   \hspace{.1in} \Rightarrow [\mt{empties} \sim \mt{selectedFields}] \\
   \hspace{.1in} \Rightarrow \{\mt{Distinct} : \mt{bool}, \\
   \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{free} \; \mt{tables}, \\
-  \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; \mt{afree} \; [] \; \mt{disallow\_window} \; \mt{bool}, \\
+  \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; \mt{afree} \; [] \; \mt{bool}, \\
   \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\
-  \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{disallow\_window} \; \mt{bool}, \\
+  \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{bool}, \\
   \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\
-  \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{allow\_window}) \; \mt{selectedExps}) \} \\
+  \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_expw} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; []) \; \mt{selectedExps}) \} \\
   \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}
 \end{array}$$
 
@@ -1680,26 +1680,24 @@ $$\begin{array}{l}
 \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables}
 \end{array}$$
 
-SQL expressions are used in several places, including $\mt{SELECT}$, $\mt{WHERE}$, $\mt{HAVING}$, and $\mt{ORDER} \; \mt{BY}$ clauses.  They reify a fragment of the standard SQL expression language, while making it possible to inject ``native'' Ur values in some places.  The arguments to the $\mt{sql\_exp}$ type family respectively give the unrestricted-availability table fields, the table fields that may only be used in arguments to aggregate functions, the available selected expressions, whether window functions are allowed, and the type of the expression.  Two abstract constructors are declared to use to specify window function allowedness.
+SQL expressions are used in several places, including $\mt{SELECT}$, $\mt{WHERE}$, $\mt{HAVING}$, and $\mt{ORDER} \; \mt{BY}$ clauses.  They reify a fragment of the standard SQL expression language, while making it possible to inject ``native'' Ur values in some places.  The arguments to the $\mt{sql\_exp}$ type family respectively give the unrestricted-availability table fields, the table fields that may only be used in arguments to aggregate functions, the available selected expressions, and the type of the expression.
 $$\begin{array}{l}
-  \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \{\mt{Unit}\} \to \mt{Type} \\
-  \mt{con} \; \mt{disallow\_window} :: \{\mt{Unit}\} \\
-  \mt{con} \; \mt{allow\_window} :: \{\mt{Unit}\}
+  \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}
 \end{array}$$
 
 Any field in scope may be converted to an expression.
 $$\begin{array}{l}
   \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\
-  \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\
+  \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\
   \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\
   \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\
-  \hspace{.1in} \to \mt{sql\_exp} \; ([\mt{tab} = [\mt{field} = \mt{fieldType}] \rc \mt{otherFields}] \rc \mt{otherTabs}) \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{fieldType}
+  \hspace{.1in} \to \mt{sql\_exp} \; ([\mt{tab} = [\mt{field} = \mt{fieldType}] \rc \mt{otherFields}] \rc \mt{otherTabs}) \; \mt{agg} \; \mt{exps} \; \mt{fieldType}
 \end{array}$$
 
 There is an analogous function for referencing named expressions.
 $$\begin{array}{l}
-  \mt{val} \; \mt{sql\_exp} : \mt{tabs} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \to \mt{rest} ::: \{\mt{Type}\} \to \mt{nm} :: \mt{Name} \\
-  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{aw} \; \mt{t}
+  \mt{val} \; \mt{sql\_exp} : \mt{tabs} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{t} ::: \mt{Type} \to \mt{rest} ::: \{\mt{Type}\} \to \mt{nm} :: \mt{Name} \\
+  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t}
 \end{array}$$
 
 Ur values of appropriate types may be injected into SQL expressions.
@@ -1718,8 +1716,8 @@ $$\begin{array}{l}
   \mt{val} \; \mt{sql\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; \mt{t} \\
   \mt{val} \; \mt{sql\_option\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; (\mt{option} \; \mt{t}) \\
   \\
-  \mt{val} \; \mt{sql\_inject} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\
-  \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t}
+  \mt{val} \; \mt{sql\_inject} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\
+  \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
 \end{array}$$
 
 Additionally, most function-free types may be injected safely, via the $\mt{serialized}$ type family.
@@ -1732,44 +1730,39 @@ $$\begin{array}{l}
 
 We have the SQL nullness test, which is necessary because of the strange SQL semantics of equality in the presence of null values.
 $$\begin{array}{l}
-  \mt{val} \; \mt{sql\_is\_null} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\
-  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{aw} \; \mt{t}) \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{bool}
+  \mt{val} \; \mt{sql\_is\_null} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{t}) \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool}
 \end{array}$$
 
 As another way of dealing with null values, there is also a restricted form of the standard \cd{COALESCE} function.
 $$\begin{array}{l}
   \mt{val} \; \mt{sql\_coalesce} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\
-  \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\
-  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; (\mt{option} \; \mt{t}) \\
-  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\
-  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t}
+  \hspace{.1in} \to \mt{t} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{t}) \\
+  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
 \end{array}$$
 
 We have generic nullary, unary, and binary operators.
 $$\begin{array}{l}
   \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\
   \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\
-  \mt{val} \; \mt{sql\_nfunc} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\
-  \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t}
-\end{array}$$
+  \mt{val} \; \mt{sql\_nfunc} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$
 
 $$\begin{array}{l}
   \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
   \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\
-  \mt{val} \; \mt{sql\_unary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{arg} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\
-  \hspace{.1in} \to \mt{sql\_unary} \; \mt{arg} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{res}
+  \mt{val} \; \mt{sql\_unary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{arg} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_unary} \; \mt{arg} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{res} \\
 \end{array}$$
 
 $$\begin{array}{l}
   \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\
   \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
   \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
-  \mt{val} \; \mt{sql\_binary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\
-  \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{arg_1} ::: \mt{Type} \to \mt{arg_2} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\
-  \hspace{.1in} \to \mt{sql\_binary} \; \mt{arg_1} \; \mt{arg_2} \; \mt{res} \\
-  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg_1} \\
-  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg_2} \\
-  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{res}
+  \mt{val} \; \mt{sql\_binary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{arg_1} ::: \mt{Type} \to \mt{arg_2} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_binary} \; \mt{arg_1} \; \mt{arg_2} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg_1} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg_2} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{res}
 \end{array}$$
 
 $$\begin{array}{l}
@@ -1786,13 +1779,13 @@ $$\begin{array}{l}
 
 Finally, we have aggregate functions.  The $\mt{COUNT(\ast)}$ syntax is handled specially, since it takes no real argument.  The other aggregate functions are placed into a general type family, using constructor classes to restrict usage to properly-typed arguments.  The key aspect of the $\mt{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields.
 $$\begin{array}{l}
-  \mt{val} \; \mt{sql\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \mt{aw} ::: \{\mt{Unit}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{int}
+  \mt{val} \; \mt{sql\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int}
 \end{array}$$
 
 $$\begin{array}{l}
   \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
-  \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Type}\} \mt{dom} ::: \mt{Type} \to \mt{ran} ::: \mt{Type} \\
-  \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{dom} \; \mt{ran} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{dom} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{ran}
+  \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{dom} ::: \mt{Type} \to \mt{ran} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{dom} \; \mt{ran} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{dom} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{ran}
 \end{array}$$
 
 $$\begin{array}{l}
@@ -1819,43 +1812,20 @@ $$\begin{array}{l}
   \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt}
 \end{array}$$
 
-There is a fancier class of aggregates called \emph{window functions}, defined in the SQL standard but currently only supported by Postgres, among the DBMSes that Ur/Web supports.  Here are the type family and associated combinator for creating a window function expression:
-
-$$\begin{array}{l}
-\mt{con} \; \mt{sql\_window} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} \\
-\mt{val} \; \mt{sql\_window} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\
-\hspace{.1in} \to \mt{t} ::: \mt{Type} \\
-\hspace{.1in} \to \mt{sql\_window} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
-\hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} \\
-\hspace{.1in} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\
-\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{allow\_window} \; \mt{t}
-\end{array}$$
-
-The function argument for an SQL \cd{PARTITION BY} clause uses the following type family and combinators:
-$$\begin{array}{l}
-\mt{con} \; \mt{sql\_partition} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
-\mt{val} \; \mt{sql\_no\_partition} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\
-\hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} \\
-\mt{val} \; \mt{sql\_partition} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
-\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{disallow\_window} \; \mt{t} \\
-\hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps}
-\end{array}$$
-
 Any SQL query that returns single columns may be turned into a subquery expression.
 
 $$\begin{array}{l}
-\mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \\
-\hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\
-\hspace{.1in} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{nt}
+\mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\
+\hspace{.1in} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{nt}
 \end{array}$$
 
 There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions.
 $$\begin{array}{l}
-\mt{val} \; \mt{sql\_if\_then\_else} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\
-\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{bool} \\
-\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\
-\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\
-\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t}
+\mt{val} \; \mt{sql\_if\_then\_else} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
+\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool} \\
+\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
 \end{array}$$
 
 \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause.
@@ -1870,7 +1840,7 @@ $$\begin{array}{l}
   \mt{val} \; \mt{sql\_inner\_join} : \mt{free} ::: \{\{\mt{Type}\}\} \to \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \\
   \hspace{.1in} \to [\mt{free} \sim \mt{tabs1}] \Rightarrow [\mt{free} \sim \mt{tabs2}] \Rightarrow [\mt{tabs1} \sim \mt{tabs2}] \\
   \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs2} \\
-  \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \\
+  \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{bool} \\
   \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{tabs2})
 \end{array}$$
 
@@ -1888,7 +1858,7 @@ $$\begin{array}{l}
   \hspace{.1in} \to [\mt{free} \sim \mt{tabs1}] \Rightarrow [\mt{free} \sim \mt{tabs2}] \Rightarrow [\mt{tabs1} \sim \mt{tabs2}] \\
  \hspace{.1in} \Rightarrow \$(\mt{map} \; (\lambda \mt{r} \Rightarrow \$(\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{nullify} \; \mt{p}.1 \; \mt{p}.2) \; \mt{r})) \; \mt{tabs2}) \\
  \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \\
- \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \\
+ \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \; [] \; [] \; \mt{bool} \\
  \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.2)) \; \mt{tabs2})
 \end{array}$$
 
@@ -1900,8 +1870,9 @@ $$\begin{array}{l}
   \\
   \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
   \mt{val} \; \mt{sql\_order\_by\_Nil} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} :: \{\mt{Type}\} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\
-  \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
-  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; [] \; \mt{exps} \; \mt{allow\_window} \; \mt{t} \to \mt{sql\_direction} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\
+  \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tf} ::: (\{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}) \\
+  \hspace{.1in} \to \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_window} \; \mt{tf} \to \mt{tf} \; \mt{tables} \; [] \; \mt{exps} \; \mt{t} \to \mt{sql\_direction} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\
   \mt{val} \; \mt{sql\_order\_by\_random} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\
   \\
   \mt{type} \; \mt{sql\_limit} \\
@@ -1913,6 +1884,45 @@ $$\begin{array}{l}
   \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset}
 \end{array}$$
 
+When using Postgres, \cd{SELECT} and \cd{ORDER BY} are allowed to contain top-level uses of \emph{window functions}.  A separate type family \cd{sql\_expw} is provided for such cases, with some type class convenience for overloading between normal and window expressions.
+$$\begin{array}{l}
+  \mt{con} \; \mt{sql\_expw} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} \\
+  \\
+  \mt{class} \; \mt{sql\_window} :: (\{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}) \to \mt{Type} \\
+  \mt{val} \; \mt{sql\_window\_normal} : \mt{sql\_window} \; \mt{sql\_exp} \\
+  \mt{val} \; \mt{sql\_window\_fancy} : \mt{sql\_window} \; \mt{sql\_expw} \\
+  \mt{val} \; \mt{sql\_window} : \mt{tf} ::: (\{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}) \\
+  \hspace{.1in} \to \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_window} \; \mt{tf} \\
+  \hspace{.1in} \to \mt{tf} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+  \hspace{.1in} \to \mt{sql\_expw} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+  \\
+  \mt{con} \; \mt{sql\_partition} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
+  \mt{val} \; \mt{sql\_no\_partition} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\
+  \hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} \\
+  \mt{val} \; \mt{sql\_partition} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+  \hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} \\
+  \\
+  \mt{con} \; \mt{sql\_window\_function} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} \\
+  \mt{val} \; \mt{sql\_window\_function} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\
+  \hspace{.1in} \to \mt{t} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_window\_function} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+  \hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} \\
+  \hspace{.1in} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\
+  \hspace{.1in} \to \mt{sql\_expw} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+  \\
+  \mt{val} \; \mt{sql\_window\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\
+  \hspace{.1in} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\
+  \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt} \\
+  \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
+  \hspace{.1in} \to \mt{sql\_window\_function} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{nt} \\
+  \mt{val} \; \mt{sql\_window\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\
+  \hspace{.1in} \to \mt{sql\_window\_function} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int} \\
+  \mt{val} \; \mt{sql\_rank} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\
+  \hspace{.1in} \to \mt{sql\_window\_function} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int}
+\end{array}$$
+
 
 \subsubsection{DML}
 
@@ -1932,19 +1942,19 @@ $$\begin{array}{l}
 Properly-typed records may be used to form $\mt{INSERT}$ commands.
 $$\begin{array}{l}
   \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
-  \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; [] \; \mt{disallow\_window}) \; \mt{fields}) \to \mt{dml}
+  \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml}
 \end{array}$$
 
 An $\mt{UPDATE}$ command is formed from a choice of which table fields to leave alone and which to change, along with an expression to use to compute the new value of each changed field and a $\mt{WHERE}$ clause.  Note that, in the table environment applied to expressions, the table being updated is hardcoded at the name $\mt{T}$.  The parsing extension for $\mt{UPDATE}$ will elaborate all table-free field references to use table variable $\mt{T}$.
 $$\begin{array}{l}
   \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to [\mt{changed} \sim \mt{unchanged}] \\
-  \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{disallow\_window}) \; \mt{changed}) \\
-  \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \to \mt{dml}
+  \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\
+  \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{bool} \to \mt{dml}
 \end{array}$$
 
 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause.  The above use of $\mt{T}$ is repeated.
 $$\begin{array}{l}
-  \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \to \mt{dml}
+  \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{bool} \to \mt{dml}
 \end{array}$$
 
 \subsubsection{Sequences}
@@ -2188,7 +2198,7 @@ $$\begin{array}{rrcll}
   \textrm{Pre-queries} & q &::=& \mt{SELECT} \; [\mt{DISTINCT}] \; P \; \mt{FROM} \; F,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\
   &&& \mid q \; R \; q \mid \{\{\{e\}\}\} \\
   \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT} \\
-  \textrm{$\mt{ORDER \; BY}$ items} & O &::=& \mt{RANDOM} [()] \mid E \; [o] \mid E \; [o], O
+  \textrm{$\mt{ORDER \; BY}$ items} & O &::=& \mt{RANDOM} [()] \mid \hat{E} \; [o] \mid \hat{E} \; [o], O
 \end{array}$$
 
 $$\begin{array}{rrcll}
@@ -2197,7 +2207,7 @@ $$\begin{array}{rrcll}
   \textrm{Pre-projections} & p &::=& t.f & \textrm{one column from a table} \\
   &&& t.\{\{c\}\} & \textrm{a record of columns from a table (of kind $\{\mt{Type}\}$)} \\
   &&& t.* & \textrm{all columns from a table} \\
-  &&& E \; [\mt{AS} \; f] & \textrm{expression column} \\
+  &&& \hat{E} \; [\mt{AS} \; f] & \textrm{expression column} \\
   \textrm{Table names} & t &::=& x & \textrm{constant table name (automatically capitalized)} \\
   &&& X & \textrm{constant table name} \\
   &&& \{\{c\}\} & \textrm{computed table name (of kind $\mt{Name}$)} \\
@@ -2216,8 +2226,7 @@ $$\begin{array}{rrcll}
   \textrm{SQL expressions} & E &::=& t.f & \textrm{column references} \\
   &&& X & \textrm{named expression references} \\
   &&& \{[e]\} & \textrm{injected native Ur expressions} \\
-  &&& \{e\} & \textrm{computed expressions, probably using} \\
-    &&&& \hspace{.1in} \textrm{$\mt{sql\_exp}$ directly} \\
+  &&& \{e\} & \textrm{computed expressions, probably using $\mt{sql\_exp}$ directly} \\
   &&& \mt{TRUE} \mid \mt{FALSE} & \textrm{boolean constants} \\
   &&& \ell & \textrm{primitive type literals} \\
   &&& \mt{NULL} & \textrm{null value (injection of $\mt{None}$)} \\
@@ -2226,12 +2235,10 @@ $$\begin{array}{rrcll}
   &&& n & \textrm{nullary operators} \\
   &&& u \; E & \textrm{unary operators} \\
   &&& E \; b \; E & \textrm{binary operators} \\
-  &&& \mt{COUNT}(\ast) \; [w] & \textrm{count number of rows} \\
-  &&& \mt{RANK}() \; [w] & \textrm{rank in sequence (Postgres only)} \\
-  &&& a(E) \; [w] & \textrm{other aggregate function} \\
+  &&& \mt{COUNT}(\ast) & \textrm{count number of rows} \\
+  &&& a(E) & \textrm{other aggregate function} \\
   &&& \mt{IF} \; E \; \mt{THEN} \; E \; \mt{ELSE} \; E & \textrm{conditional} \\
-  &&& (Q) & \textrm{subquery (must return a single} \\
-  &&&& \hspace{.1in} \textrm{expression column)} \\
+  &&& (Q) & \textrm{subquery (must return a single expression column)} \\
   &&& (E) & \textrm{explicit precedence} \\
   \textrm{Nullary operators} & n &::=& \mt{CURRENT\_TIMESTAMP} \\
   \textrm{Unary operators} & u &::=& \mt{NOT} \\
@@ -2239,7 +2246,13 @@ $$\begin{array}{rrcll}
   \textrm{Aggregate functions} & a &::=& \mt{COUNT} \mid \mt{AVG} \mid \mt{SUM} \mid \mt{MIN} \mid \mt{MAX} \\
   \textrm{Directions} & o &::=& \mt{ASC} \mid \mt{DESC} \mid \{e\} \\
   \textrm{SQL integer} & N &::=& n \mid \{e\} \\
-  \textrm{Window} & w &::=& \mt{OVER} \; ([\mt{PARTITION} \; \mt{BY} \; E] \; [\mt{ORDER} \; \mt{BY} \; O]) & \textrm{(Postgres only)}
+  \textrm{Windowable expressions} & \hat{E} &::=& E \\
+  &&& w \; [\mt{OVER} \; ( & \textrm{(Postgres only)} \\
+  &&& \hspace{.1in} [\mt{PARTITION} \; \mt{BY} \; E] \\
+  &&& \hspace{.1in} [\mt{ORDER} \; \mt{BY} \; O])] \\
+  \textrm{Window function} & w &::=& \mt{RANK}() \\
+  &&& \mt{COUNT}(*) \\
+  &&& a(E)
 \end{array}$$
 
 Additionally, an SQL expression may be inserted into normal Ur code with the syntax $(\mt{SQL} \; E)$ or $(\mt{WHERE} \; E)$.  Similar shorthands exist for other nonterminals, with the prefix $\mt{FROM}$ for $\mt{FROM}$ items and $\mt{SELECT1}$ for pre-queries.
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 68e20fb0..bea6e105 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -305,23 +305,15 @@ val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused :::
            OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
        -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
 
-con allow_window :: {Unit}
-con disallow_window :: {Unit}
-
-con sql_exp :: {{Type}} (* Free tables, for normal use *)
-    -> {{Type}}         (* Free tables, for use in arguments to aggregate functions *)
-    -> {Type}           (* Free ad-hoc variables *)
-    -> {Unit}           (* Allow window functions here?  ([allow_window] indicates yes.) *)
-    -> Type             (* SQL type of this expression *)
-    -> Type
-val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type
+con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
+val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
                      -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type}
                      -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] =>
-                     sql_exp fs agg exps aw t
-                     -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') aw t
+                     sql_exp fs agg exps t
+                     -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t
 
 val check : fs ::: {Type}
-            -> sql_exp [] [] fs disallow_window bool
+            -> sql_exp [] [] fs bool
             -> sql_constraint fs []
 
 
@@ -359,7 +351,7 @@ val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type
 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) [] [] disallow_window bool
+       -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool
        -> sql_from_items free (tabs1 ++ tabs2)
 
 class nullify :: Type -> Type -> Type
@@ -370,14 +362,14 @@ val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(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 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) [] [] disallow_window bool
+       -> 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 : 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 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) [] [] disallow_window bool
+       -> 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 : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
@@ -385,9 +377,12 @@ val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::
     => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (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)) [] [] disallow_window bool
+       -> 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))
 
+(** [ORDER BY] and [SELECT] expressions may use window functions, so we introduce a type family for such expressions. *)
+con sql_expw :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
+
 val sql_query1 : free ::: {{Type}}
                  -> afree ::: {{Type}}
                  -> tables ::: {{Type}}
@@ -401,11 +396,11 @@ val sql_query1 : free ::: {{Type}}
                  => [empties ~ selectedFields]
                  => {Distinct : bool,
                      From : sql_from_items free tables,
-                     Where : sql_exp (free ++ tables) afree [] disallow_window bool,
+                     Where : sql_exp (free ++ tables) afree [] bool,
                      GroupBy : sql_subset tables grouped,
-                     Having : sql_exp (free ++ grouped) (afree ++ tables) [] disallow_window bool,
+                     Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool,
                      SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
-                     SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [] allow_window)
+                     SelectExps : $(map (sql_expw (free ++ grouped) (afree ++ tables) [])
                                             selectedExps) }
                  -> sql_query1 free afree tables selectedFields selectedExps
 
@@ -432,10 +427,21 @@ type sql_direction
 val sql_asc : sql_direction
 val sql_desc : sql_direction
 
+(** This type class supports automatic injection of either regular or window expressions into [sql_expw]. *)
+class sql_window :: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type) -> Type
+val sql_window_normal : sql_window sql_exp
+val sql_window_fancy : sql_window sql_expw
+val sql_window : tf ::: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type)
+                 -> tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+                 -> sql_window tf
+                 -> tf tables agg exps t
+                 -> sql_expw tables agg exps t
+
 con sql_order_by :: {{Type}} -> {Type} -> Type
 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
-val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
-                        -> sql_exp tables [] exps allow_window t -> sql_direction
+val sql_order_by_Cons : tf ::: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type) -> tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+                        -> sql_window tf
+                        -> tf tables [] exps t -> sql_direction
                         -> sql_order_by tables exps
                         -> sql_order_by tables exps
 val sql_order_by_random : tables ::: {{Type}} -> exps ::: {Type}
@@ -462,42 +468,42 @@ val sql_query : free ::: {{Type}}
                 -> sql_query free afree selectedFields selectedExps
 
 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
-                -> aw ::: {Unit} -> fieldType ::: Type -> agg ::: {{Type}}
+                -> fieldType ::: Type -> agg ::: {{Type}}
                 -> exps ::: {Type}
                 -> tab :: Name -> field :: Name
                 -> sql_exp
                        ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
-                       agg exps aw fieldType
+                       agg exps fieldType
 
-val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> aw ::: {Unit} -> t ::: Type -> rest ::: {Type}
+val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
               -> nm :: Name
-              -> sql_exp tabs agg ([nm = t] ++ rest) aw t
+              -> sql_exp tabs agg ([nm = t] ++ rest) t
 
 class sql_injectable
 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
 
 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                 -> aw ::: {Unit} -> t ::: Type
-                 -> sql_injectable t -> t -> sql_exp tables agg exps aw t
+                 -> t ::: Type
+                 -> sql_injectable t -> t -> sql_exp tables agg exps t
 
 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                  -> aw ::: {Unit} -> t ::: Type
-                  -> sql_exp tables agg exps aw (option t)
-                  -> sql_exp tables agg exps aw bool
+                  -> t ::: Type
+                  -> sql_exp tables agg exps (option t)
+                  -> sql_exp tables agg exps bool
 
 val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                  -> aw ::: {Unit} -> t ::: Type
-                  -> sql_exp tables agg exps aw (option t)
-                  -> sql_exp tables agg exps aw t
-                  -> sql_exp tables agg exps aw t
+                  -> t ::: Type
+                  -> sql_exp tables agg exps (option t)
+                  -> sql_exp tables agg exps t
+                  -> sql_exp tables agg exps t
 
 val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                       -> aw ::: {Unit} -> t ::: Type
-                       -> sql_exp tables agg exps aw bool
-                       -> sql_exp tables agg exps aw t
-                       -> sql_exp tables agg exps aw t
-                       -> sql_exp tables agg exps aw t
+                       -> t ::: Type
+                       -> sql_exp tables agg exps bool
+                       -> sql_exp tables agg exps t
+                       -> sql_exp tables agg exps t
+                       -> sql_exp tables agg exps t
 
 class sql_arith
 val sql_arith_int : sql_arith int
@@ -507,9 +513,9 @@ val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t)
 con sql_unary :: Type -> Type -> Type
 val sql_not : sql_unary bool bool
 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                -> aw ::: {Unit} -> arg ::: Type -> res ::: Type
-                -> sql_unary arg res -> sql_exp tables agg exps aw arg
-                -> sql_exp tables agg exps aw res
+                -> arg ::: Type -> res ::: Type
+                -> sql_unary arg res -> sql_exp tables agg exps arg
+                -> sql_exp tables agg exps res
 
 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
 
@@ -517,10 +523,10 @@ con sql_binary :: Type -> Type -> Type -> Type
 val sql_and : sql_binary bool bool bool
 val sql_or : sql_binary bool bool bool
 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                 -> aw ::: {Unit} -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
-                 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps aw arg1
-                 -> sql_exp tables agg exps aw arg2
-                 -> sql_exp tables agg exps aw res
+                 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
+                 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
+                 -> sql_exp tables agg exps arg2
+                 -> sql_exp tables agg exps res
 
 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
@@ -537,14 +543,14 @@ val sql_ge : t ::: Type -> sql_binary t t bool
 
 val sql_like : sql_binary string string bool
 
-val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit}
-                -> sql_exp tables agg exps aw int
+val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+                -> sql_exp tables agg exps int
 
 con sql_aggregate :: Type -> Type -> Type
 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                    -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type
-                    -> sql_aggregate dom ran -> sql_exp agg agg exps aw dom
-                    -> sql_exp tables agg exps aw ran
+                    -> dom ::: Type -> ran ::: Type
+                    -> sql_aggregate dom ran -> sql_exp agg agg exps dom
+                    -> sql_exp tables agg exps ran
 
 val sql_count_col : t ::: Type -> sql_aggregate (option t) int
 
@@ -564,56 +570,59 @@ val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t)
 val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
 val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
 
-con sql_partition :: {{Type}} -> {{Type}} -> {Type} -> Type
-val sql_no_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                       -> sql_partition tables agg exps
-val sql_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
-                    -> sql_exp tables agg exps disallow_window t
-                    -> sql_partition tables agg exps
-
-con sql_window :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
-val sql_window : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                 -> t ::: Type
-                 -> sql_window tables agg exps t
-                 -> sql_partition tables agg exps
-                 -> sql_order_by tables exps
-                 -> sql_exp tables agg exps allow_window t
-
-val sql_window_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                           -> t ::: Type -> nt ::: Type
-                           -> sql_aggregate t nt
-                           -> sql_exp tables agg exps disallow_window t
-                           -> sql_window tables agg exps nt
-val sql_window_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                       -> sql_window tables agg exps int
-val sql_window_rank : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                      -> sql_window tables agg exps int
-
 con sql_nfunc :: Type -> Type
 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                -> aw ::: {Unit} -> t ::: Type
-                -> sql_nfunc t -> sql_exp tables agg exps aw t
+                -> t ::: Type
+                -> sql_nfunc t -> sql_exp tables agg exps t
 val sql_current_timestamp : sql_nfunc time
 
 con sql_ufunc :: Type -> Type -> Type
 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type
-                -> sql_ufunc dom ran -> sql_exp tables agg exps aw dom
-                -> sql_exp tables agg exps aw ran
+                -> dom ::: Type -> ran ::: Type
+                -> sql_ufunc dom ran -> sql_exp tables agg exps dom
+                -> sql_exp tables agg exps ran
 val sql_octet_length : sql_ufunc blob int
 val sql_known : t ::: Type -> sql_ufunc t bool
 val sql_lower : sql_ufunc string string
 val sql_upper : sql_ufunc string string
 
-val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type
+val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
                    -> sql_injectable_prim t
-                   -> sql_exp tables agg exps aw t
-                   -> sql_exp tables agg exps aw (option t)
+                   -> sql_exp tables agg exps t
+                   -> sql_exp tables agg exps (option t)
 
-val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> aw ::: {Unit} -> t ::: Type -> nt ::: Type
+val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type
                    -> nullify t nt
                    -> sql_query tables agg [] [nm = t]
-                   -> sql_exp tables agg exps aw nt
+                   -> sql_exp tables agg exps nt
+
+(** Window function expressions *)
+
+con sql_partition :: {{Type}} -> {{Type}} -> {Type} -> Type
+val sql_no_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+                       -> sql_partition tables agg exps
+val sql_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+                    -> sql_exp tables agg exps t
+                    -> sql_partition tables agg exps
+
+con sql_window_function :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
+val sql_window_function : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+                          -> t ::: Type
+                          -> sql_window_function tables agg exps t
+                          -> sql_partition tables agg exps
+                          -> sql_order_by tables exps
+                          -> sql_expw tables agg exps t
+
+val sql_window_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+                           -> t ::: Type -> nt ::: Type
+                           -> sql_aggregate t nt
+                           -> sql_exp tables agg exps t
+                           -> sql_window_function tables agg exps nt
+val sql_window_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+                       -> sql_window_function tables agg exps int
+val sql_rank : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+               -> sql_window_function tables agg exps int
+
 
 (*** Executing queries *)
 
@@ -637,19 +646,19 @@ val tryDml : dml -> transaction (option string)
 
 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
              -> sql_table fields uniques
-             -> $(map (fn t :: Type => sql_exp [] [] [] disallow_window t) fields)
+             -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
              -> dml
 
 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
              [changed ~ unchanged] =>
-                $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] disallow_window t) changed)
+                $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
                 -> sql_table (changed ++ unchanged) uniques
-                -> sql_exp [T = changed ++ unchanged] [] [] disallow_window bool
+                -> sql_exp [T = changed ++ unchanged] [] [] bool
                 -> dml
 
 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
              -> sql_table fields uniques
-             -> sql_exp [T = fields] [] [] disallow_window bool
+             -> sql_exp [T = fields] [] [] bool
              -> dml
 
 (*** Sequences *)
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 60774ba5..e504204e 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -376,14 +376,14 @@ fun nonempty [fs] [us] (t : sql_table fs us) =
     oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t)
 
 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
-    [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t))
-    (e1 : sql_exp tables agg exps aw (option t))
-    (e2 : sql_exp tables agg exps aw (option t)) =
+    [t ::: Type] (_ : sql_injectable (option t))
+    (e1 : sql_exp tables agg exps (option t))
+    (e2 : sql_exp tables agg exps (option t)) =
     (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
 
 fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
-    [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t))
-    (e1 : sql_exp tables agg exps aw (option t))
+    [t ::: Type] (_ : sql_injectable (option t))
+    (e1 : sql_exp tables agg exps (option t))
     (e2 : option t) =
     case e2 of
         None => (SQL {e1} IS NULL)
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index def3bc63..489e744d 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -269,15 +269,15 @@ val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us
                -> transaction bool
 
 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                 -> aw ::: {Unit} -> t ::: Type -> sql_injectable (option t)
-                 -> sql_exp tables agg exps aw (option t)
-                 -> sql_exp tables agg exps aw (option t)
-                 -> sql_exp tables agg exps aw bool
+                 -> t ::: Type -> sql_injectable (option t)
+                 -> sql_exp tables agg exps (option t)
+                 -> sql_exp tables agg exps (option t)
+                 -> sql_exp tables agg exps bool
 
 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
-                  -> aw ::: {Unit} -> t ::: Type -> sql_injectable (option t)
-                  -> sql_exp tables agg exps aw (option t)
+                  -> t ::: Type -> sql_injectable (option t)
+                  -> sql_exp tables agg exps (option t)
                   -> option t
-                  -> sql_exp tables agg exps aw bool
+                  -> sql_exp tables agg exps bool
 
 val mkRead' : t ::: Type -> (string -> option t) -> string -> read t
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 0e04cf51..4754d4ce 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -242,7 +242,11 @@ fun expError env err =
          eprefaces' ([("Class constraint", p_con env c)]
                      @ (case E.resolveFailureCause () of
                             NONE => []
-                          | SOME c' => [("Reduced to unresolvable", p_con env c')])))
+                          | SOME c' => [("Reduced to unresolvable", p_con env c')]))(*;
+         app (fn (c, rs) => (eprefaces' [("CLASS", p_con env c)];
+                             app (fn (c, e) => eprefaces' [("RULE", p_con env c),
+                                                           ("IMPL", p_exp env e)]) rs))
+             (E.listClasses env)*))
       | IllegalRec (x, e) =>
         (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
          eprefaces' [("Variable", PD.string x),
diff --git a/src/monoize.sml b/src/monoize.sml
index 8224b26f..4985c932 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -249,7 +249,13 @@ fun monoType env =
                     (L'.TFfi ("Basis", "string"), loc)
                   | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_from_items"), _), _), _), _) =>
                     (L'.TFfi ("Basis", "string"), loc)
-                  | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_exp"), _), _), _), _), _), _), _), _), _), _) =>
+                  | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_exp"), _), _), _), _), _), _), _), _) =>
+                    (L'.TFfi ("Basis", "string"), loc)
+                  | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_expw"), _), _), _), _), _), _), _), _) =>
+                    (L'.TFfi ("Basis", "string"), loc)
+                  | L.CApp ((L.CFfi ("Basis", "sql_window"), _), _) =>
+                    (L'.TRecord [], loc)
+                  | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_window_function"), _), _), _), _), _), _), _), _) =>
                     (L'.TFfi ("Basis", "string"), loc)
                   | L.CApp ((L.CApp ((L.CFfi ("Basis", "primary_key"), _), _), _), _) =>
                     (L'.TFfi ("Basis", "string"), loc)
@@ -299,16 +305,16 @@ fun monoType env =
                     (L'.TRecord [], loc)
                   | L.CApp ((L.CFfi ("Basis", "sql_maxable"), _), _) =>
                     (L'.TRecord [], loc)
-                  | L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_partition"), _), _), _), _), _), _) =>
-                    (L'.TFfi ("Basis", "string"), loc)
-                  | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_window"), _), _), _), _), _), _), _), _) =>
-                    (L'.TFfi ("Basis", "string"), loc)
                   | L.CApp ((L.CFfi ("Basis", "sql_arith"), _), _) =>
                     (L'.TRecord [], loc)
                   | L.CApp ((L.CFfi ("Basis", "sql_nfunc"), _), _) =>
                     (L'.TFfi ("Basis", "string"), loc)
                   | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_ufunc"), _), _), _), _) =>
                     (L'.TFfi ("Basis", "string"), loc)
+                  | L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_partition"), _), _), _), _), _), _) =>
+                    (L'.TFfi ("Basis", "string"), loc)
+                  | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_window"), _), _), _), _), _), _), _), _) =>
+                    (L'.TFfi ("Basis", "string"), loc)
 
                   | L.CApp ((L.CFfi ("Basis", "channel"), _), _) =>
                     (L'.TFfi ("Basis", "channel"), loc)
@@ -2111,9 +2117,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             (L.ECApp (
              (L.ECApp (
               (L.ECApp (
-               (L.ECApp (
-                (L.EFfi ("Basis", "sql_inject"), _),
-                _), _),
+               (L.EFfi ("Basis", "sql_inject"), _),
                _), _),
               _), _),
              _), _),
@@ -2426,7 +2430,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
           | L.ECApp (
             (L.ECApp (
              (L.ECApp (
-              (L.EFfi ("Basis", "sql_order_by_Cons"), _),
+              (L.ECApp (
+               (L.EFfi ("Basis", "sql_order_by_Cons"), _),
+               _), _),
               _), _),
              _), _),
             _) =>
@@ -2434,19 +2440,20 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                 val s = (L'.TFfi ("Basis", "string"), loc)
                 fun sc s = (L'.EPrim (Prim.String s), loc)
             in
-                ((L'.EAbs ("e1", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc),
-                           (L'.EAbs ("d", s, (L'.TFun (s, s), loc),
-                                     (L'.EAbs ("e2", s, s,
-                                               (L'.ECase ((L'.ERel 0, loc),
-                                                          [((L'.PPrim (Prim.String ""), loc),
-                                                            strcat [(L'.ERel 2, loc),
-                                                                    (L'.ERel 1, loc)]),
-                                                           ((L'.PWild, loc),
-                                                            strcat [(L'.ERel 2, loc),
-                                                                    (L'.ERel 1, loc),
-                                                                    sc ", ",
-                                                                    (L'.ERel 0, loc)])],
-                                                          {disc = s, result = s}), loc)), loc)), loc)), loc),
+                ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun (s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc)), loc),
+                           (L'.EAbs ("e1", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc),
+                                     (L'.EAbs ("d", s, (L'.TFun (s, s), loc),
+                                               (L'.EAbs ("e2", s, s,
+                                                         (L'.ECase ((L'.ERel 0, loc),
+                                                                    [((L'.PPrim (Prim.String ""), loc),
+                                                                      strcat [(L'.ERel 2, loc),
+                                                                              (L'.ERel 1, loc)]),
+                                                                     ((L'.PWild, loc),
+                                                                      strcat [(L'.ERel 2, loc),
+                                                                              (L'.ERel 1, loc),
+                                                                              sc ", ",
+                                                                              (L'.ERel 0, loc)])],
+                                                                    {disc = s, result = s}), loc)), loc)), loc)), loc)), loc),
                  fm)
             end
 
@@ -2512,10 +2519,8 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
              (L.ECApp (
               (L.ECApp (
                (L.ECApp (
-                (L.ECApp (
                  (L.EFfi ("Basis", "sql_unary"), _),
                  _), _),
-                _), _),
                _), _),
               _), _),
              _), _),
@@ -2544,9 +2549,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
               (L.ECApp (
                (L.ECApp (
                 (L.ECApp (
-                 (L.ECApp (
-                  (L.EFfi ("Basis", "sql_binary"), _),
-                  _), _),
+                 (L.EFfi ("Basis", "sql_binary"), _),
                  _), _),
                 _), _),
                _), _),
@@ -2579,9 +2582,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                (L.ECApp (
                 (L.ECApp (
                  (L.ECApp (
-                  (L.ECApp (
-                   (L.EFfi ("Basis", "sql_field"), _),
-                   _), _),
+                  (L.EFfi ("Basis", "sql_field"), _),
                   _), _),
                  _), _),
                 _), _),
@@ -2595,9 +2596,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
              (L.ECApp (
               (L.ECApp (
                (L.ECApp (
-                (L.ECApp (
-                 (L.EFfi ("Basis", "sql_exp"), _),
-                 _), _),
+                (L.EFfi ("Basis", "sql_exp"), _),
                 _), _),
                _), _),
               _), _),
@@ -2701,9 +2700,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
           | L.ECApp (
             (L.ECApp (
              (L.ECApp (
-              (L.ECApp (
-               (L.EFfi ("Basis", "sql_count"), _),
-               _), _),
+              (L.EFfi ("Basis", "sql_count"), _),
               _), _),
              _), _),
             _) => ((L'.EPrim (Prim.String "COUNT(*)"), loc),
@@ -2714,9 +2711,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
              (L.ECApp (
               (L.ECApp (
                (L.ECApp (
-                (L.ECApp (
-                 (L.EFfi ("Basis", "sql_aggregate"), _),
-                 _), _),
+                (L.EFfi ("Basis", "sql_aggregate"), _),
                 _), _),
                _), _),
               _), _),
@@ -2732,7 +2727,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                                    sc ")"]
             in
                 ((L'.EAbs ("c", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc),
-                           (L'.EAbs ("e1", s, s, main), loc)), loc),
+                           (L'.EAbs ("e1", s, (L'.TFun (s, s), loc), main), loc)), loc),
                  fm)
             end
 
@@ -2781,73 +2776,33 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                                  (L'.EPrim (Prim.String "MIN"), loc)), loc)), loc),
              fm)
 
-          | L.ECApp (
-            (L.ECApp (
-             (L.ECApp (
-               (L.EFfi ("Basis", "sql_no_partition"), _),
-               _), _),
-             _), _),
-            _) => ((L'.EPrim (Prim.String ""), loc), fm)
-          | L.ECApp (
-            (L.ECApp (
-             (L.ECApp (
-              (L.ECApp (
-               (L.EFfi ("Basis", "sql_partition"), _),
-               _), _),
-              _), _),
-             _), _),
-            _) =>
-            let
-                val s = (L'.TFfi ("Basis", "string"), loc)
-            in
-                ((L'.EAbs ("e", s, s, strcat [(L'.EPrim (Prim.String "PARTITION BY "), loc), (L'.ERel 0, loc)]), loc),
-                 fm)
-            end
-
+          | L.EFfi ("Basis", "sql_asc") => ((L'.EPrim (Prim.String ""), loc), fm)
+          | L.EFfi ("Basis", "sql_desc") => ((L'.EPrim (Prim.String " DESC"), loc), fm)
           | L.ECApp (
             (L.ECApp (
              (L.ECApp (
               (L.ECApp (
-               (L.EFfi ("Basis", "sql_window"), _),
+               (L.EFfi ("Basis", "sql_nfunc"), _),
                _), _),
               _), _),
              _), _),
-            _) =>
+           _) =>
             let
-                val () = if #windowFunctions (Settings.currentDbms ()) then
-                             ()
-                         else
-                             ErrorMsg.errorAt loc "The DBMS you've selected doesn't support window functions."
-
                 val s = (L'.TFfi ("Basis", "string"), loc)
                 fun sc s = (L'.EPrim (Prim.String s), loc)
-
-                val main = strcat [(L'.ERel 2, loc),
-                                   sc " OVER (",
-                                   (L'.ERel 1, loc),
-                                   (L'.ECase ((L'.ERel 0, loc),
-                                              [((L'.PPrim (Prim.String ""), loc),
-                                                sc ""),
-                                               ((L'.PWild, loc),
-                                                strcat [sc " ORDER BY ",
-                                                        (L'.ERel 0, loc)])],
-                                              {disc = s,
-                                               result = s}), loc),
-                                   sc ")"]
             in
-                ((L'.EAbs ("w", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc),
-                           (L'.EAbs ("p", s, (L'.TFun (s, s), loc),
-                                     (L'.EAbs ("o", s, s,
-                                               main), loc)), loc)), loc),
+                ((L'.EAbs ("s", s, s, (L'.ERel 0, loc)), loc),
                  fm)
             end
 
+          | L.EFfi ("Basis", "sql_window_normal") => ((L'.ERecord [], loc), fm)
+          | L.EFfi ("Basis", "sql_window_fancy") => ((L'.ERecord [], loc), fm)
           | L.ECApp (
             (L.ECApp (
              (L.ECApp (
               (L.ECApp (
                (L.ECApp (
-                (L.EFfi ("Basis", "sql_window_aggregate"), _),
+                (L.EFfi ("Basis", "sql_window"), _),
                 _), _),
                _), _),
               _), _),
@@ -2855,43 +2810,13 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             _) =>
             let
                 val s = (L'.TFfi ("Basis", "string"), loc)
-                fun sc s = (L'.EPrim (Prim.String s), loc)
-
-                val main = strcat [(L'.ERel 1, loc),
-                                   sc "(",
-                                   (L'.ERel 0, loc),
-                                   sc ")"]
             in
-                ((L'.EAbs ("c", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc),
-                           (L'.EAbs ("e1", s, s, main), loc)), loc),
+                ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun (s, s), loc),
+                           (L'.EAbs ("e", s, s,
+                                     (L'.ERel 0, loc)), loc)), loc),
                  fm)
             end
 
-          | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_window_count"), _), _), _), _), _), _) =>
-            ((L'.EPrim (Prim.String "COUNT(*)"), loc), fm)
-          | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_window_rank"), _), _), _), _), _), _) =>
-            ((L'.EPrim (Prim.String "RANK()"), loc), fm)
-
-          | L.EFfi ("Basis", "sql_asc") => ((L'.EPrim (Prim.String ""), loc), fm)
-          | L.EFfi ("Basis", "sql_desc") => ((L'.EPrim (Prim.String " DESC"), loc), fm)
-          | L.ECApp (
-            (L.ECApp (
-             (L.ECApp (
-              (L.ECApp (
-               (L.ECApp (
-                (L.EFfi ("Basis", "sql_nfunc"), _),
-                _), _),
-               _), _),
-              _), _),
-             _), _),
-            _) =>
-            let
-                val s = (L'.TFfi ("Basis", "string"), loc)
-                fun sc s = (L'.EPrim (Prim.String s), loc)
-            in
-                ((L'.EAbs ("s", s, s, (L'.ERel 0, loc)), loc),
-                 fm)
-            end
           | L.EFfi ("Basis", "sql_current_timestamp") => ((L'.EPrim (Prim.String "CURRENT_TIMESTAMP"), loc), fm)
 
           | L.ECApp (
@@ -2899,9 +2824,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
              (L.ECApp (
               (L.ECApp (
                (L.ECApp (
-                (L.ECApp (
-                 (L.EFfi ("Basis", "sql_ufunc"), _),
-                 _), _),
+                (L.EFfi ("Basis", "sql_ufunc"), _),
                 _), _),
                _), _),
               _), _),
@@ -2935,9 +2858,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
              (L.ECApp (
               (L.ECApp (
                (L.ECApp (
-                (L.ECApp (
-                 (L.EFfi ("Basis", "sql_is_null"), _), _),
-                 _), _),
+                (L.EFfi ("Basis", "sql_is_null"), _), _),
                 _), _),
                _), _),
               _), _)) =>
@@ -2978,11 +2899,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
              (L.ECApp (
               (L.ECApp (
                (L.ECApp (
-                (L.ECApp (
-                 (L.ECApp (
-                  (L.EFfi ("Basis", "sql_if_then_else"), _), _),
-                  _), _),
-                 _), _),
+                (L.EFfi ("Basis", "sql_if_then_else"), _), _),
                 _), _),
                _), _),
               _), _)) =>
@@ -3007,9 +2924,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             (L.ECApp (
              (L.ECApp (
               (L.ECApp (
-               (L.ECApp (
-                (L.EFfi ("Basis", "sql_nullable"), _),
-                _), _),
+               (L.EFfi ("Basis", "sql_nullable"), _),
                _), _),
               _), _),
              _), _),
@@ -3030,9 +2945,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
               (L.ECApp (
                (L.ECApp (
                 (L.ECApp (
-                 (L.ECApp (
-                  (L.EFfi ("Basis", "sql_subquery"), _),
-                  _), _),
+                 (L.EFfi ("Basis", "sql_subquery"), _),
                  _), _),
                 _), _),
                _), _),
@@ -3051,6 +2964,97 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                  fm)
             end
 
+          | L.ECApp (
+            (L.ECApp (
+             (L.ECApp (
+               (L.EFfi ("Basis", "sql_no_partition"), _),
+               _), _),
+             _), _),
+            _) => ((L'.EPrim (Prim.String ""), loc), fm)
+          | L.ECApp (
+            (L.ECApp (
+             (L.ECApp (
+              (L.ECApp (
+               (L.EFfi ("Basis", "sql_partition"), _),
+               _), _),
+              _), _),
+             _), _),
+            _) =>
+            let
+                val s = (L'.TFfi ("Basis", "string"), loc)
+            in
+                ((L'.EAbs ("e", s, s, strcat [(L'.EPrim (Prim.String "PARTITION BY "), loc), (L'.ERel 0, loc)]), loc),
+                 fm)
+            end
+
+          | L.ECApp (
+            (L.ECApp (
+             (L.ECApp (
+              (L.ECApp (
+               (L.EFfi ("Basis", "sql_window_function"), _),
+               _), _),
+              _), _),
+             _), _),
+            _) =>
+            let
+                val () = if #windowFunctions (Settings.currentDbms ()) then
+                             ()
+                         else
+                             ErrorMsg.errorAt loc "The DBMS you've selected doesn't support window functions."
+
+                val s = (L'.TFfi ("Basis", "string"), loc)
+                fun sc s = (L'.EPrim (Prim.String s), loc)
+
+                val main = strcat [(L'.ERel 2, loc),
+                                   sc " OVER (",
+                                   (L'.ERel 1, loc),
+                                   (L'.ECase ((L'.ERel 0, loc),
+                                              [((L'.PPrim (Prim.String ""), loc),
+                                                sc ""),
+                                               ((L'.PWild, loc),
+                                                strcat [sc " ORDER BY ",
+                                                        (L'.ERel 0, loc)])],
+                                              {disc = s,
+                                               result = s}), loc),
+                                   sc ")"]
+            in
+                ((L'.EAbs ("w", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc),
+                           (L'.EAbs ("p", s, (L'.TFun (s, s), loc),
+                                     (L'.EAbs ("o", s, s,
+                                               main), loc)), loc)), loc),
+                 fm)
+            end
+
+          | L.ECApp (
+            (L.ECApp (
+             (L.ECApp (
+              (L.ECApp (
+               (L.ECApp (
+                (L.EFfi ("Basis", "sql_window_aggregate"), _),
+                _), _),
+               _), _),
+              _), _),
+             _), _),
+            _) =>
+            let
+                val s = (L'.TFfi ("Basis", "string"), loc)
+                fun sc s = (L'.EPrim (Prim.String s), loc)
+
+                val main = strcat [(L'.ERel 1, loc),
+                                   sc "(",
+                                   (L'.ERel 0, loc),
+                                   sc ")"]
+            in
+                ((L'.EAbs ("c", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc),
+                           (L'.EAbs ("e1", s, s, main), loc)), loc),
+                 fm)
+            end
+
+          | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_window_count"), _), _), _), _), _), _) =>
+            ((L'.EPrim (Prim.String "COUNT(*)"), loc), fm)
+          | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_rank"), _), _), _), _), _), _) =>
+            ((L'.EPrim (Prim.String "RANK()"), loc), fm)
+
           | L.EFfiApp ("Basis", "nextval", [(e, _)]) =>
             let
                 val (e, fm) = monoExp (env, st, fm) e
diff --git a/src/settings.sml b/src/settings.sml
index 3b89ce46..28739d6a 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -538,7 +538,7 @@ type dbms = {
      falseString : string,
      onlyUnion : bool,
      nestedRelops : bool,
-     windowFunctions : bool
+     windowFunctions: bool
 }
 
 val dbmses = ref ([] : dbms list)
diff --git a/src/urweb.grm b/src/urweb.grm
index eec8f8c1..708e5fcd 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -309,7 +309,7 @@ fun applyWindow loc e window =
                                         (ECApp ((EVar (["Basis"], "sql_order_by_Nil", Infer), dummy),
                                                 (CWild (KRecord (KType, dummy), dummy), dummy)),
                                          dummy)))
-        val e' = (EVar (["Basis"], "sql_window", Infer), loc)
+        val e' = (EVar (["Basis"], "sql_window_function", Infer), loc)
         val e' = (EApp (e', e), loc)
         val e' = (EApp (e', pb), loc)
     in
@@ -345,7 +345,7 @@ fun applyWindow loc e window =
  | UNION | INTERSECT | EXCEPT
  | LIMIT | OFFSET | ALL
  | TRUE | FALSE | CAND | OR | NOT
- | COUNT | AVG | SUM | MIN | MAX | RANK
+ | COUNT | AVG | SUM | MIN | MAX | RANK | PARTITION | OVER
  | ASC | DESC | RANDOM
  | INSERT | INTO | VALUES | UPDATE | SET | DELETE | NULL | IS | COALESCE | LIKE
  | CURRENT_TIMESTAMP
@@ -353,7 +353,6 @@ fun applyWindow loc e window =
  | CCONSTRAINT | UNIQUE | CHECK | PRIMARY | FOREIGN | KEY | ON | NO | ACTION | RESTRICT | CASCADE | REFERENCES
  | JOIN | INNER | CROSS | OUTER | LEFT | RIGHT | FULL
  | CIF | CTHEN | CELSE
- | OVER | PARTITION
 
 %nonterm
    file of decl list
@@ -1755,6 +1754,8 @@ query1 : SELECT dopt select FROM tables wopt gopt hopt
                                                           exps)
                                                      end
 
+                                             val exps = map (fn (c, e) => (c, (EApp ((EVar (["Basis"], "sql_window", Infer), loc), e), loc))) exps
+
                                              val sel = (CRecord sel, loc)
 
                                              val grp = case gopt of
@@ -2041,49 +2042,37 @@ sqlexp : TRUE                           (sql_inject (EVar (["Basis"], "True", In
        | NULL                           (sql_inject ((EVar (["Basis"], "None", Infer), 
                                                       s (NULLleft, NULLright))))
 
-       | COUNT LPAREN STAR RPAREN window (let
-                                              val loc = s (COUNTleft, windowright)
-                                          in
-                                              case window of
-                                                  NONE => (EVar (["Basis"], "sql_count", Infer), loc)
-                                                | SOME _ =>
-                                                  let
-                                                      val e = (EVar (["Basis"], "sql_window_count", Infer), loc)
-                                                  in
-                                                      applyWindow loc e window
-                                                  end
-                                          end)
-       | RANK UNIT window                (let
-                                              val loc = s (RANKleft, windowright)
-                                              val e = (EVar (["Basis"], "sql_window_rank", Infer), loc)
-                                          in
-                                              applyWindow loc e window
-                                          end)
-       | COUNT LPAREN sqlexp RPAREN window (let
-                                                val loc = s (COUNTleft, windowright)
-                                                          
-                                                val e = (EVar (["Basis"], "sql_count_col", Infer), loc)
-                                            in
-                                                case window of
-                                                    NONE =>
-                                                    let
-                                                        val e = (EApp ((EVar (["Basis"], "sql_aggregate", Infer), loc),
-                                                                       e), loc)
-                                                    in
-                                                        (EApp (e, sqlexp), loc)
-                                                    end
-                                                  | SOME _ =>
-                                                    let
-                                                        val e = (EApp ((EVar (["Basis"], "sql_window_aggregate", Infer), loc),
-                                                                       e), loc)
-                                                        val e = (EApp (e, sqlexp), loc)
-                                                    in
-                                                        applyWindow loc e window
-                                                    end
-                                            end)
+       | COUNT LPAREN STAR RPAREN window(let
+                                             val loc = s (COUNTleft, windowright)
+                                         in
+                                             case window of
+                                                 NONE => (EVar (["Basis"], "sql_count", Infer), loc)
+                                               | SOME _ => applyWindow loc (EVar (["Basis"], "sql_window_count", Infer), loc) window
+                                         end)
+       | COUNT LPAREN sqlexp RPAREN window(let
+                                               val loc = s (COUNTleft, RPARENright)
+                                               val e = (EVar (["Basis"], "sql_count_col", Infer), loc)
+                                           in
+                                               case window of
+                                                   NONE =>
+                                                   let
+                                                       val e = (EApp ((EVar (["Basis"], "sql_aggregate", Infer), loc),
+                                                                      e), loc)
+                                                   in
+                                                       (EApp (e, sqlexp), loc)
+                                                   end
+                                                 | SOME _ =>
+                                                   let
+                                                       val e = (EVar (["Basis"], "sql_count_col", Infer), loc)
+                                                       val e = (EApp ((EVar (["Basis"], "sql_window_aggregate", Infer), loc),
+                                                                      e), loc)
+                                                   in
+                                                       applyWindow loc (EApp (e, sqlexp), loc) window
+                                                   end
+                                           end)
        | sqlagg LPAREN sqlexp RPAREN window (let
-                                                 val loc = s (sqlaggleft, windowright)
-
+                                                 val loc = s (sqlaggleft, RPARENright)
+                                                           
                                                  val e = (EVar (["Basis"], "sql_" ^ sqlagg, Infer), loc)
                                              in
                                                  case window of
@@ -2098,11 +2087,15 @@ sqlexp : TRUE                           (sql_inject (EVar (["Basis"], "True", In
                                                      let
                                                          val e = (EApp ((EVar (["Basis"], "sql_window_aggregate", Infer), loc),
                                                                         e), loc)
-                                                         val e = (EApp (e, sqlexp), loc)
                                                      in
-                                                         applyWindow loc e window
+                                                         applyWindow loc (EApp (e, sqlexp), loc) window
                                                      end
                                              end)
+       | RANK UNIT window               (let
+                                             val loc = s (RANKleft, windowright)
+                                         in
+                                             applyWindow loc (EVar (["Basis"], "sql_rank", Infer), loc) window
+                                         end)
        | COALESCE LPAREN sqlexp COMMA sqlexp RPAREN
                                         (let
                                              val loc = s (COALESCEright, sqlexp2right)
diff --git a/src/urweb.lex b/src/urweb.lex
index 272c5e65..0994ecec 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -463,8 +463,6 @@ xint = x[0-9a-fA-F][0-9a-fA-F];
 <INITIAL> "OFFSET"    => (Tokens.OFFSET (pos yypos, pos yypos + size yytext));
 <INITIAL> "ALL"       => (Tokens.ALL (pos yypos, pos yypos + size yytext));
 <INITIAL> "SELECT1"   => (Tokens.SELECT1 (pos yypos, pos yypos + size yytext));
-<INITIAL> "OVER"      => (Tokens.OVER (pos yypos, pos yypos + size yytext));
-<INITIAL> "PARTITION" => (Tokens.PARTITION (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "JOIN"      => (Tokens.JOIN (pos yypos, pos yypos + size yytext));
 <INITIAL> "INNER"     => (Tokens.INNER (pos yypos, pos yypos + size yytext));
@@ -490,6 +488,8 @@ xint = x[0-9a-fA-F][0-9a-fA-F];
 <INITIAL> "MIN"       => (Tokens.MIN (pos yypos, pos yypos + size yytext));
 <INITIAL> "MAX"       => (Tokens.MAX (pos yypos, pos yypos + size yytext));
 <INITIAL> "RANK"      => (Tokens.RANK (pos yypos, pos yypos + size yytext));
+<INITIAL> "PARTITION" => (Tokens.PARTITION (pos yypos, pos yypos + size yytext));
+<INITIAL> "OVER"      => (Tokens.OVER (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "IF"        => (Tokens.CIF (pos yypos, pos yypos + size yytext));
 <INITIAL> "THEN"      => (Tokens.CTHEN (pos yypos, pos yypos + size yytext));
diff --git a/tests/window.ur b/tests/window.ur
index dc338a43..c0eaf6e2 100644
--- a/tests/window.ur
+++ b/tests/window.ur
@@ -1,6 +1,6 @@
 table empsalary : { Depname : string,
-                   Empno : int,
-                   Salary : int }
+                    Empno : int,
+                    Salary : int }
 
 fun main () : transaction page =
     x <- queryX (SELECT empsalary.Depname, empsalary.Empno, empsalary.Salary,