Constraints in modules

13 files changed, 461 insertions, 304 deletions

diff --git a/src/disjoint.sml b/src/disjoint.sml
index c9f6d2e9..6c66fdd8 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -30,70 +30,86 @@ structure Disjoint :> DISJOINT = struct
 open Elab
 open ElabOps
 
-structure SS = BinarySetFn(struct
-                           type ord_key = string
-                           val compare = String.compare
-                           end)
-
-structure IS = IntBinarySet
-structure IM = IntBinaryMap
-
-type name_ineqs = {
-     namesC : SS.set,
-     namesR : IS.set,
-     namesN : IS.set
-}
-
-val name_default = {
-    namesC = SS.empty,
-    namesR = IS.empty,
-    namesN = IS.empty
-}
-
-type row_ineqs = {
-     namesC : SS.set,
-     namesR : IS.set,
-     namesN : IS.set,
-     rowsR : IS.set,
-     rowsN : IS.set
-}
-
-val row_default = {
-    namesC = SS.empty,
-    namesR = IS.empty,
-    namesN = IS.empty,
-    rowsR = IS.empty,
-    rowsN = IS.empty
-}
-
-fun nameToRow_ineqs {namesC, namesR, namesN} =
-    {namesC = namesC,
-     namesR = namesR,
-     namesN = namesN,
-     rowsR = IS.empty,
-     rowsN = IS.empty}
-
-type env = {
-     namesR : name_ineqs IM.map,
-     namesN : name_ineqs IM.map,
-     rowsR : row_ineqs IM.map,
-     rowsN : row_ineqs IM.map
-}
-
-val empty = {
-    namesR = IM.empty,
-    namesN = IM.empty,
-    rowsR = IM.empty,
-    rowsN = IM.empty
-}
-
 datatype piece =
          NameC of string
        | NameR of int
        | NameN of int
+       | NameM of int * string list * string
        | RowR of int
        | RowN of int
-       | Unknown
+       | RowM of int * string list * string
+
+fun p2s p =
+    case p of
+        NameC s => "NameC(" ^ s ^ ")"
+      | NameR n => "NameR(" ^ Int.toString n ^ ")"
+      | NameN n => "NameN(" ^ Int.toString n ^ ")"
+      | NameM (n, _, s) => "NameR(" ^ Int.toString n ^ ", " ^ s ^ ")"
+      | RowR n => "RowR(" ^ Int.toString n ^ ")"
+      | RowN n => "RowN(" ^ Int.toString n ^ ")"
+      | RowM (n, _, s) => "RowR(" ^ Int.toString n ^ ", " ^ s ^ ")"
+
+fun pp p = print (p2s p ^ "\n")
+
+structure PK = struct
+
+type ord_key = piece
+
+fun join (o1, o2) =
+    case o1 of
+        EQUAL => o2 ()
+      | v => v
+
+fun joinL f (os1, os2) =
+    case (os1, os2) of
+        (nil, nil) => EQUAL
+      | (nil, _) => LESS
+      | (h1 :: t1, h2 :: t2) =>
+        join (f (h1, h2), fn () => joinL f (t1, t2))
+      | (_ :: _, nil) => GREATER
+
+fun compare (p1, p2) =
+    case (p1, p2) of
+        (NameC s1, NameC s2) => String.compare (s1, s2)
+      | (NameR n1, NameR n2) => Int.compare (n1, n2)
+      | (NameN n1, NameN n2) => Int.compare (n1, n2)
+      | (NameM (n1, ss1, s1), NameM (n2, ss2, s2)) =>
+        join (Int.compare (n1, n2),
+           fn () => join (String.compare (s1, s2), fn () =>
+                                                      joinL String.compare (ss1, ss2)))
+      | (RowR n1, RowR n2) => Int.compare (n1, n2)
+      | (RowN n1, RowN n2) => Int.compare (n1, n2)
+      | (RowM (n1, ss1, s1), RowM (n2, ss2, s2)) =>
+        join (Int.compare (n1, n2),
+           fn () => join (String.compare (s1, s2), fn () =>
+                                                      joinL String.compare (ss1, ss2)))
+
+      | (NameC _, _) => LESS
+      | (_, NameC _) => GREATER
+
+      | (NameR _, _) => LESS
+      | (_, NameR _) => GREATER
+
+      | (NameN _, _) => LESS
+      | (_, NameN _) => GREATER
+
+      | (NameM _, _) => LESS
+      | (_, NameM _) => GREATER
+
+      | (RowR _, _) => LESS
+      | (_, RowR _) => GREATER
+
+      | (RowN _, _) => LESS
+      | (_, RowN _) => GREATER
+
+end
+
+structure PS = BinarySetFn(PK)
+structure PM = BinaryMapFn(PK)
+
+type env = PS.set PM.map
+
+val empty = PM.empty
 
 fun nameToRow (c, loc) =
     (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
@@ -103,190 +119,112 @@ fun pieceToRow (p, loc) =
         NameC s => nameToRow (CName s, loc)
       | NameR n => nameToRow (CRel n, loc)
       | NameN n => nameToRow (CNamed n, loc)
+      | NameM (n, xs, x) => nameToRow (CModProj (n, xs, x), loc)
       | RowR n => (CRel n, loc)
-      | RowN n => (CRel n, loc)
-      | Unknown => raise Fail "Unknown to row"
+      | RowN n => (CNamed n, loc)
+      | RowM (n, xs, x) => (CModProj (n, xs, x), loc)
+
+datatype piece' =
+         Piece of piece
+       | Unknown of con
 
 fun decomposeRow env c =
     let
         fun decomposeName (c, acc) =
             case #1 (hnormCon env c) of
-                CName s => NameC s :: acc
-              | CRel n => NameR n :: acc
-              | CNamed n => NameN n :: acc
-              | _ => (print "Unknown name\n"; Unknown :: acc)
-                     
+                CName s => Piece (NameC s) :: acc
+              | CRel n => Piece (NameR n) :: acc
+              | CNamed n => Piece (NameN n) :: acc
+              | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x)) :: acc
+              | _ => Unknown c :: acc
+
         fun decomposeRow (c, acc) =
             case #1 (hnormCon env c) of
                 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
               | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
-              | CRel n => RowR n :: acc
-              | CNamed n => RowN n :: acc
-              | _ => (print "Unknown row\n"; Unknown :: acc)
+              | CRel n => Piece (RowR n) :: acc
+              | CNamed n => Piece (RowN n) :: acc
+              | CModProj (m1, ms, x) => Piece (RowM (m1, ms, x)) :: acc
+              | _ => Unknown c :: acc
     in
         decomposeRow (c, [])
     end
 
-fun assertPiece_name (ps, ineqs : name_ineqs) =
-    {namesC = foldl (fn (p', namesC) =>
-                        case p' of
-                            NameC s => SS.add (namesC, s)
-                          | _ => namesC) (#namesC ineqs) ps,
-     namesR = foldl (fn (p', namesR) =>
-                        case p' of
-                            NameR n => IS.add (namesR, n)
-                          | _ => namesR) (#namesR ineqs) ps,
-     namesN = foldl (fn (p', namesN) =>
-                        case p' of
-                            NameN n => IS.add (namesN, n)
-                          | _ => namesN) (#namesN ineqs) ps}
-
-fun assertPiece_row (ps, ineqs : row_ineqs) =
-    {namesC = foldl (fn (p', namesC) =>
-                        case p' of
-                            NameC s => SS.add (namesC, s)
-                          | _ => namesC) (#namesC ineqs) ps,
-     namesR = foldl (fn (p', namesR) =>
-                        case p' of
-                            NameR n => IS.add (namesR, n)
-                          | _ => namesR) (#namesR ineqs) ps,
-     namesN = foldl (fn (p', namesN) =>
-                        case p' of
-                            NameN n => IS.add (namesN, n)
-                          | _ => namesN) (#namesN ineqs) ps,
-     rowsR = foldl (fn (p', rowsR) =>
-                        case p' of
-                            RowR n => IS.add (rowsR, n)
-                          | _ => rowsR) (#rowsR ineqs) ps,
-     rowsN = foldl (fn (p', rowsN) =>
-                        case p' of
-                            RowN n => IS.add (rowsN, n)
-                          | _ => rowsN) (#rowsN ineqs) ps}
-
-fun assertPiece ps (p, denv) =
-    case p of
-        Unknown => denv
-      | NameC _ => denv
-
-      | NameR n =>
-        let
-            val ineqs = Option.getOpt (IM.find (#namesR denv, n), name_default)
-            val ineqs = assertPiece_name (ps, ineqs)
-        in
-            {namesR = IM.insert (#namesR denv, n, ineqs),
-             namesN = #namesN denv,
-             rowsR = #rowsR denv,
-             rowsN = #rowsN denv}
-        end
-
-      | NameN n =>
-        let
-            val ineqs = Option.getOpt (IM.find (#namesN denv, n), name_default)
-            val ineqs = assertPiece_name (ps, ineqs)
-        in
-            {namesR = #namesR denv,
-             namesN = IM.insert (#namesN denv, n, ineqs),
-             rowsR = #rowsR denv,
-             rowsN = #rowsN denv}
-        end
-
-      | RowR n =>
-        let
-            val ineqs = Option.getOpt (IM.find (#rowsR denv, n), row_default)
-            val ineqs = assertPiece_row (ps, ineqs)
-        in
-            {namesR = #namesR denv,
-             namesN = #namesN denv,
-             rowsR = IM.insert (#rowsR denv, n, ineqs),
-             rowsN = #rowsN denv}
-        end
-
-      | RowN n =>
-        let
-            val ineqs = Option.getOpt (IM.find (#rowsN denv, n), row_default)
-            val ineqs = assertPiece_row (ps, ineqs)
-        in
-            {namesR = #namesR denv,
-             namesN = #namesN denv,
-             rowsR = #rowsR denv,
-             rowsN = IM.insert (#rowsN denv, n, ineqs)}
-        end
-
 fun assert env denv (c1, c2) =
     let
         val ps1 = decomposeRow env c1
         val ps2 = decomposeRow env c2
 
+        val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
+        val ps1 = unUnknown ps1
+        val ps2 = unUnknown ps2
+
+        (*val () = print "APieces1:\n"
+        val () = app pp ps1
+        val () = print "APieces2:\n"
+        val () = app pp ps2*)
+
+        fun assertPiece ps (p, denv) =
+            let
+                val pset = Option.getOpt (PM.find (denv, p), PS.empty)
+                val pset = PS.addList (pset, ps)
+            in
+                PM.insert (denv, p, pset)
+            end
+
         val denv = foldl (assertPiece ps2) denv ps1
     in
         foldl (assertPiece ps1) denv ps2
     end
 
-fun nameEnter {namesC, namesR, namesN} =
-    {namesC = namesC,
-     namesR = IS.map (fn n => n + 1) namesR,
-     namesN = namesN}
-
-fun rowEnter {namesC, namesR, namesN, rowsR, rowsN} =
-    {namesC = namesC,
-     namesR = IS.map (fn n => n + 1) namesR,
-     namesN = namesN,
-     rowsR = IS.map (fn n => n + 1) rowsR,
-     rowsN = rowsN}
-
-fun enter {namesR, namesN, rowsR, rowsN} =
-    {namesR = IM.foldli (fn (n, ineqs, namesR) => IM.insert (namesR, n+1, nameEnter ineqs)) IM.empty namesR,
-     namesN = IM.map nameEnter namesN,
-     rowsR = IM.foldli (fn (n, ineqs, rowsR) => IM.insert (rowsR, n+1, rowEnter ineqs)) IM.empty rowsR,
-     rowsN = IM.map rowEnter rowsN}
-
-fun getIneqs (denv : env) p =
+fun pieceEnter p =
     case p of
-        Unknown => raise Fail "getIneqs: Unknown"
-      | NameC _ => raise Fail "getIneqs: NameC"
-      | NameR n => nameToRow_ineqs (Option.getOpt (IM.find (#namesR denv, n), name_default))
-      | NameN n => nameToRow_ineqs (Option.getOpt (IM.find (#namesN denv, n), name_default))
-      | RowR n => Option.getOpt (IM.find (#rowsR denv, n), row_default)
-      | RowN n => Option.getOpt (IM.find (#rowsN denv, n), row_default)
-
-fun prove1' denv (p1, p2) =
-    let
-        val {namesC, namesR, namesN, rowsR, rowsN} = getIneqs denv p1
-    in
-        case p2 of
-            Unknown => raise Fail "prove1': Unknown"
-          | NameC s => SS.member (namesC, s)
-          | NameR n => IS.member (namesR, n)
-          | NameN n => IS.member (namesN, n)
-          | RowR n => IS.member (rowsR, n)
-          | RowN n => IS.member (rowsN, n)
-    end
+        NameR n => NameR (n + 1)
+      | RowR n => RowR (n + 1)
+      | _ => p
+
+fun enter denv =
+    PM.foldli (fn (p, pset, denv') =>
+                  PM.insert (denv', pieceEnter p, PS.map pieceEnter pset))
+    PM.empty denv
 
 fun prove1 denv (p1, p2) =
     case (p1, p2) of
         (NameC s1, NameC s2) => s1 <> s2
-      | (NameC _, _) => prove1' denv (p2, p1)
-      | (_, RowR _) => prove1' denv (p2, p1)
-      | (_, RowN _) => prove1' denv (p2, p1)
-      | _ => prove1' denv (p1, p2)
+      | _ =>
+        case PM.find (denv, p1) of
+            NONE => false
+          | SOME pset => PS.member (pset, p2)
 
 fun prove env denv (c1, c2, loc) =
     let
         val ps1 = decomposeRow env c1
         val ps2 = decomposeRow env c2
 
-        val hasUnknown = List.exists (fn p => p = Unknown)
+        val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
+        val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
     in
         if hasUnknown ps1 orelse hasUnknown ps2 then
             [(c1, c2)]
         else
-            foldl (fn (p1, rem) =>
-                      foldl (fn (p2, rem) =>
-                                if prove1 denv (p1, p2) then
-                                    rem
-                                else
-                                    (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
-            [] ps1
+            let
+                val ps1 = unUnknown ps1
+                val ps2 = unUnknown ps2
+
+            in
+                (*print "Pieces1:\n";
+                app pp ps1;
+                print "Pieces2:\n";
+                app pp ps2;*)
+
+                foldl (fn (p1, rem) =>
+                          foldl (fn (p2, rem) =>
+                                    if prove1 denv (p1, p2) then
+                                        rem
+                                    else
+                                        (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
+                      [] ps1
+            end
     end
 
 end
diff --git a/src/elab.sml b/src/elab.sml
index cf9a7e7a..9eb8ad2f 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -95,6 +95,7 @@ datatype sgn_item' =
        | SgiVal of string * int * con
        | SgiStr of string * int * sgn
        | SgiSgn of string * int * sgn
+       | SgiConstraint of con * con
 
 and sgn' =
     SgnConst of sgn_item list
@@ -113,6 +114,7 @@ datatype decl' =
        | DSgn of string * int * sgn
        | DStr of string * int * sgn * str
        | DFfiStr of string * int * sgn
+       | DConstraint of con * con
 
      and str' =
          StrConst of decl list
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 54e53607..0e43c9a7 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -81,5 +81,6 @@ signature ELAB_ENV = sig
     val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option
     val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
     val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
+    val projectConstraints : env -> { sgn : Elab.sgn, str : Elab.str } -> (Elab.con * Elab.con) list option
 
 end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 4c27c98d..897f481d 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -291,6 +291,7 @@ fun declBinds env (d, _) =
       | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
       | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
       | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
+      | DConstraint _ => env
 
 fun sgiBinds env (sgi, _) =
     case sgi of
@@ -299,6 +300,7 @@ fun sgiBinds env (sgi, _) =
       | SgiVal (x, n, t) => pushENamedAs env x n t
       | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
       | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
+      | SgiConstraint _ => env
 
 fun sgnSeek f sgis =
     let
@@ -308,13 +310,14 @@ fun sgnSeek f sgis =
               | (sgi, _) :: sgis =>
                 case f sgi of
                     SOME v => SOME (v, (sgns, strs, cons))
-                    | NONE =>
-                      case sgi of
-                          SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
-                        | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
-                        | SgiVal _ => seek (sgis, sgns, strs, cons)
-                        | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
-                        | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
+                  | NONE =>
+                    case sgi of
+                        SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+                      | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+                      | SgiVal _ => seek (sgis, sgns, strs, cons)
+                      | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
+                      | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
+                      | SgiConstraint _ => seek (sgis, sgns, strs, cons)
     in
         seek (sgis, IM.empty, IM.empty, IM.empty)
     end
@@ -461,5 +464,32 @@ fun projectVal env {sgn, str, field} =
       | SgnError => SOME (CError, ErrorMsg.dummySpan)
       | _ => NONE
 
+fun sgnSeekConstraints (str, sgis) =
+    let
+        fun seek (sgis, sgns, strs, cons, acc) =
+            case sgis of
+                [] => acc
+              | (sgi, _) :: sgis =>
+                case sgi of
+                    SgiConstraint (c1, c2) =>
+                    let
+                        val sub = sgnSubCon (str, (sgns, strs, cons))
+                    in
+                        seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
+                    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)
+                  | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
+                  | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
+                  | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
+    in
+        seek (sgis, IM.empty, IM.empty, IM.empty, [])
+    end
+
+fun projectConstraints env {sgn, str} =
+    case #1 (hnormSgn env sgn) of
+        SgnConst sgis => SOME (sgnSeekConstraints (str, sgis))
+      | SgnError => SOME []
+      | _ => NONE
 
 end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index c90a0494..d394c679 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -111,15 +111,16 @@ fun p_con' par env (c, _) =
          handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
       | CModProj (m1, ms, x) =>
         let
-            val (m1x, sgn) = E.lookupStrNamed env m1
-
+            val m1x = #1 (E.lookupStrNamed env m1)
+                handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
+               
             val m1s = if !debug then
                           m1x ^ "__" ^ Int.toString m1
                       else
                           m1x
         in
             p_list_sep (string ".") string (m1x :: ms @ [x])
-        end
+        end 
 
       | CApp (c1, c2) => parenIf par (box [p_con env c1,
                                            space,
@@ -193,19 +194,22 @@ fun p_exp' par env (e, _) =
     case e of
         EPrim p => Prim.p_t p
       | ERel n =>
-        if !debug then
-            string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
-        else
-            string (#1 (E.lookupERel env n))
+        ((if !debug then
+              string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
+          else
+              string (#1 (E.lookupERel env n)))
+         handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
       | ENamed n =>
-        if !debug then
-            string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
-        else
-            string (#1 (E.lookupENamed env n))
+        ((if !debug then
+              string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
+          else
+              string (#1 (E.lookupENamed env n)))
+         handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n))
       | EModProj (m1, ms, x) =>
         let
-            val (m1x, sgn) = E.lookupStrNamed env m1
-
+            val m1x = #1 (E.lookupStrNamed env m1)
+                handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
+                  
             val m1s = if !debug then
                           m1x ^ "__" ^ Int.toString m1
                       else
@@ -325,6 +329,13 @@ fun p_sgn_item env (sgi, _) =
                                    string "=",
                                    space,
                                    p_sgn env sgn]
+      | SgiConstraint (c1, c2) => box [string "constraint",
+                                       space,
+                                       p_con env c1,
+                                       space,
+                                       string "~",
+                                       space,
+                                       p_con env c2]
 
 and p_sgn env (sgn, _) =
     case sgn of
@@ -340,7 +351,8 @@ and p_sgn env (sgn, _) =
                               end,
                               newline,
                               string "end"]
-      | SgnVar n => string (#1 (E.lookupSgnNamed env n))
+      | SgnVar n => ((string (#1 (E.lookupSgnNamed env n)))
+                     handle E.UnboundNamed _ => string ("UNBOUND_SGN_" ^ Int.toString n))
       | SgnFun (x, n, sgn, sgn') => box [string "functor",
                                          space,
                                          string "(",
@@ -367,13 +379,14 @@ and p_sgn env (sgn, _) =
                                      p_con env c]
       | SgnProj (m1, ms, x) =>
         let
-            val (m1x, sgn) = E.lookupStrNamed env m1
-
+            val m1x = #1 (E.lookupStrNamed env m1)
+                handle E.UnboundNamed _ => "UNBOUND_SGN_" ^ Int.toString m1
+                   
             val m1s = if !debug then
                           m1x ^ "__" ^ Int.toString m1
                       else
                           m1x
-        in
+         in
             p_list_sep (string ".") string (m1x :: ms @ [x])
         end
       | SgnError => string "<ERROR>"
@@ -430,6 +443,13 @@ fun p_decl env ((d, _) : decl) =
                                     string ":",
                                     space,
                                     p_sgn env sgn]
+      | DConstraint (c1, c2) => box [string "constraint",
+                                     space,
+                                     p_con env c1,
+                                     space,
+                                     string "~",
+                                     space,
+                                     p_con env c2]
 
 and p_str env (str, _) =
     case str of
@@ -438,7 +458,8 @@ and p_str env (str, _) =
                             p_file env ds,
                             newline,
                             string "end"]
-      | StrVar n => string (#1 (E.lookupStrNamed env n))
+      | StrVar n => ((string (#1 (E.lookupStrNamed env n)))
+                     handle E.UnboundNamed _ => string ("UNBOUND_STR_" ^ Int.toString n))
       | StrProj (str, s) => box [p_str env str,
                                  string ".",
                                  string s]
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 65906c72..9879a9f9 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -379,6 +379,12 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                 S.map2 (sg ctx s,
                      fn s' =>
                         (SgiSgn (x, n, s'), loc))
+              | SgiConstraint (c1, c2) =>
+                S.bind2 (con ctx c1,
+                         fn c1' =>
+                            S.map2 (con ctx c2,
+                                    fn c2' =>
+                                       (SgiConstraint (c1', c2'), loc)))
 
         and sg ctx s acc =
             S.bindP (sg' ctx s acc, sgn ctx)
@@ -396,7 +402,8 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                  | SgiStr (x, _, sgn) =>
                                                    bind (ctx, Str (x, sgn))
                                                  | SgiSgn (x, _, sgn) =>
-                                                   bind (ctx, Sgn (x, sgn)),
+                                                   bind (ctx, Sgn (x, sgn))
+                                                 | SgiConstraint _ => ctx,
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
@@ -502,7 +509,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                  | DStr (x, _, sgn, _) =>
                                                    bind (ctx, Str (x, sgn))
                                                  | DFfiStr (x, _, sgn) =>
-                                                   bind (ctx, Str (x, sgn)),
+                                                   bind (ctx, Str (x, sgn))
+                                                 | DConstraint _ => ctx,
                                                mfd ctx d)) ctx ds,
                      fn ds' => (StrConst ds', loc))
               | StrVar _ => S.return2 strAll
@@ -557,6 +565,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                 S.map2 (mfsg ctx sgn,
                         fn sgn' =>
                            (DFfiStr (x, n, sgn'), loc))
+              | DConstraint (c1, c2) =>
+                S.bind2 (mfc ctx c1,
+                         fn c1' =>
+                            S.map2 (mfc ctx c2,
+                                    fn c2' =>
+                                       (DConstraint (c1', c2'), loc)))
     in
         mfd
     end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index bc43515f..216d483f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -715,7 +715,9 @@ and unifyCons'' (env, denv) (c1All as (c1, _)) (c2All as (c2, _)) =
         fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
     in
         case (c1, c2) of
-            (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
+            (L'.CUnit, L'.CUnit) => []
+
+          | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
             unifyCons' (env, denv) d1 d2
             @ unifyCons' (env, denv) r1 r2
           | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
@@ -1137,6 +1139,7 @@ datatype sgn_error =
        | DuplicateVal of ErrorMsg.span * string
        | DuplicateSgn of ErrorMsg.span * string
        | DuplicateStr of ErrorMsg.span * string
+       | NotConstraintsable of L'.sgn
 
 fun sgnError env err =
     case err of
@@ -1183,6 +1186,9 @@ fun sgnError env err =
         ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
       | DuplicateStr (loc, s) =>
         ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
+      | NotConstraintsable sgn =>
+        (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
+         eprefaces' [("Signature", p_sgn env sgn)])
 
 datatype str_error =
          UnboundStr of ErrorMsg.span * string
@@ -1212,7 +1218,7 @@ fun strError env err =
 
 val hnormSgn = E.hnormSgn
 
-fun elabSgn_item denv ((sgi, loc), (env, gs)) =
+fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
     case sgi of
         L.SgiConAbs (x, k) =>
         let
@@ -1220,7 +1226,7 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
 
             val (env', n) = E.pushCNamed env x k' NONE
         in
-            ([(L'.SgiConAbs (x, n, k'), loc)], (env', gs))
+            ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs))
         end
 
       | L.SgiCon (x, ko, c) =>
@@ -1234,7 +1240,7 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
         in
             checkKind env c' ck k';
 
-            ([(L'.SgiCon (x, n, k', c'), loc)], (env', gs' @ gs))
+            ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
         end
 
       | L.SgiVal (x, c) =>
@@ -1246,7 +1252,7 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
             (unifyKinds ck ktype
              handle KUnify ue => strError env (NotType (ck, ue)));
 
-            ([(L'.SgiVal (x, n, c'), loc)], (env', gs' @ gs))
+            ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
         end
 
       | L.SgiStr (x, sgn) =>
@@ -1254,7 +1260,7 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
             val (sgn', gs') = elabSgn (env, denv) sgn
             val (env', n) = E.pushStrNamed env x sgn'
         in
-            ([(L'.SgiStr (x, n, sgn'), loc)], (env', gs' @ gs))
+            ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
         end
 
       | L.SgiSgn (x, sgn) =>
@@ -1262,7 +1268,7 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
             val (sgn', gs') = elabSgn (env, denv) sgn
             val (env', n) = E.pushSgnNamed env x sgn'
         in
-            ([(L'.SgiSgn (x, n, sgn'), loc)], (env', gs' @ gs))
+            ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
         end
 
       | L.SgiInclude sgn =>
@@ -1271,16 +1277,29 @@ fun elabSgn_item denv ((sgi, loc), (env, gs)) =
         in
             case #1 (hnormSgn env sgn') of
                 L'.SgnConst sgis =>
-                (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, gs' @ gs))
+                (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs))
               | _ => (sgnError env (NotIncludable sgn');
-                      ([], (env, [])))
+                      ([], (env, denv, [])))
+        end
+
+      | L.SgiConstraint (c1, c2) =>
+        let
+            val (c1', k1, gs1) = elabCon (env, denv) c1
+            val (c2', k2, gs2) = elabCon (env, denv) c2
+
+            val denv = 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'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2))
         end
 
 and elabSgn (env, denv) (sgn, loc) =
     case sgn of
         L.SgnConst sgis =>
         let
-            val (sgis', (_, gs)) = ListUtil.foldlMapConcat (elabSgn_item denv) (env, []) sgis
+            val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis
 
             val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) =>
                               case sgi of
@@ -1313,7 +1332,8 @@ and elabSgn (env, denv) (sgn, loc) =
                                        sgnError env (DuplicateStr (loc, x))
                                    else
                                        ();
-                                   (cons, vals, sgns, SS.add (strs, x))))
+                                   (cons, vals, sgns, SS.add (strs, x)))
+                                | L'.SgiConstraint _ => (cons, vals, sgns, strs))
                     (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
         in
             ((L'.SgnConst sgis', loc), gs)
@@ -1410,35 +1430,65 @@ fun selfifyAt env {str, sgn} =
           | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
     end
 
-fun dopen env {str, strs, sgn} =
+fun dopen (env, denv) {str, strs, sgn} =
     let
         val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
                 (L'.StrVar str, #2 sgn) strs
     in
         case #1 (hnormSgn env sgn) of
             L'.SgnConst sgis =>
-            ListUtil.foldlMap (fn ((sgi, loc), env') =>
+            ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) =>
                                   case sgi of
                                       L'.SgiConAbs (x, n, k) =>
-                                      ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
-                                       E.pushCNamedAs env' x n k NONE)
+                                      let
+                                          val c = (L'.CModProj (str, strs, x), loc)
+                                      in
+                                          ((L'.DCon (x, n, k, c), loc),
+                                           (E.pushCNamedAs env' x n k (SOME c), denv'))
+                                      end
                                     | L'.SgiCon (x, n, k, c) =>
                                       ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
-                                       E.pushCNamedAs env' x n k (SOME c))
+                                       (E.pushCNamedAs env' x n k (SOME c), denv'))
                                     | L'.SgiVal (x, n, t) =>
                                       ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc),
-                                       E.pushENamedAs env' x n t)
+                                       (E.pushENamedAs env' x n t, denv'))
                                     | L'.SgiStr (x, n, sgn) =>
                                       ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc),
-                                       E.pushStrNamedAs env' x n sgn)
+                                       (E.pushStrNamedAs env' x n sgn, denv'))
                                     | L'.SgiSgn (x, n, sgn) =>
                                       ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc),
-                                       E.pushSgnNamedAs env' x n sgn))
-                              env sgis
+                                       (E.pushSgnNamedAs env' x n sgn, denv'))
+                                    | L'.SgiConstraint (c1, c2) =>
+                                      ((L'.DConstraint (c1, c2), loc),
+                                       (env', denv (* D.assert env denv (c1, c2) *) )))
+                              (env, denv) sgis
           | _ => (strError env (UnOpenable sgn);
-                  ([], env))
+                  ([], (env, denv)))
     end
 
+fun dopenConstraints (loc, env, denv) {str, strs} =
+    case E.lookupStr env str of
+        NONE => (strError env (UnboundStr (loc, str));
+                 denv)
+      | SOME (n, sgn) =>
+        let
+            val (st, 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) strs
+                            
+            val cso = E.projectConstraints env {sgn = sgn, str = st}
+
+            val denv = case cso of
+                           NONE => (strError env (UnboundStr (loc, str));
+                                    denv)
+                         | SOME cs => foldl (fn ((c1, c2), denv) => D.assert env denv (c1, c2)) denv cs
+        in
+            denv
+        end
+
 fun sgiOfDecl (d, loc) =
     case d of
         L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc)
@@ -1446,6 +1496,12 @@ fun sgiOfDecl (d, loc) =
       | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc)
       | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc)
       | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc)
+      | L'.DConstraint cs => (L'.SgiConstraint cs, loc)
+
+fun sgiBindsD (env, denv) (sgi, _) =
+    case sgi of
+        L'.SgiConstraint (c1, c2) => D.assert env denv (c1, c2)
+      | _ => denv
 
 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
     case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
@@ -1454,20 +1510,20 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
 
       | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
         let
-            fun folder (sgi2All as (sgi, _), env) =
+            fun folder (sgi2All as (sgi, _), (env, denv)) =
                 let
                     fun seek p =
                         let
-                            fun seek env ls =
+                            fun seek (env, denv) ls =
                                 case ls of
                                     [] => (sgnError env (UnmatchedSgi sgi2All);
-                                           env)
+                                           (env, denv))
                                   | h :: t =>
                                     case p h of
-                                        NONE => seek (E.sgiBinds env h) t
-                                      | SOME env => env
+                                        NONE => seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t
+                                      | SOME envs => envs
                         in
-                            seek env sgis1
+                            seek (env, denv) sgis1
                         end
                 in
                     case sgi of
@@ -1485,7 +1541,8 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                                  SOME (if n1 = n2 then
                                                            env
                                                        else
-                                                           E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)))
+                                                           E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)),
+                                                       denv)
                                              end
                                          else
                                              NONE
@@ -1502,7 +1559,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                      L'.SgiCon (x', n1, k1, c1) =>
                                      if x = x' then
                                          let
-                                             fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2))
+                                             fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv)
                                          in
                                              (case unifyCons (env, denv) c1 c2 of
                                                   [] => good ()
@@ -1521,11 +1578,11 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                      L'.SgiVal (x', n1, c1) =>
                                      if x = x' then
                                          (case unifyCons (env, denv) c1 c2 of
-                                              [] => SOME env
+                                              [] => SOME (env, denv)
                                             | _ => NONE)
                                          handle CUnify (c1, c2, err) =>
                                                 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
-                                                 SOME env)
+                                                 SOME (env, denv))
                                      else
                                          NONE
                                    | _ => NONE)
@@ -1545,7 +1602,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                                                             (selfifyAt env {str = (L'.StrVar n1, #2 sgn2),
                                                                                             sgn = sgn2})
                                          in
-                                             SOME env
+                                             SOME (env, denv)
                                          end
                                      else
                                          NONE
@@ -1566,14 +1623,24 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                                        else
                                                            E.pushSgnNamedAs env x n1 sgn2
                                          in
-                                             SOME env
+                                             SOME (env, denv)
                                          end
                                      else
                                          NONE
                                    | _ => NONE)
+
+                      | L'.SgiConstraint (c2, d2) =>
+                        seek (fn sgi1All as (sgi1, _) =>
+                                 case sgi1 of
+                                     L'.SgiConstraint (c1, d1) =>
+                                     if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then
+                                         SOME (env, D.assert env denv (c2, d2))
+                                     else
+                                         NONE
+                                   | _ => NONE)
                 end
         in
-            ignore (foldl folder env sgis2)
+            ignore (foldl folder (env, denv) sgis2)
         end
 
       | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
@@ -1591,7 +1658,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
       | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
 
 
-fun elabDecl denv ((d, loc), (env, gs)) =
+fun elabDecl ((d, loc), (env, denv, gs)) =
     case d of
         L.DCon (x, ko, c) =>
         let
@@ -1604,7 +1671,7 @@ fun elabDecl denv ((d, loc), (env, gs)) =
         in
             checkKind env c' ck k';
 
-            ([(L'.DCon (x, n, k', c'), loc)], (env', gs' @ gs))
+            ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
         end
       | L.DVal (x, co, e) =>
         let
@@ -1617,7 +1684,7 @@ fun elabDecl denv ((d, loc), (env, gs)) =
 
             val gs3 = checkCon (env, denv) e' et c'
         in
-            ([(L'.DVal (x, n, c', e'), loc)], (env', gs1 @ gs2 @ gs3 @ gs))
+            ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs))
         end
 
       | L.DSgn (x, sgn) =>
@@ -1625,7 +1692,7 @@ fun elabDecl denv ((d, loc), (env, gs)) =
             val (sgn', gs') = elabSgn (env, denv) sgn
             val (env', n) = E.pushSgnNamed env x sgn'
         in
-            ([(L'.DSgn (x, n, sgn'), loc)], (env', gs' @ gs))
+            ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
         end
 
       | L.DStr (x, sgno, str) =>
@@ -1691,7 +1758,7 @@ fun elabDecl denv ((d, loc), (env, gs)) =
                    | _ => strError env (FunctorRebind loc))
               | _ => ();
 
-            ([(L'.DStr (x, n, sgn', str'), loc)], (env', gs' @ gs))
+            ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
         end
 
       | L.DFfiStr (x, sgn) =>
@@ -1700,32 +1767,54 @@ fun elabDecl denv ((d, loc), (env, gs)) =
 
             val (env', n) = E.pushStrNamed env x sgn'
         in
-            ([(L'.DFfiStr (x, n, sgn'), loc)], (env', gs' @ gs))
+            ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
         end
 
       | L.DOpen (m, ms) =>
-        case E.lookupStr env m of
-            NONE => (strError env (UnboundStr (loc, m));
-                     ([], (env, [])))
-          | 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') = dopen env {str = n, strs = ms, sgn = sgn}
-            in
-                (ds, (env', []))
-            end
+        (case E.lookupStr env m of
+             NONE => (strError env (UnboundStr (loc, m));
+                      ([], (env, denv, [])))
+           | 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', []))
+             end)
+
+      | L.DConstraint (c1, c2) =>
+        let
+            val (c1', k1, gs1) = elabCon (env, denv) c1
+            val (c2', k2, gs2) = elabCon (env, denv) c2
+            val gs3 = map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1', c2', loc))
+
+            val denv' = 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', gs1 @ gs2 @ gs3))
+        end
+
+      | L.DOpenConstraints (m, ms) =>
+        let
+            val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
+        in
+            ([], (env, denv, []))
+        end
 
 and elabStr (env, denv) (str, loc) =
     case str of
         L.StrConst ds =>
         let
-            val (ds', (env', gs)) = ListUtil.foldlMapConcat (elabDecl denv) (env, []) ds
+            val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
             val sgis = map sgiOfDecl ds'
 
             val (sgis, _, _, _, _) =
@@ -1781,7 +1870,8 @@ and elabStr (env, denv) (str, loc) =
                                           (SS.add (strs, x), x)
                               in
                                   ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
-                              end)
+                              end
+                            | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs))
 
                 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
         in
@@ -1852,7 +1942,7 @@ fun elabFile basis env file =
 
         val (env', basis_n) = E.pushStrNamed env "Basis" sgn
 
-        val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn}
+        val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn}
 
         fun discoverC r x =
             case E.lookupC env' x of
@@ -1868,7 +1958,7 @@ fun elabFile basis env file =
             let
                 val () = resetKunif ()
                 val () = resetCunif ()
-                val (ds, (env, gs)) = elabDecl D.empty (d, (env, gs))
+                val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs))
             in
                 if ErrorMsg.anyErrors () then
                     ()
diff --git a/src/explify.sml b/src/explify.sml
index e0226213..c5e7fbd4 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -91,15 +91,16 @@ fun explifyExp (e, loc) =
 
 fun explifySgi (sgi, loc) =
     case sgi of
-        L.SgiConAbs (x, n, k) => (L'.SgiConAbs (x, n, explifyKind k), loc)
-      | L.SgiCon (x, n, k, c) => (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
-      | L.SgiVal (x, n, c) => (L'.SgiVal (x, n, explifyCon c), loc)
-      | L.SgiStr (x, n, sgn) => (L'.SgiStr (x, n, explifySgn sgn), loc)
-      | L.SgiSgn (x, n, sgn) => (L'.SgiSgn (x, n, explifySgn sgn), loc)
+        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.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc)
+      | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
+      | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
+      | L.SgiConstraint _ => NONE
 
 and explifySgn (sgn, loc) =
     case sgn of
-        L.SgnConst sgis => (L'.SgnConst (map explifySgi sgis), loc)
+        L.SgnConst sgis => (L'.SgnConst (List.mapPartial explifySgi sgis), loc)
       | L.SgnVar n => (L'.SgnVar n, loc)
       | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc)
       | L.SgnWhere (sgn, x, c) => (L'.SgnWhere (explifySgn sgn, x, explifyCon c), loc)
@@ -108,22 +109,23 @@ and explifySgn (sgn, loc) =
 
 fun explifyDecl (d, loc : EM.span) =
     case d of
-        L.DCon (x, n, k, c) => (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
-      | L.DVal (x, n, t, e) => (L'.DVal (x, n, explifyCon t, explifyExp e), loc)
+        L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
+      | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc)
 
-      | L.DSgn (x, n, sgn) => (L'.DSgn (x, n, explifySgn sgn), loc)
-      | L.DStr (x, n, sgn, str) => (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc)
-      | L.DFfiStr (x, n, sgn) => (L'.DFfiStr (x, n, explifySgn sgn), loc)
+      | L.DSgn (x, n, sgn) => SOME (L'.DSgn (x, n, explifySgn sgn), loc)
+      | L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc)
+      | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc)
+      | L.DConstraint (c1, c2) => NONE
 
 and explifyStr (str, loc) =
     case str of
-        L.StrConst ds => (L'.StrConst (map explifyDecl ds), loc)
+        L.StrConst ds => (L'.StrConst (List.mapPartial explifyDecl ds), loc)
       | L.StrVar n => (L'.StrVar n, loc)
       | L.StrProj (str, s) => (L'.StrProj (explifyStr str, s), loc)
       | L.StrFun (m, n, dom, ran, str) => (L'.StrFun (m, n, explifySgn dom, explifySgn ran, explifyStr str), loc)
       | L.StrApp (str1, str2) => (L'.StrApp (explifyStr str1, explifyStr str2), loc)
       | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc)
 
-val explify = map explifyDecl
+val explify = List.mapPartial explifyDecl
 
 end
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 4bf03388..84877eee 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -44,7 +44,8 @@ val s = ErrorMsg.spanOf
  | TYPE | NAME
  | ARROW | LARROW | DARROW
  | FN | PLUSPLUS | DOLLAR | TWIDDLE
- | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | INCLUDE | OPEN
+ | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN
+ | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS
 
 %nonterm
    file of decl list
@@ -128,6 +129,10 @@ decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft,
        | OPEN mpath                     (case mpath of
                                              [] => raise Fail "Impossible mpath parse [1]"
                                            | m :: ms => (DOpen (m, ms), s (OPENleft, mpathright)))
+       | OPEN CONSTRAINTS mpath         (case mpath of
+                                             [] => raise Fail "Impossible mpath parse [3]"
+                                           | m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright)))
+       | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
 
 sgn    : sgntm                          (sgntm)
        | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
@@ -161,6 +166,7 @@ sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, k
                                                  (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))),
                                          s (FUNCTORleft, sgn2right))
        | INCLUDE sgn                    (SgiInclude sgn, s (INCLUDEleft, sgnright))
+       | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
 
 sgis   :                                ([])
        | sgi sgis                       (sgi :: sgis)
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 3fa0b45c..8b4a1789 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -160,6 +160,8 @@ realconst = [0-9]+\.[0-9]*;
 <INITIAL> "extern"    => (Tokens.EXTERN (pos yypos, pos yypos + size yytext));
 <INITIAL> "include"   => (Tokens.INCLUDE (pos yypos, pos yypos + size yytext));
 <INITIAL> "open"      => (Tokens.OPEN (pos yypos, pos yypos + size yytext));
+<INITIAL> "constraint"=> (Tokens.CONSTRAINT (pos yypos, pos yypos + size yytext));
+<INITIAL> "constraints"=> (Tokens.CONSTRAINTS (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "Type"      => (Tokens.TYPE (pos yypos, pos yypos + size yytext));
 <INITIAL> "Name"      => (Tokens.NAME (pos yypos, pos yypos + size yytext));
diff --git a/src/source.sml b/src/source.sml
index 0b168dd0..4aea002e 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -75,6 +75,7 @@ datatype sgn_item' =
        | SgiStr of string * sgn
        | SgiSgn of string * sgn
        | SgiInclude of sgn
+       | SgiConstraint of con * con
 
 and sgn' =
     SgnConst of sgn_item list
@@ -110,6 +111,8 @@ datatype decl' =
        | DStr of string * sgn option * str
        | DFfiStr of string * sgn
        | DOpen of string * string list
+       | DConstraint of con * con
+       | DOpenConstraints of string * string list
 
      and str' =
          StrConst of decl list
diff --git a/src/source_print.sml b/src/source_print.sml
index 41051c81..8fc27106 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -287,6 +287,13 @@ fun p_sgn_item (sgi, _) =
       | SgiInclude sgn => box [string "include",
                                space,
                                p_sgn sgn]
+      | SgiConstraint (c1, c2) => box [string "constraint",
+                                       space,
+                                       p_con c1,
+                                       space,
+                                       string "~",
+                                       space,
+                                       p_con c2]
 
 and p_sgn (sgn, _) =
     case sgn of
@@ -398,6 +405,18 @@ fun p_decl ((d, _) : decl) =
       | DOpen (m, ms) => box [string "open",
                               space,
                               p_list_sep (string ".") string (m :: ms)]
+      | DConstraint (c1, c2) => box [string "constraint",
+                                     space,
+                                     p_con c1,
+                                     space,
+                                     string "~",
+                                     space,
+                                     p_con c2]
+      | DOpenConstraints (m, ms) => box [string "open",
+                                         space,
+                                         string "constraints",
+                                         space,
+                                         p_list_sep (string ".") string (m :: ms)]
 
 and p_str (str, _) =
     case str of
diff --git a/tests/constraint.lac b/tests/constraint.lac
new file mode 100644
index 00000000..54c77093
--- /dev/null
+++ b/tests/constraint.lac
@@ -0,0 +1,29 @@
+signature S = sig
+        con nm :: Name
+        con r :: {Type}
+
+        constraint [nm] ~ r
+end
+
+structure M : S = struct
+        con nm = #A
+        con r = [B = float, C = string]
+
+        constraint [A] ~ [B]
+        constraint [nm] ~ r
+        constraint [C] ~ [D]
+end
+
+structure M' = struct
+        open M
+
+        con combo = [nm = int] ++ r
+end
+
+structure M' = struct
+        open constraints M
+
+        con nm' = M.nm
+        con r' = M.r
+        con combo = [nm' = int] ++ r'
+end