Monoized GROUP BY

4 files changed, 413 insertions, 346 deletions

diff --git a/src/elaborate.sml b/src/elaborate.sml
index 206c58cd..9fa22026 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1681,6 +1681,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                 val gsD = List.mapPartial (fn Disjoint d => SOME d | _ => NONE) gs
                 val gsO = List.filter (fn Disjoint _ => false | _ => true) gs
             in
+                (*TextIO.print ("|gsO| = " ^ Int.toString (length gsO) ^ "\n");*)
                 ((L'.ERecord xes', loc),
                  (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
                  enD (prove (xes', gsD)) @ gsO)
@@ -2729,377 +2730,387 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
 
 
 fun elabDecl ((d, loc), (env, denv, gs : constraint list)) =
-    case d of
-        L.DCon (x, ko, c) =>
-        let
-            val k' = case ko of
-                         NONE => kunif loc
-                       | SOME k => elabKind k
-
-            val (c', ck, gs') = elabCon (env, denv) c
-            val (env', n) = E.pushCNamed env x k' (SOME c')
-        in
-            checkKind env c' ck k';
-
-            ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
-        end
-      | L.DDatatype (x, xs, xcs) =>
-        let
-            val k = (L'.KType, loc)
-            val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
-            val (env, n) = E.pushCNamed env x k' NONE
-            val t = (L'.CNamed n, loc)
-            val nxs = length xs - 1
-            val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
-
-            val (env', denv') = foldl (fn (x, (env', denv')) =>
-                                          (E.pushCRel env' x k,
-                                           D.enter denv')) (env, denv) xs
-
-            val (xcs, (used, env, gs)) =
-                ListUtil.foldlMap
-                (fn ((x, to), (used, env, gs)) =>
-                    let
-                        val (to, t, gs') = case to of
-                                           NONE => (NONE, t, gs)
-                                         | SOME t' =>
-                                           let
-                                               val (t', tk, gs') = elabCon (env', denv') t'
-                                           in
-                                               checkKind env' t' tk k;
-                                               (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs)
-                                           end
-                        val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
-
-                        val (env, n') = E.pushENamed env x t
-                    in
-                        if SS.member (used, x) then
-                            strError env (DuplicateConstructor (x, loc))
-                        else
-                            ();
-                        ((x, n', to), (SS.add (used, x), env, gs'))
-                    end)
-                (SS.empty, env, []) xcs
-
-            val env = E.pushDatatype env n xs xcs
-        in
-            ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
-        end
-
-      | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
-
-      | L.DDatatypeImp (x, m1 :: ms, s) =>
-        (case E.lookupStr env m1 of
-             NONE => (expError env (UnboundStrInExp (loc, m1));
-                      ([], (env, denv, gs)))
-           | SOME (n, sgn) =>
-             let
-                 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
-                                     case E.projectStr env {sgn = sgn, str = str, field = m} of
-                                         NONE => (conError env (UnboundStrInCon (loc, m));
-                                                  (strerror, sgnerror))
-                                       | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
-                                  ((L'.StrVar n, loc), sgn) ms
-             in
-                 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
-                     ((L'.CModProj (n, ms, s), _), gs') =>
-                     (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
-                          NONE => (conError env (UnboundDatatype (loc, s));
-                                   ([], (env, denv, gs)))
-                        | SOME (xs, xncs) =>
-                          let
-                              val k = (L'.KType, loc)
-                              val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
-                              val t = (L'.CModProj (n, ms, s), loc)
-                              val (env, n') = E.pushCNamed env x k' (SOME t)
-                              val env = E.pushDatatype env n' xs xncs
+    let
+        (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
 
-                              val t = (L'.CNamed n', loc)
-                              val env = foldl (fn ((x, n, to), env) =>
-                                                  let
-                                                      val t = case to of
-                                                                  NONE => t
-                                                                | SOME t' => (L'.TFun (t', t), loc)
+        val r = 
+            case d of
+                L.DCon (x, ko, c) =>
+                let
+                    val k' = case ko of
+                                 NONE => kunif loc
+                               | SOME k => elabKind k
 
-                                                      val t = foldr (fn (x, t) =>
-                                                                        (L'.TCFun (L'.Implicit, x, k, t), loc))
-                                                              t xs
-                                                  in
-                                                      E.pushENamedAs env x n t
-                                                  end) env xncs
-                          in
-                              ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs))
-                          end)
-                   | _ => (strError env (NotDatatype loc);
-                           ([], (env, denv, [])))
-             end)
+                    val (c', ck, gs') = elabCon (env, denv) c
+                    val (env', n) = E.pushCNamed env x k' (SOME c')
+                in
+                    checkKind env c' ck k';
 
-      | L.DVal (x, co, e) =>
-        let
-            val (c', _, gs1) = case co of
-                                    NONE => (cunif (loc, ktype), ktype, [])
-                                  | SOME c => elabCon (env, denv) c
+                    ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
+                end
+              | L.DDatatype (x, xs, xcs) =>
+                let
+                    val k = (L'.KType, loc)
+                    val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+                    val (env, n) = E.pushCNamed env x k' NONE
+                    val t = (L'.CNamed n, loc)
+                    val nxs = length xs - 1
+                    val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
+
+                    val (env', denv') = foldl (fn (x, (env', denv')) =>
+                                                  (E.pushCRel env' x k,
+                                                   D.enter denv')) (env, denv) xs
+
+                    val (xcs, (used, env, gs')) =
+                        ListUtil.foldlMap
+                            (fn ((x, to), (used, env, gs)) =>
+                                let
+                                    val (to, t, gs') = case to of
+                                                           NONE => (NONE, t, gs)
+                                                         | SOME t' =>
+                                                           let
+                                                               val (t', tk, gs') = elabCon (env', denv') t'
+                                                           in
+                                                               checkKind env' t' tk k;
+                                                               (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs)
+                                                           end
+                                    val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
+
+                                    val (env, n') = E.pushENamed env x t
+                                in
+                                    if SS.member (used, x) then
+                                        strError env (DuplicateConstructor (x, loc))
+                                    else
+                                        ();
+                                    ((x, n', to), (SS.add (used, x), env, gs'))
+                                end)
+                            (SS.empty, env, []) xcs
 
-            val (e', et, gs2) = elabExp (env, denv) e
-            val gs3 = checkCon (env, denv) e' et c'
-            val (c', gs4) = normClassConstraint (env, denv) c'
-            val (env', n) = E.pushENamed env x c'
-        in
-            (*prefaces "DVal" [("x", Print.PD.string x),
-                             ("c'", p_con env c')];*)
-            ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
-        end
-      | L.DValRec vis =>
-        let
-            fun allowable (e, _) =
-                case e of
-                    L.EAbs _ => true
-                  | L.ECAbs (_, _, _, e) => allowable e
-                  | L.EDisjoint (_, _, e) => allowable e
-                  | _ => false
-
-            val (vis, gs) = ListUtil.foldlMap
-                                (fn ((x, co, e), gs) =>
-                                    let
-                                        val (c', _, gs1) = case co of
-                                                               NONE => (cunif (loc, ktype), ktype, [])
-                                                             | SOME c => elabCon (env, denv) c
-                                    in
-                                        ((x, c', e), enD gs1 @ gs)
-                                    end) [] vis
+                    val env = E.pushDatatype env n xs xcs
+                in
+                    ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs' @ gs))
+                end
 
-            val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
-                                                   let
-                                                       val (env, n) = E.pushENamed env x c'
-                                                   in
-                                                       ((x, n, c', e), env)
-                                                   end) env vis
+              | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
+
+              | L.DDatatypeImp (x, m1 :: ms, s) =>
+                (case E.lookupStr env m1 of
+                     NONE => (expError env (UnboundStrInExp (loc, m1));
+                              ([], (env, denv, gs)))
+                   | SOME (n, sgn) =>
+                     let
+                         val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+                                                    case E.projectStr env {sgn = sgn, str = str, field = m} of
+                                                        NONE => (conError env (UnboundStrInCon (loc, m));
+                                                                 (strerror, sgnerror))
+                                                      | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                                                ((L'.StrVar n, loc), sgn) ms
+                     in
+                         case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
+                             ((L'.CModProj (n, ms, s), _), gs') =>
+                             (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
+                                  NONE => (conError env (UnboundDatatype (loc, s));
+                                           ([], (env, denv, gs)))
+                                | SOME (xs, xncs) =>
+                                  let
+                                      val k = (L'.KType, loc)
+                                      val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+                                      val t = (L'.CModProj (n, ms, s), loc)
+                                      val (env, n') = E.pushCNamed env x k' (SOME t)
+                                      val env = E.pushDatatype env n' xs xncs
+
+                                      val t = (L'.CNamed n', loc)
+                                      val env = foldl (fn ((x, n, to), env) =>
+                                                          let
+                                                              val t = case to of
+                                                                          NONE => t
+                                                                        | SOME t' => (L'.TFun (t', t), loc)
+
+                                                              val t = foldr (fn (x, t) =>
+                                                                                (L'.TCFun (L'.Implicit, x, k, t), loc))
+                                                                            t xs
+                                                          in
+                                                              E.pushENamedAs env x n t
+                                                          end) env xncs
+                                  in
+                                      ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs))
+                                  end)
+                           | _ => (strError env (NotDatatype loc);
+                                   ([], (env, denv, [])))
+                     end)
 
-            val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
-                                                  let
-                                                      val (e', et, gs1) = elabExp (env, denv) e
-                                                                          
-                                                      val gs2 = checkCon (env, denv) e' et c'
-                                                  in
-                                                      if allowable e then
-                                                          ()
-                                                      else
-                                                          expError env (IllegalRec (x, e'));
-                                                      ((x, n, c', e'), gs1 @ enD gs2 @ gs)
-                                                  end) gs vis
-        in
-            ([(L'.DValRec vis, loc)], (env, denv, gs))
-        end
+              | L.DVal (x, co, e) =>
+                let
+                    val (c', _, gs1) = case co of
+                                           NONE => (cunif (loc, ktype), ktype, [])
+                                         | SOME c => elabCon (env, denv) c
+
+                    val (e', et, gs2) = elabExp (env, denv) e
+                    val gs3 = checkCon (env, denv) e' et c'
+                    val (c', gs4) = normClassConstraint (env, denv) c'
+                    val (env', n) = E.pushENamed env x c'
+                in
+                    (*prefaces "DVal" [("x", Print.PD.string x),
+                                       ("c'", p_con env c')];*)
+                    ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
+                end
+              | L.DValRec vis =>
+                let
+                    fun allowable (e, _) =
+                        case e of
+                            L.EAbs _ => true
+                          | L.ECAbs (_, _, _, e) => allowable e
+                          | L.EDisjoint (_, _, e) => allowable e
+                          | _ => false
+
+                    val (vis, gs) = ListUtil.foldlMap
+                                        (fn ((x, co, e), gs) =>
+                                            let
+                                                val (c', _, gs1) = case co of
+                                                                       NONE => (cunif (loc, ktype), ktype, [])
+                                                                     | SOME c => elabCon (env, denv) c
+                                            in
+                                                ((x, c', e), enD gs1 @ gs)
+                                            end) [] vis
+
+                    val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
+                                                           let
+                                                               val (env, n) = E.pushENamed env x c'
+                                                           in
+                                                               ((x, n, c', e), env)
+                                                           end) env vis
+
+                    val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
+                                                          let
+                                                              val (e', et, gs1) = elabExp (env, denv) e
+                                                                                  
+                                                              val gs2 = checkCon (env, denv) e' et c'
+                                                          in
+                                                              if allowable e then
+                                                                  ()
+                                                              else
+                                                                  expError env (IllegalRec (x, e'));
+                                                              ((x, n, c', e'), gs1 @ enD gs2 @ gs)
+                                                          end) gs vis
+                in
+                    ([(L'.DValRec vis, loc)], (env, denv, gs))
+                end
 
-      | L.DSgn (x, sgn) =>
-        let
-            val (sgn', gs') = elabSgn (env, denv) sgn
-            val (env', n) = E.pushSgnNamed env x sgn'
-        in
-            ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
-        end
+              | L.DSgn (x, sgn) =>
+                let
+                    val (sgn', gs') = elabSgn (env, denv) sgn
+                    val (env', n) = E.pushSgnNamed env x sgn'
+                in
+                    ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
+                end
 
-      | L.DStr (x, sgno, str) =>
-        let
-            val () = if x = "Basis" then
-                         raise Fail "Not allowed to redefine structure 'Basis'"
-                     else
-                         ()
+              | L.DStr (x, sgno, str) =>
+                let
+                    val () = if x = "Basis" then
+                                 raise Fail "Not allowed to redefine structure 'Basis'"
+                             else
+                                 ()
 
-            val formal = Option.map (elabSgn (env, denv)) sgno
+                    val formal = Option.map (elabSgn (env, denv)) sgno
 
-            val (str', sgn', gs') =
-                case formal of
-                    NONE =>
-                    let
-                        val (str', actual, ds) = elabStr (env, denv) str
-                    in
-                        (str', selfifyAt env {str = str', sgn = actual}, ds)
-                    end
-                  | SOME (formal, gs1) =>
-                    let
-                        val str =
-                            case #1 (hnormSgn env formal) of
-                                L'.SgnConst sgis =>
-                                (case #1 str of
-                                     L.StrConst ds =>
-                                     let
-                                         val needed = foldl (fn ((sgi, _), needed) =>
-                                                                case sgi of
-                                                                    L'.SgiConAbs (x, _, _) => SS.add (needed, x)
-                                                                  | _ => needed)
-                                                            SS.empty sgis
-                                                      
-                                         val needed = foldl (fn ((d, _), needed) =>
-                                                                case d of
-                                                                    L.DCon (x, _, _) => (SS.delete (needed, x)
-                                                                                         handle NotFound => needed)
-                                                                  | L.DClass (x, _) => (SS.delete (needed, x)
-                                                                                        handle NotFound => needed)
-                                                                  | L.DOpen _ => SS.empty
-                                                                  | _ => needed)
-                                                            needed ds
-                                     in
-                                         case SS.listItems needed of
-                                             [] => str
-                                           | xs =>
+                    val (str', sgn', gs') =
+                        case formal of
+                            NONE =>
+                            let
+                                val (str', actual, gs') = elabStr (env, denv) str
+                            in
+                                (str', selfifyAt env {str = str', sgn = actual}, gs')
+                            end
+                          | SOME (formal, gs1) =>
+                            let
+                                val str =
+                                    case #1 (hnormSgn env formal) of
+                                        L'.SgnConst sgis =>
+                                        (case #1 str of
+                                             L.StrConst ds =>
                                              let
-                                                 val kwild = (L.KWild, #2 str)
-                                                 val cwild = (L.CWild kwild, #2 str)
-                                                 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
+                                                 val needed = foldl (fn ((sgi, _), needed) =>
+                                                                        case sgi of
+                                                                            L'.SgiConAbs (x, _, _) => SS.add (needed, x)
+                                                                          | _ => needed)
+                                                                    SS.empty sgis
+                                                              
+                                                 val needed = foldl (fn ((d, _), needed) =>
+                                                                        case d of
+                                                                            L.DCon (x, _, _) => (SS.delete (needed, x)
+                                                                                                 handle NotFound =>
+                                                                                                        needed)
+                                                                          | L.DClass (x, _) => (SS.delete (needed, x)
+                                                                                                handle NotFound => needed)
+                                                                          | L.DOpen _ => SS.empty
+                                                                          | _ => needed)
+                                                                    needed ds
                                              in
-                                                 (L.StrConst (ds @ ds'), #2 str)
+                                                 case SS.listItems needed of
+                                                     [] => str
+                                                   | xs =>
+                                                     let
+                                                         val kwild = (L.KWild, #2 str)
+                                                         val cwild = (L.CWild kwild, #2 str)
+                                                         val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
+                                                     in
+                                                         (L.StrConst (ds @ ds'), #2 str)
+                                                     end
                                              end
-                                     end
-                                   | _ => str)
-                              | _ => str
-
-                        val (str', actual, gs2) = elabStr (env, denv) str
-                    in
-                        subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
-                        (str', formal, enD gs1 @ gs2)
-                    end
+                                           | _ => str)
+                                      | _ => str
 
-            val (env', n) = E.pushStrNamed env x sgn'
-        in
-            case #1 (hnormSgn env sgn') of
-                L'.SgnFun _ =>
-                (case #1 str' of
-                     L'.StrFun _ => ()
-                   | _ => strError env (FunctorRebind loc))
-              | _ => ();
-
-            ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
-        end
+                                val (str', actual, gs2) = elabStr (env, denv) str
+                            in
+                                subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
+                                (str', formal, enD gs1 @ gs2)
+                            end
 
-      | L.DFfiStr (x, sgn) =>
-        let
-            val (sgn', gs') = elabSgn (env, denv) sgn
+                    val (env', n) = E.pushStrNamed env x sgn'
+                in
+                    case #1 (hnormSgn env sgn') of
+                        L'.SgnFun _ =>
+                        (case #1 str' of
+                             L'.StrFun _ => ()
+                           | _ => strError env (FunctorRebind loc))
+                      | _ => ();
+
+                    ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
+                end
 
-            val (env', n) = E.pushStrNamed env x sgn'
-        in
-            ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
-        end
+              | L.DFfiStr (x, sgn) =>
+                let
+                    val (sgn', gs') = elabSgn (env, denv) sgn
 
-      | L.DOpen (m, ms) =>
-        (case E.lookupStr env m of
-             NONE => (strError env (UnboundStr (loc, m));
-                      ([], (env, denv, gs)))
-           | SOME (n, sgn) =>
-             let
-                 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
-                                          case E.projectStr env {str = str, sgn = sgn, field = m} of
-                                              NONE => (strError env (UnboundStr (loc, m));
-                                                       (strerror, sgnerror))
-                                            | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
-                                      ((L'.StrVar n, loc), sgn) ms
+                    val (env', n) = E.pushStrNamed env x sgn'
+                in
+                    ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
+                end
 
-                 val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn}
-                 val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms}
-             in
-                 (ds, (env', denv', gs))
-             end)
+              | L.DOpen (m, ms) =>
+                (case E.lookupStr env m of
+                     NONE => (strError env (UnboundStr (loc, m));
+                              ([], (env, denv, gs)))
+                   | SOME (n, sgn) =>
+                     let
+                         val (_, sgn) = foldl (fn (m, (str, sgn)) =>
+                                                  case E.projectStr env {str = str, sgn = sgn, field = m} of
+                                                      NONE => (strError env (UnboundStr (loc, m));
+                                                               (strerror, sgnerror))
+                                                    | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                                              ((L'.StrVar n, loc), sgn) ms
+
+                         val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn}
+                         val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms}
+                     in
+                         (ds, (env', denv', gs))
+                     end)
 
-      | L.DConstraint (c1, c2) =>
-        let
-            val (c1', k1, gs1) = elabCon (env, denv) c1
-            val (c2', k2, gs2) = elabCon (env, denv) c2
-            val gs3 = D.prove env denv (c1', c2', loc)
+              | L.DConstraint (c1, c2) =>
+                let
+                    val (c1', k1, gs1) = elabCon (env, denv) c1
+                    val (c2', k2, gs2) = elabCon (env, denv) c2
+                    val gs3 = D.prove env denv (c1', c2', loc)
 
-            val (denv', gs4) = D.assert env denv (c1', c2')
-        in
-            checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
-            checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
+                    val (denv', gs4) = D.assert env denv (c1', c2')
+                in
+                    checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
+                    checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
 
-            ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs))
-        end
+                    ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs))
+                end
 
-      | L.DOpenConstraints (m, ms) =>
-        let
-            val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
-        in
-            ([], (env, denv, gs))
-        end
+              | L.DOpenConstraints (m, ms) =>
+                let
+                    val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
+                in
+                    ([], (env, denv, gs))
+                end
 
-      | L.DExport str =>
-        let
-            val (str', sgn, gs') = elabStr (env, denv) str
+              | L.DExport str =>
+                let
+                    val (str', sgn, gs') = elabStr (env, denv) str
 
-            val sgn =
-                case #1 (hnormSgn env sgn) of
-                    L'.SgnConst sgis =>
-                    let
-                        fun doOne (all as (sgi, _), env) =
-                            (case sgi of
-                                 L'.SgiVal (x, n, t) =>
-                                 (case hnormCon (env, denv) t of
-                                      ((L'.TFun (dom, ran), _), []) =>
-                                      (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
-                                           (((L'.TRecord domR, _), []),
-                                            ((L'.CApp (tf, arg), _), [])) =>
-                                           (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of
-                                                (((L'.CModProj (basis, [], "transaction"), _), []),
-                                                 ((L'.CApp (tf, arg3), _), [])) =>
-                                                (case (basis = !basis_r,
-                                                       hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
-                                                     (true,
-                                                      ((L'.CApp (tf, arg2), _), []),
-                                                      (((L'.CRecord (_, []), _), []))) =>
-                                                     (case (hnormCon (env, denv) tf) of
-                                                          ((L'.CApp (tf, arg1), _), []) =>
-                                                          (case (hnormCon (env, denv) tf,
-                                                                 hnormCon (env, denv) domR,
-                                                                 hnormCon (env, denv) arg1,
-                                                                 hnormCon (env, denv) arg2) of
-                                                               ((tf, []), (domR, []), (arg1, []),
-                                                                ((L'.CRecord (_, []), _), [])) =>
-                                                               let
-                                                                   val t = (L'.CApp (tf, arg1), loc)
-                                                                   val t = (L'.CApp (t, arg2), loc)
-                                                                   val t = (L'.CApp (t, arg3), loc)
-                                                                   val t = (L'.CApp (
-                                                                            (L'.CModProj (basis, [], "transaction"), loc),
-                                                                            t), loc)
-                                                               in
-                                                                   (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc),
-                                                                                               t),
-                                                                                      loc)), loc)
-                                                               end
-                                                             | _ => all)
-                                                        | _ => all)
-                                                   | _ => all)
-                                              | _ => all)
-                                         | _ => all)
-                                    | _ => all)
-                               | _ => all,
-                             E.sgiBinds env all)
-                    in
-                        (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
-                    end
-                  | _ => sgn
-        in
-            ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
-        end
+                    val sgn =
+                        case #1 (hnormSgn env sgn) of
+                            L'.SgnConst sgis =>
+                            let
+                                fun doOne (all as (sgi, _), env) =
+                                    (case sgi of
+                                         L'.SgiVal (x, n, t) =>
+                                         (case hnormCon (env, denv) t of
+                                              ((L'.TFun (dom, ran), _), []) =>
+                                              (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
+                                                   (((L'.TRecord domR, _), []),
+                                                    ((L'.CApp (tf, arg), _), [])) =>
+                                                   (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of
+                                                        (((L'.CModProj (basis, [], "transaction"), _), []),
+                                                         ((L'.CApp (tf, arg3), _), [])) =>
+                                                        (case (basis = !basis_r,
+                                                               hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
+                                                             (true,
+                                                              ((L'.CApp (tf, arg2), _), []),
+                                                              (((L'.CRecord (_, []), _), []))) =>
+                                                             (case (hnormCon (env, denv) tf) of
+                                                                  ((L'.CApp (tf, arg1), _), []) =>
+                                                                  (case (hnormCon (env, denv) tf,
+                                                                         hnormCon (env, denv) domR,
+                                                                         hnormCon (env, denv) arg1,
+                                                                         hnormCon (env, denv) arg2) of
+                                                                       ((tf, []), (domR, []), (arg1, []),
+                                                                        ((L'.CRecord (_, []), _), [])) =>
+                                                                       let
+                                                                           val t = (L'.CApp (tf, arg1), loc)
+                                                                           val t = (L'.CApp (t, arg2), loc)
+                                                                           val t = (L'.CApp (t, arg3), loc)
+                                                                           val t = (L'.CApp (
+                                                                                    (L'.CModProj
+                                                                                         (basis, [], "transaction"), loc),
+                                                                                    t), loc)
+                                                                       in
+                                                                           (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR,
+                                                                                                        loc),
+                                                                                                       t),
+                                                                                              loc)), loc)
+                                                                       end
+                                                                     | _ => all)
+                                                                | _ => all)
+                                                           | _ => all)
+                                                      | _ => all)
+                                                 | _ => all)
+                                            | _ => all)
+                                       | _ => all,
+                                     E.sgiBinds env all)
+                            in
+                                (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
+                            end
+                          | _ => sgn
+                in
+                    ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
+                end
 
-      | L.DTable (x, c) =>
-        let
-            val (c', k, gs') = elabCon (env, denv) c
-            val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
-        in
-            checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
-            ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
-        end
+              | L.DTable (x, c) =>
+                let
+                    val (c', k, gs') = elabCon (env, denv) c
+                    val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
+                in
+                    checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
+                    ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
+                end
 
-      | L.DClass (x, c) =>
-        let
-            val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
-            val (c', ck, gs) = elabCon (env, denv) c
-            val (env, n) = E.pushCNamed env x k (SOME c')
-            val env = E.pushClass env n
-        in
-            checkKind env c' ck k;
-            ([(L'.DClass (x, n, c'), loc)], (env, denv, []))
-        end
+              | L.DClass (x, c) =>
+                let
+                    val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+                    val (c', ck, gs) = elabCon (env, denv) c
+                    val (env, n) = E.pushCNamed env x k (SOME c')
+                    val env = E.pushClass env n
+                in
+                    checkKind env c' ck k;
+                    ([(L'.DClass (x, n, c'), loc)], (env, denv, []))
+                end
+    in
+        r
+    end
 
 and elabStr (env, denv) (str, loc) =
     case str of
diff --git a/src/monoize.sml b/src/monoize.sml
index 7344c22f..5341ab99 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -614,7 +614,24 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                                            strcatComma loc (map (fn (x, _) => strcat loc [(L'.EField (gf "From", x), loc),
                                                                                           sc (" AS " ^ x)]) tables),
                                            sc " WHERE ",
-                                           gf "Where"
+                                           gf "Where",
+                                           if List.all (fn (x, xts) =>
+                                                           case List.find (fn (x', _) => x' = x) grouped of
+                                                               NONE => List.null xts
+                                                             | SOME (_, xts') =>
+                                                               List.all (fn (x, _) =>
+                                                                            List.exists (fn (x', _) => x' = x)
+                                                                                        xts') xts) tables then
+                                               sc ""
+                                           else
+                                               strcat loc [
+                                               sc " GROUP BY ",
+                                               strcatComma loc (map (fn (x, xts) =>
+                                                                        strcatComma loc
+                                                                                    (map (fn (x', _) =>
+                                                                                             sc (x ^ "." ^ x'))
+                                                                                         xts)) grouped)
+                                               ]
                               ]), loc),
                      fm)
                   | _ => poly ()
diff --git a/tests/group_by.ur b/tests/group_by.ur
index 569676d5..93655568 100644
--- a/tests/group_by.ur
+++ b/tests/group_by.ur
@@ -9,3 +9,23 @@ val q4 = (SELECT * FROM t1 WHERE t1.A = 0 GROUP BY t1.C HAVING t1.C < 0.2)
 
 val q5 = (SELECT t1.A, t2.D FROM t1, t2 GROUP BY t2.D, t1.A)
 val q6 = (SELECT t1.A, t2.D FROM t1, t2 WHERE t1.C = 0.0 GROUP BY t2.D, t1.A HAVING t1.A = t1.A AND t2.D = 17)
+
+
+datatype list a = Nil | Cons of a * list a
+
+val r1 : transaction (list {B : string}) =
+        query q1
+        (fn fs acc => return (Cons (fs.T1, acc)))
+        Nil
+
+val r2 : transaction string =
+        ls <- r1;
+        return (case ls of
+                    Nil => "Problem"
+                  | Cons ({B = b, ...}, _) => b)
+
+val main : unit -> transaction page = fn () =>
+        s <- r2;
+        return <html><body>
+                {cdata s}
+        </body></html>
diff --git a/tests/where.ur b/tests/where.ur
index ab430941..8b4d89c5 100644
--- a/tests/where.ur
+++ b/tests/where.ur
@@ -9,3 +9,22 @@ val q5 = (SELECT * FROM t1 WHERE {1} = {1})
 val q6 = (SELECT * FROM t1 WHERE {"Hi"} < {"Bye"})
 val q7 = (SELECT * FROM t1 WHERE {1} <> {1} AND NOT ({"Hi"} >= {"Bye"}))
 val q8 = (SELECT * FROM t1 WHERE t1.A = 1 OR t1.C < 3.0)
+
+datatype list a = Nil | Cons of a * list a
+
+val r1 : transaction (list {A : int, B : string, C : float}) =
+        query q8
+        (fn fs acc => return (Cons (fs.T1, acc)))
+        Nil
+
+val r2 : transaction string =
+        ls <- r1;
+        return (case ls of
+                    Nil => "Problem"
+                  | Cons ({B = b, ...}, _) => b)
+
+val main : unit -> transaction page = fn () =>
+        s <- r2;
+        return <html><body>
+                {cdata s}
+        </body></html>