Mutual datatypes through Elaborate

9 files changed, 493 insertions, 344 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 555cc25c..de2db500 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -132,7 +132,7 @@ withtype exp = exp' located
 datatype sgn_item' =
          SgiConAbs of string * int * kind
        | SgiCon of string * int * kind * con
-       | SgiDatatype of string * int * string list * (string * int * con option) list
+       | SgiDatatype of (string * int * string list * (string * int * con option) list) list
        | SgiDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
        | SgiVal of string * int * con
        | SgiStr of string * int * sgn
@@ -154,7 +154,7 @@ and sgn = sgn' located
 
 datatype decl' =
          DCon of string * int * kind * con
-       | DDatatype of string * int * string list * (string * int * con option) list
+       | DDatatype of (string * int * string list * (string * int * con option) list) list
        | DDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
        | DVal of string * int * con * exp
        | DValRec of (string * int * con * exp) list
diff --git a/src/elab_env.sml b/src/elab_env.sml
index efc2b74e..88b2554b 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -909,7 +909,7 @@ fun sgiSeek (sgi, (sgns, strs, cons)) =
     case sgi of
         SgiConAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
       | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
-      | SgiDatatype (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
+      | SgiDatatype dts => (sgns, strs, foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts)
       | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x))
       | SgiVal _ => (sgns, strs, cons)
       | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
@@ -929,7 +929,7 @@ fun sgnSeek f sgis =
                     let
                         val cons =
                             case sgi of
-                                SgiDatatype (x, n, _, _) => IM.insert (cons, n, x)
+                                SgiDatatype dts => foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts
                               | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x)
                               | _ => cons
                     in
@@ -1209,26 +1209,31 @@ fun sgiBinds env (sgi, loc) =
     case sgi of
         SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
       | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
-      | SgiDatatype (x, n, xs, xncs) =>
+      | SgiDatatype dts =>
         let
-            val k = (KType, loc)
-            val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
+            fun doOne ((x, n, xs, xncs), env) =
+                let
+                    val k = (KType, loc)
+                    val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
 
-            val env = pushCNamedAs env x n k' NONE
-        in
-            foldl (fn ((x', n', to), env) =>
-                      let
-                          val t =
-                              case to of
-                                  NONE => (CNamed n, loc)
-                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
+                    val env = pushCNamedAs env x n k' NONE
+                in
+                    foldl (fn ((x', n', to), env) =>
+                              let
+                                  val t =
+                                      case to of
+                                          NONE => (CNamed n, loc)
+                                        | SOME t => (TFun (t, (CNamed n, loc)), loc)
 
-                          val k = (KType, loc)
-                          val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
-                      in
-                          pushENamedAs env x' n' t
-                      end)
-            env xncs
+                                  val k = (KType, loc)
+                                  val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
+                              in
+                                  pushENamedAs env x' n' t
+                              end)
+                          env xncs
+                end
+        in
+            foldl doOne env dts
         end
       | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
         let
@@ -1288,16 +1293,16 @@ fun projectCon env {sgn, str, field} =
         SgnConst sgis =>
         (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
                         | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
-                        | SgiDatatype (x, _, xs, _) =>
-                          if x = field then
-                              let
-                                  val k = (KType, #2 sgn)
-                                  val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
-                              in
-                                  SOME (k', NONE)
-                              end
-                          else
-                              NONE
+                        | SgiDatatype dts =>
+                          (case List.find (fn (x, _, xs, _) => x = field) dts of
+                               SOME (_, _, xs, _) =>
+                               let
+                                   val k = (KType, #2 sgn)
+                                   val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
+                               in
+                                   SOME (k', NONE)
+                                   end
+                             | NONE => NONE)
                         | SgiDatatypeImp (x, _, m1, ms, x', xs, _) =>
                           if x = field then
                               let
@@ -1325,7 +1330,10 @@ fun projectCon env {sgn, str, field} =
 fun projectDatatype env {sgn, str, field} =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
-        (case sgnSeek (fn SgiDatatype (x, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
+        (case sgnSeek (fn SgiDatatype dts =>
+                          (case List.find (fn (x, _, _, _) => x = field) dts of
+                               SOME (_, _, xs, xncs) => SOME (xs, xncs)
+                             | NONE => NONE)
                         | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
                         | _ => NONE) sgis of
              NONE => NONE
@@ -1344,7 +1352,18 @@ fun projectConstructor env {sgn, str, field} =
                                     else
                                         SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs
         in
-            case sgnSeek (fn SgiDatatype (_, n, xs, xncs) => consider (n, xs, xncs)
+            case sgnSeek (fn SgiDatatype dts =>
+                             let
+                                 fun search dts =
+                                     case dts of
+                                         [] => NONE
+                                       | (_, n, xs, xncs) :: dts =>
+                                         case consider (n, xs, xncs) of
+                                             NONE => search dts
+                                           | v => v
+                             in
+                                 search dts
+                             end
                            | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs)
                            | _ => NONE) sgis of
                 NONE => NONE
@@ -1382,7 +1401,18 @@ fun projectVal env {sgn, str, field} =
                                         NONE) xncs
         in
             case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
-                           | SgiDatatype (_, n, xs, xncs) => seek (n, xs, xncs)
+                           | SgiDatatype dts =>
+                             let
+                                 fun search dts =
+                                     case dts of
+                                         [] => NONE
+                                       | (_, n, xs, xncs) :: dts =>
+                                         case seek (n, xs, xncs) of
+                                             NONE => search dts
+                                           | v => v
+                             in
+                                 search dts
+                             end
                            | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs)
                            | _ => NONE) sgis of
                 NONE => NONE
@@ -1406,7 +1436,8 @@ fun sgnSeekConstraints (str, sgis) =
                     end
                   | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
                   | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
-                  | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+                  | SgiDatatype dts => seek (sgis, sgns, strs,
+                                             foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts, acc)
                   | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
                   | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
                   | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
@@ -1431,29 +1462,34 @@ fun edeclBinds env (d, loc) =
 fun declBinds env (d, loc) =
     case d of
         DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
-      | DDatatype (x, n, xs, xncs) =>
+      | DDatatype dts =>
         let
-            val k = (KType, loc) 
-            val nxs = length xs
-            val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
-                                               ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
-                                                (KArrow (k, kb), loc)))
-                                           ((CNamed n, loc), k) xs
-                                              
-            val env = pushCNamedAs env x n kb NONE
-            val env = pushDatatype env n xs xncs
+            fun doOne ((x, n, xs, xncs), env) =
+                let
+                    val k = (KType, loc) 
+                    val nxs = length xs
+                    val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
+                                                       ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
+                                                        (KArrow (k, kb), loc)))
+                                                   ((CNamed n, loc), k) xs
+                                   
+                    val env = pushCNamedAs env x n kb NONE
+                    val env = pushDatatype env n xs xncs
+                in
+                    foldl (fn ((x', n', to), env) =>
+                              let
+                                  val t =
+                                      case to of
+                                          NONE => tb
+                                        | SOME t => (TFun (t, tb), loc)
+                                  val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
+                              in
+                                  pushENamedAs env x' n' t
+                              end)
+                          env xncs
+                end
         in
-            foldl (fn ((x', n', to), env) =>
-                      let
-                          val t =
-                              case to of
-                                  NONE => tb
-                                | SOME t => (TFun (t, tb), loc)
-                          val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
-                      in
-                          pushENamedAs env x' n' t
-                      end)
-                  env xncs
+            foldl doOne env dts
         end
       | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
         let
diff --git a/src/elab_print.sml b/src/elab_print.sml
index bbbd9f8d..ab38c2e1 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -486,9 +486,7 @@ fun p_datatype env (x, n, xs, cons) =
         val env = E.pushCNamedAs env x n k NONE
         val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
     in
-        box [string "datatype",
-             space,
-             string x,
+        box [string x,
              p_list_sep (box []) (fn x => box [space, string x]) xs,
              space,
              string "=",
@@ -507,7 +505,7 @@ fun p_named x n =
     else
         string x
 
-fun p_sgn_item env (sgi, _) =
+fun p_sgn_item env (sgiAll as (sgi, _)) =
     case sgi of
         SgiConAbs (x, n, k) => box [string "con",
                                     space,
@@ -527,7 +525,9 @@ fun p_sgn_item env (sgi, _) =
                                     string "=",
                                     space,
                                     p_con env c]
-      | SgiDatatype x => p_datatype env x
+      | SgiDatatype x => box [string "datatype",
+                              space,
+                              p_list_sep (box [space, string "and", space]) (p_datatype (E.sgiBinds env sgiAll)) x]
       | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
@@ -669,7 +669,9 @@ fun p_decl env (dAll as (d, _) : decl) =
                                   string "=",
                                   space,
                                   p_con env c]
-      | DDatatype x => p_datatype env x
+      | DDatatype x => box [string "datatype",
+                            space,
+                            p_list_sep (box [space, string "and", space]) (p_datatype (E.declBinds env dAll)) x]
       | DDatatypeImp (x, _, m1, ms, x', _, _) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 51a203f2..036aa867 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -568,15 +568,17 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                         S.map2 (con ctx c,
                              fn c' =>
                                 (SgiCon (x, n, k', c'), loc)))
-              | SgiDatatype (x, n, xs, xncs) =>
-                S.map2 (ListUtil.mapfold (fn (x, n, c) =>
-                                             case c of
-                                                 NONE => S.return2 (x, n, c)
-                                               | SOME c =>
-                                                 S.map2 (con ctx c,
-                                                      fn c' => (x, n, SOME c'))) xncs,
-                        fn xncs' =>
-                           (SgiDatatype (x, n, xs, xncs'), loc))
+              | SgiDatatype dts =>
+                S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
+                                             S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+                                                                          case c of
+                                                                              NONE => S.return2 (x, n, c)
+                                                                            | SOME c =>
+                                                                              S.map2 (con ctx c,
+                                                                                   fn c' => (x, n, SOME c'))) xncs,
+                                                  fn xncs' => (x, n, xs, xncs'))) dts,
+                        fn dts' =>
+                           (SgiDatatype dts', loc))
               | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
                 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
                                              case c of
@@ -627,8 +629,15 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                    bind (ctx, NamedC (x, n, k, NONE))
                                                  | SgiCon (x, n, k, c) =>
                                                    bind (ctx, NamedC (x, n, k, SOME c))
-                                                 | SgiDatatype (x, n, _, xncs) =>
-                                                   bind (ctx, NamedC (x, n, (KType, loc), NONE))
+                                                 | SgiDatatype dts =>
+                                                   foldl (fn ((x, n, ks, _), ctx) =>
+                                                             let
+                                                                 val k' = (KType, loc)
+                                                                 val k = foldl (fn (_, k) => (KArrow (k', k), loc))
+                                                                               k' ks
+                                                             in
+                                                                 bind (ctx, NamedC (x, n, k, NONE))
+                                                             end) ctx dts
                                                  | SgiDatatypeImp (x, n, m1, ms, s, _, _) =>
                                                    bind (ctx, NamedC (x, n, (KType, loc),
                                                                       SOME (CModProj (m1, ms, s), loc)))
@@ -753,29 +762,34 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                               (case #1 d of
                                                    DCon (x, n, k, c) =>
                                                    bind (ctx, NamedC (x, n, k, SOME c))
-                                                 | DDatatype (x, n, xs, xncs) =>
+                                                 | DDatatype dts =>
                                                    let
-                                                       val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE))
+                                                       fun doOne ((x, n, xs, xncs), ctx) =
+                                                           let
+                                                               val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE))
+                                                           in
+                                                               foldl (fn ((x, _, co), ctx) =>
+                                                                         let
+                                                                             val t =
+                                                                                 case co of
+                                                                                     NONE => CNamed n
+                                                                                   | SOME t => TFun (t, (CNamed n, loc))
+                                                                                               
+                                                                             val k = (KType, loc)
+                                                                             val t = (t, loc)
+                                                                             val t = foldr (fn (x, t) =>
+                                                                                               (TCFun (Explicit,
+                                                                                                       x,
+                                                                                                       k,
+                                                                                                       t), loc))
+                                                                                           t xs
+                                                                         in
+                                                                             bind (ctx, NamedE (x, t))
+                                                                         end)
+                                                                     ctx xncs
+                                                           end
                                                    in
-                                                       foldl (fn ((x, _, co), ctx) =>
-                                                                 let
-                                                                     val t =
-                                                                         case co of
-                                                                             NONE => CNamed n
-                                                                           | SOME t => TFun (t, (CNamed n, loc))
-
-                                                                     val k = (KType, loc)
-                                                                     val t = (t, loc)
-                                                                     val t = foldr (fn (x, t) =>
-                                                                                       (TCFun (Explicit,
-                                                                                               x,
-                                                                                               k,
-                                                                                               t), loc))
-                                                                             t xs
-                                                                 in
-                                                                     bind (ctx, NamedE (x, t))
-                                                                 end)
-                                                       ctx xncs
+                                                       foldl doOne ctx dts
                                                    end
                                                  | DDatatypeImp (x, n, m, ms, x', _, _) =>
                                                    bind (ctx, NamedC (x, n, (KType, loc),
@@ -851,15 +865,18 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                             S.map2 (mfc ctx c,
                                     fn c' =>
                                        (DCon (x, n, k', c'), loc)))
-              | DDatatype (x, n, xs, xncs) =>
-                S.map2 (ListUtil.mapfold (fn (x, n, c) =>
-                                             case c of
-                                                 NONE => S.return2 (x, n, c)
-                                               | SOME c =>
-                                                 S.map2 (mfc ctx c,
-                                                      fn c' => (x, n, SOME c'))) xncs,
-                        fn xncs' =>
-                           (DDatatype (x, n, xs, xncs'), loc))
+              | DDatatype dts =>
+                S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
+                                             S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+                                                                          case c of
+                                                                              NONE => S.return2 (x, n, c)
+                                                                            | SOME c =>
+                                                                              S.map2 (mfc ctx c,
+                                                                                   fn c' => (x, n, SOME c'))) xncs,
+                                                     fn xncs' =>
+                                                        (x, n, xs, xncs'))) dts,
+                     fn dts' =>
+                        (DDatatype dts', loc))
               | DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
                 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
                                              case c of
@@ -1059,9 +1076,10 @@ fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds
 and maxNameDecl (d, _) =
     case d of
         DCon (_, n, _, _) => n
-      | DDatatype (_, n, _, ns) =>
+      | DDatatype dts =>
+        foldl (fn ((_, n, _, ns), max) =>
                   foldl (fn ((_, n', _), m) => Int.max (n', m))
-                        n ns
+                        (Int.max (n, max)) ns) 0 dts
       | DDatatypeImp (_, n1, n2, _, _, _, ns) =>
         foldl (fn ((_, n', _), m) => Int.max (n', m))
               (Int.max (n1, n2)) ns
@@ -1101,9 +1119,10 @@ and maxNameSgi (sgi, _) =
     case sgi of
         SgiConAbs (_, n, _) => n
       | SgiCon (_, n, _, _) => n
-      | SgiDatatype (_, n, _, ns) =>
-        foldl (fn ((_, n', _), m) => Int.max (n', m))
-              n ns
+      | SgiDatatype dts =>
+        foldl (fn ((_, n, _, ns), max) =>
+                  foldl (fn ((_, n', _), m) => Int.max (n', m))
+                        (Int.max (n, max)) ns) 0 dts
       | SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
         foldl (fn ((_, n', _), m) => Int.max (n', m))
               (Int.max (n1, n2)) ns
diff --git a/src/elaborate.sml b/src/elaborate.sml
index f91f83c7..8b23d91e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1971,47 +1971,65 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
         end
 
-      | L.SgiDatatype (x, xs, xcs) =>
+      | L.SgiDatatype dts =>
         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), gs' @ gs)
-                                           end
-                        val t = foldl (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
+            val (dts, env) = ListUtil.foldlMap (fn ((x, xs, xcs), env) =>
+                                                   let
+                                                       val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+                                                       val (env, n) = E.pushCNamed env x k' NONE
+                                                   in
+                                                       ((x, n, xs, xcs), env)
+                                                   end)
+                             env dts
+
+            val (dts, env) = ListUtil.foldlMap
+                             (fn ((x, n, xs, xcs), env) =>
+                                 let
+                                     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),
+                                                                                 gs' @ gs)
+                                                                            end
+                                                     val t = foldl (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
+                                 in
+                                     ((x, n, xs, xcs), E.pushDatatype env n xs xcs)
+                                 end)
+                             env dts
         in
-            ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
+            ([(L'.SgiDatatype dts, loc)], (env, denv, gs))
         end
 
       | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp"
@@ -2199,21 +2217,31 @@ and elabSgn (env, denv) (sgn, loc) =
                                    else
                                        ();
                                    (SS.add (cons, x), vals, sgns, strs))
-                                | L'.SgiDatatype (x, _, _, xncs) =>
+                                | L'.SgiDatatype dts =>
                                   let
-                                      val vals = foldl (fn ((x, _, _), vals) =>
-                                                           (if SS.member (vals, x) then
-                                                                sgnError env (DuplicateVal (loc, x))
-                                                            else
-                                                                ();
-                                                            SS.add (vals, x)))
-                                                       vals xncs
+                                      val (cons, vals) =
+                                          let
+                                              fun doOne ((x, _, _, xncs), (cons, vals)) =
+                                                  let
+                                                      val vals = foldl (fn ((x, _, _), vals) =>
+                                                                           (if SS.member (vals, x) then
+                                                                                sgnError env (DuplicateVal (loc, x))
+                                                                            else
+                                                                                ();
+                                                                            SS.add (vals, x)))
+                                                                       vals xncs
+                                                  in
+                                                      if SS.member (cons, x) then
+                                                          sgnError env (DuplicateCon (loc, x))
+                                                      else
+                                                          ();
+                                                      (SS.add (cons, x), vals)
+                                                  end
+                                          in
+                                              foldl doOne (cons, vals) dts
+                                          end
                                   in
-                                      if SS.member (cons, x) then
-                                          sgnError env (DuplicateCon (loc, x))
-                                      else
-                                          ();
-                                      (SS.add (cons, x), vals, sgns, strs)
+                                      (cons, vals, sgns, strs)
                                   end
                                 | L'.SgiDatatypeImp (x, _, _, _, _, _, _) =>
                                   (if SS.member (cons, x) then
@@ -2318,15 +2346,15 @@ and selfify env {str, strs, sgn} =
       | L'.SgnVar _ => sgn
 
       | L'.SgnConst sgis =>
-        (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
-                              (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
-                            | (L'.SgiDatatype (x, n, xs, xncs), loc) =>
-                              (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
+        (L'.SgnConst (ListUtil.mapConcat (fn (L'.SgiConAbs (x, n, k), loc) =>
+                              [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
+                            | (L'.SgiDatatype dts, loc) =>
+                              map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts
                             | (L'.SgiClassAbs (x, n, k), loc) =>
-                              (L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
+                              [(L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
                             | (L'.SgiStr (x, n, sgn), loc) =>
-                              (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
-                            | x => x) sgis), #2 sgn)
+                              [(L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)]
+                            | x => [x]) sgis), #2 sgn)
       | L'.SgnFun _ => sgn
       | L'.SgnWhere _ => sgn
       | L'.SgnProj (m, ms, x) =>
@@ -2360,46 +2388,47 @@ and dopen env {str, strs, sgn} =
     in
         case #1 (hnormSgn env sgn) of
             L'.SgnConst sgis =>
-            ListUtil.foldlMap (fn ((sgi, loc), env') =>
-                                  let
-                                      val d =
-                                          case sgi of
-                                              L'.SgiConAbs (x, n, k) =>
-                                              let
-                                                  val c = (L'.CModProj (str, strs, x), loc)
-                                              in
-                                                  (L'.DCon (x, n, k, c), loc)
-                                              end
-                                            | L'.SgiCon (x, n, k, c) =>
-                                              (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
-                                            | L'.SgiDatatype (x, n, xs, xncs) =>
-                                              (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
-                                            | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
-                                              (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)
-                                            | L'.SgiVal (x, n, t) =>
-                                              (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)
-                                            | L'.SgiStr (x, n, sgn) =>
-                                              (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
-                                            | L'.SgiSgn (x, n, sgn) =>
-                                              (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
-                                            | L'.SgiConstraint (c1, c2) =>
-                                              (L'.DConstraint (c1, c2), loc)
-                                            | L'.SgiClassAbs (x, n, k) =>
-                                              let
-                                                  val c = (L'.CModProj (str, strs, x), loc)
-                                              in
-                                                  (L'.DCon (x, n, k, c), loc)
-                                              end
-                                            | L'.SgiClass (x, n, k, _) =>
-                                              let
-                                                  val c = (L'.CModProj (str, strs, x), loc)
-                                              in
-                                                  (L'.DCon (x, n, k, c), loc)
-                                              end
-                                  in
-                                      (d, E.declBinds env' d)
-                                  end)
-                              env sgis
+            ListUtil.foldlMapConcat
+                (fn ((sgi, loc), env') =>
+                    let
+                        val d =
+                            case sgi of
+                                L'.SgiConAbs (x, n, k) =>
+                                let
+                                    val c = (L'.CModProj (str, strs, x), loc)
+                                in
+                                    [(L'.DCon (x, n, k, c), loc)]
+                                end
+                              | L'.SgiCon (x, n, k, c) =>
+                                [(L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
+                              | L'.SgiDatatype dts =>
+                                map (fn (x, n, xs, xncs) => (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts
+                              | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
+                                [(L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)]
+                              | L'.SgiVal (x, n, t) =>
+                                [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)]
+                              | L'.SgiStr (x, n, sgn) =>
+                                [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)]
+                              | L'.SgiSgn (x, n, sgn) =>
+                                [(L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)]
+                              | L'.SgiConstraint (c1, c2) =>
+                                [(L'.DConstraint (c1, c2), loc)]
+                              | L'.SgiClassAbs (x, n, k) =>
+                                let
+                                    val c = (L'.CModProj (str, strs, x), loc)
+                                in
+                                    [(L'.DCon (x, n, k, c), loc)]
+                                end
+                              | L'.SgiClass (x, n, k, _) =>
+                                let
+                                    val c = (L'.CModProj (str, strs, x), loc)
+                                in
+                                    [(L'.DCon (x, n, k, c), loc)]
+                                end
+                    in
+                        (d, foldl (fn (d, env') => E.declBinds env' d) env' d)
+                    end)
+                env sgis
           | _ => (strError env (UnOpenable sgn);
                   ([], env))
     end
@@ -2445,12 +2474,11 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
                 let
                     (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*)
 
-                    fun seek p =
+                    fun seek' f p =
                         let
                             fun seek env ls =
                                 case ls of
-                                    [] => (sgnError env (UnmatchedSgi sgi2All);
-                                           env)
+                                    [] => f env
                                   | h :: t =>
                                     case p (env, h) of
                                         NONE =>
@@ -2474,6 +2502,9 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
                         in
                             seek env sgis1
                         end
+
+                    val seek = seek' (fn env => (sgnError env (UnmatchedSgi sgi2All);
+                                                 env))
                 in
                     case sgi of
                         L'.SgiConAbs (x, n2, k2) =>
@@ -2498,12 +2529,23 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
                                      case sgi1 of
                                          L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
                                        | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
-                                       | L'.SgiDatatype (x', n1, xs, _) =>
+                                       | L'.SgiDatatype dts =>
                                          let
                                              val k = (L'.KType, loc)
-                                             val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+
+                                             fun search dts =
+                                                 case dts of
+                                                     [] => NONE
+                                                   | (x', n1, xs, _) :: dts =>
+                                                     let
+                                                         val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+                                                     in
+                                                         case found (x', n1, k', NONE) of
+                                                             NONE => search dts
+                                                           | x => x
+                                                     end
                                          in
-                                             found (x', n1, k', NONE)
+                                             search dts
                                          end
                                        | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) =>
                                          let
@@ -2549,66 +2591,93 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
                                        | _ => NONE
                                  end)
 
-                      | L'.SgiDatatype (x, n2, xs2, xncs2) =>
-                        seek (fn (env, sgi1All as (sgi1, _)) =>
-                                 let
-                                     fun found (n1, xs1, xncs1) =
-                                         let
-                                             fun mismatched ue =
-                                                 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
-                                                  SOME env)
-
-                                             val k = (L'.KType, loc)
-                                             val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
+                      | L'.SgiDatatype dts2 =>
+                        let
+                            fun found' (sgi1All, (x1, n1, xs1, xncs1), (x2, n2, xs2, xncs2), env) =
+                                if x1 <> x2 then
+                                    NONE
+                                else
+                                    let
+                                        fun mismatched ue =
+                                            (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
+                                             SOME env)
 
-                                             fun good () =
-                                                 let
-                                                     val env = E.sgiBinds env sgi1All
-                                                     val env = if n1 = n2 then
-                                                                   env
-                                                               else
-                                                                   E.pushCNamedAs env x n2 k'
-                                                                                  (SOME (L'.CNamed n1, loc))
-                                                 in
-                                                     SOME env
-                                                 end
+                                        val k = (L'.KType, loc)
+                                        val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
 
-                                             val env = E.pushCNamedAs env x n1 k' NONE
-                                             val env = if n1 = n2 then
-                                                           env
-                                                       else
-                                                           E.pushCNamedAs env x n2 k' (SOME (L'.CNamed n1, loc))
-                                             val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
-                                             fun xncBad ((x1, _, t1), (x2, _, t2)) =
-                                                 String.compare (x1, x2) <> EQUAL
-                                                 orelse case (t1, t2) of
-                                                            (NONE, NONE) => false
-                                                          | (SOME t1, SOME t2) =>
-                                                            (unifyCons env t1 t2; false)
-                                                          | _ => true
-                                         in
-                                             (if xs1 <> xs2
-                                                 orelse length xncs1 <> length xncs2
-                                                 orelse ListPair.exists xncBad (xncs1, xncs2) then
-                                                  mismatched NONE
-                                              else
-                                                  good ())
-                                             handle CUnify ue => mismatched (SOME ue)
-                                         end
-                                 in
-                                     case sgi1 of
-                                         L'.SgiDatatype (x', n1, xs, xncs1) =>
-                                         if x' = x then
-                                             found (n1, xs, xncs1)
-                                         else
-                                             NONE
-                                       | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) =>
-                                         if x' = x then
-                                             found (n1, xs, xncs1)
+                                        fun good () =
+                                            let
+                                                val env = E.sgiBinds env sgi1All
+                                                val env = if n1 = n2 then
+                                                              env
+                                                          else
+                                                              E.pushCNamedAs env x1 n2 k'
+                                                                             (SOME (L'.CNamed n1, loc))
+                                            in
+                                                SOME env
+                                            end
+
+                                        val env = E.pushCNamedAs env x1 n1 k' NONE
+                                        val env = if n1 = n2 then
+                                                      env
+                                                  else
+                                                      E.pushCNamedAs env x1 n2 k' (SOME (L'.CNamed n1, loc))
+                                        val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
+                                        fun xncBad ((x1, _, t1), (x2, _, t2)) =
+                                            String.compare (x1, x2) <> EQUAL
+                                            orelse case (t1, t2) of
+                                                       (NONE, NONE) => false
+                                                     | (SOME t1, SOME t2) =>
+                                                       (unifyCons env t1 t2; false)
+                                                     | _ => true
+                                    in
+                                        (if xs1 <> xs2
+                                            orelse length xncs1 <> length xncs2
+                                            orelse ListPair.exists xncBad (xncs1, xncs2) then
+                                             mismatched NONE
                                          else
-                                             NONE
-                                       | _ => NONE
-                                 end)
+                                             good ())
+                                        handle CUnify ue => mismatched (SOME ue)
+                                    end
+                        in
+                            seek'
+                                (fn _ =>
+                                    let
+                                        fun seekOne (dt2, env) =
+                                            seek (fn (env, sgi1All as (sgi1, _)) =>
+                                                     case sgi1 of
+                                                         L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) =>
+                                                         found' (sgi1All, (x', n1, xs, xncs1), dt2, env)
+                                                       | _ => NONE)
+
+                                        fun seekAll (dts, env) =
+                                            case dts of
+                                                [] => env
+                                              | dt :: dts => seekAll (dts, seekOne (dt, env))
+                                    in
+                                        seekAll (dts2, env)
+                                    end)
+                                (fn (env, sgi1All as (sgi1, _)) =>
+                                    let
+                                        fun found dts1 =
+                                            let
+                                                fun iter (dts1, dts2, env) =
+                                                    case (dts1, dts2) of
+                                                        ([], []) => SOME env
+                                                      | (dt1 :: dts1, dt2 :: dts2) =>
+                                                        (case found' (sgi1All, dt1, dt2, env) of
+                                                             NONE => NONE
+                                                           | SOME env => iter (dts1, dts2, env))
+                                                      | _ => NONE
+                                            in
+                                                iter (dts1, dts2, env)
+                                            end
+                                    in
+                                        case sgi1 of
+                                            L'.SgiDatatype dts1 => found dts1
+                                          | _ => NONE
+                                    end)
+                        end
 
                       | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) =>
                         seek (fn (env, sgi1All as (sgi1, _)) =>
@@ -3033,58 +3102,63 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
 
                     ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
                 end
-              | L.DDatatype (x, xs, xcs) =>
+              | L.DDatatype dts =>
                 let
-                    val positive = List.all (fn (_, to) =>
-                                                case to of
-                                                    NONE => true
-                                                  | SOME t => positive x t) xcs
-
                     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
-                    val d' = (L'.DDatatype (x, n, xs, xcs), loc)
-                in
-                    (*if positive then
-                        ()
-                    else
-                        declError env (Nonpositive d');*)
+                    val (dts, env) = ListUtil.foldlMap
+                                     (fn ((x, xs, xcs), env) =>
+                                         let
+                                             val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+                                             val (env, n) = E.pushCNamed env x k' NONE
+                                         in
+                                             ((x, n, xs, xcs), env)
+                                         end)
+                                     env dts
 
-                    ([d'], (env, denv, gs' @ gs))
+                    val (dts, (env, gs')) = ListUtil.foldlMap
+                                     (fn ((x, n, xs, xcs), (env, gs')) =>
+                                         let
+                                             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, gs') xcs
+                                         in
+                                             ((x, n, xs, xcs), (E.pushDatatype env n xs xcs, gs'))
+                                         end)
+                                     (env, []) dts
+                in
+                    ([(L'.DDatatype dts, loc)], (env, denv, gs' @ gs))
                 end
 
               | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
@@ -3484,24 +3558,31 @@ and elabStr (env, denv) (str, loc) =
                               in
                                   ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
                               end
-                            | L'.SgiDatatype (x, n, xs, xncs) =>
+                            | L'.SgiDatatype dts =>
                               let
-                                  val (cons, x) =
-                                      if SS.member (cons, x) then
-                                          (cons, "?" ^ x)
-                                      else
-                                          (SS.add (cons, x), x)
-
-                                  val (xncs, vals) =
-                                      ListUtil.foldlMap
-                                          (fn ((x, n, t), vals) =>
-                                              if SS.member (vals, x) then
-                                                  (("?" ^ x, n, t), vals)
+                                  fun doOne ((x, n, xs, xncs), (cons, vals)) =
+                                      let
+                                          val (cons, x) =
+                                              if SS.member (cons, x) then
+                                                  (cons, "?" ^ x)
                                               else
-                                                  ((x, n, t), SS.add (vals, x)))
-                                      vals xncs
+                                                  (SS.add (cons, x), x)
+                                                  
+                                          val (xncs, vals) =
+                                              ListUtil.foldlMap
+                                                  (fn ((x, n, t), vals) =>
+                                                      if SS.member (vals, x) then
+                                                          (("?" ^ x, n, t), vals)
+                                                      else
+                                                          ((x, n, t), SS.add (vals, x)))
+                                                  vals xncs
+                                      in
+                                          ((x, n, xs, xncs), (cons, vals))
+                                      end
+
+                                  val (dts, (cons, vals)) = ListUtil.foldlMap doOne (cons, vals) dts
                               in
-                                  ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
+                                  ((L'.SgiDatatype dts, loc) :: sgis, cons, vals, sgns, strs)
                               end
                             | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
                               let
diff --git a/src/explify.sml b/src/explify.sml
index 2e181771..145fccd2 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -137,9 +137,10 @@ fun explifySgi (sgi, loc) =
     case sgi of
         L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)
       | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
-      | L.SgiDatatype (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs,
+      (*| L.SgiDatatype (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs,
                                                                 map (fn (x, n, co) =>
-                                                                        (x, n, Option.map explifyCon co)) xncs), loc)
+                                                                        (x, n, Option.map explifyCon co)) xncs), loc)*)
+      | L.SgiDatatype _ => raise Fail "Explify SgiDatatype"
       | L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
         SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, xs, map (fn (x, n, co) =>
                                                               (x, n, Option.map explifyCon co)) xncs), loc)
@@ -163,9 +164,10 @@ and explifySgn (sgn, loc) =
 fun explifyDecl (d, loc : EM.span) =
     case d of
         L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
-      | L.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs,
+      (*| L.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs,
                                                             map (fn (x, n, co) =>
-                                                                    (x, n, Option.map explifyCon co)) xncs), loc)
+                                                                    (x, n, Option.map explifyCon co)) xncs), loc)*)
+      | L.DDatatype _ => raise Fail "Explify DDatatype"
       | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
         SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs,
                                map (fn (x, n, co) =>
diff --git a/src/source.sml b/src/source.sml
index 9d3eea79..0f62cadd 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -85,7 +85,7 @@ datatype inference =
 datatype sgn_item' =
          SgiConAbs of string * kind
        | SgiCon of string * kind option * con
-       | SgiDatatype of string * string list * (string * con option) list
+       | SgiDatatype of (string * string list * (string * con option) list) list
        | SgiDatatypeImp of string * string list * string
        | SgiVal of string * con
        | SgiTable of string * con * exp * exp
@@ -148,7 +148,7 @@ and edecl = edecl' located
 
 datatype decl' =
          DCon of string * kind option * con
-       | DDatatype of string * string list * (string * con option) list
+       | DDatatype of (string * string list * (string * con option) list) list
        | DDatatypeImp of string * string list * string
        | DVal of string * con option * exp
        | DValRec of (string * con option * exp) list
diff --git a/src/source_print.sml b/src/source_print.sml
index 0f8b093b..b4f9bfd3 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -360,9 +360,7 @@ and p_vali (x, co, e) =
 
 
 fun p_datatype (x, xs, cons) =
-    box [string "datatype",
-         space,
-         string x,
+    box [string x,
          p_list_sep (box []) (fn x => box [space, string x]) xs,
          space,
          string "=",
@@ -399,7 +397,9 @@ fun p_sgn_item (sgi, _) =
                                       string "=",
                                       space,
                                       p_con c]
-      | SgiDatatype x => p_datatype x
+      | SgiDatatype x => box [string "datatype",
+                              space,
+                              p_list_sep (box [space, string "and", space]) p_datatype x]
       | SgiDatatypeImp (x, ms, x') =>
         box [string "datatype",
              space,
@@ -530,7 +530,9 @@ fun p_decl ((d, _) : decl) =
                                     string "=",
                                     space,
                                     p_con c]
-      | DDatatype x => p_datatype x
+      | DDatatype x => box [string "datatype",
+                            space,
+                            p_list_sep (box [space, string "and", space]) p_datatype x]
       | DDatatypeImp (x, ms, x') =>
         box [string "datatype",
              space,
diff --git a/src/urweb.grm b/src/urweb.grm
index 4697fef7..bd834b47 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -226,6 +226,8 @@ datatype attr = Class of exp | Normal of con * exp
  | dargs of string list
  | barOpt of unit
  | dcons of (string * con option) list
+ | dtype of string * string list * (string * con option) list
+ | dtypes of (string * string list * (string * con option) list) list
  | dcon of string * con option
 
  | pkopt of exp
@@ -394,7 +396,7 @@ decl   : CON SYMBOL cargl2 kopt EQ cexp (let
                                          end)
        | LTYPE SYMBOL EQ cexp           ([(DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                            s (LTYPEleft, cexpright))])
-       | DATATYPE SYMBOL dargs EQ barOpt dcons([(DDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))])
+       | DATATYPE dtypes                ([(DDatatype dtypes, s (DATATYPEleft, dtypesright))])
        | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
                 (case dargs of
                      [] => [(DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))]
@@ -464,6 +466,11 @@ decl   : CON SYMBOL cargl2 kopt EQ cexp (let
        | COOKIE SYMBOL COLON cexp       ([(DCookie (SYMBOL, cexp), s (COOKIEleft, cexpright))])
        | STYLE SYMBOL                   ([(DStyle SYMBOL, s (STYLEleft, SYMBOLright))])
 
+dtype  : SYMBOL dargs EQ barOpt dcons   (SYMBOL, dargs, dcons)
+
+dtypes : dtype                          ([dtype])
+       | dtype AND dtypes               (dtype :: dtypes)
+
 kopt   :                                (NONE)
        | DCOLON kind                    (SOME kind)
 
@@ -652,7 +659,7 @@ sgi    : CON SYMBOL DCOLON kind         ((SgiConAbs (SYMBOL, kind), s (CONleft,
        | CON SYMBOL DCOLON kind EQ cexp ((SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)))
        | LTYPE SYMBOL EQ cexp           ((SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                           s (LTYPEleft, cexpright)))
-       | DATATYPE SYMBOL dargs EQ barOpt dcons((SgiDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright)))
+       | DATATYPE dtypes                ((SgiDatatype dtypes, s (DATATYPEleft, dtypesright)))
        | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
                 (case dargs of
                      [] => (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))