diff --git a/samples/ListClient.as b/samples/ListClient.as
new file mode 100644
index 00000000000..4c46fa7fa24
--- /dev/null
+++ b/samples/ListClient.as
@@ -0,0 +1,7 @@
+let List = import "ListLib.as"; // todo: make local so not re-exported in type!
+
+type Stack = List.List<Int>;
+
+func push(x : Int, s : Stack) : Stack = List.cons<Int>(x, s);
+
+let empty = List.nil<Int>();
diff --git a/samples/ListClient.txt b/samples/ListClient.txt
new file mode 100644
index 00000000000..64e12b76cd3
--- /dev/null
+++ b/samples/ListClient.txt
@@ -0,0 +1,12 @@
+-- Parsing ListClient.as:
+-- Parsing ListLib.as:
+-- Checking ListLib.as:
+-- Checking ListClient.as:
+type Stack = List<Int>
+let List : module {type List<T> = ?(T, List<T>); cons : <T>(T, List<T>) -> List<T>; nil : <T>() -> List<T>}
+let empty : ?(Int, List<Int>)
+let push : (Int, Stack) -> Stack
+-- Interpreting ListLib.as:
+-- Interpreting ListClient.as:
+nil()
+  <= null
diff --git a/samples/ListLib.as b/samples/ListLib.as
new file mode 100644
index 00000000000..318325de37a
--- /dev/null
+++ b/samples/ListLib.as
@@ -0,0 +1,3 @@
+type List<T> = ?(T, List<T>);
+func nil<T>() : List<T> = null;
+func cons<T>(x : T, l : List<T>) : List<T> = ?(x, l);
diff --git a/samples/ListLib.txt b/samples/ListLib.txt
new file mode 100644
index 00000000000..0be86d08973
--- /dev/null
+++ b/samples/ListLib.txt
@@ -0,0 +1,6 @@
+-- Parsing ListLib.as:
+-- Checking ListLib.as:
+type List<T> = ?(T, List<T>)
+let cons : <T>(T, List<T>) -> List<T>
+let nil : <T>() -> List<T>
+-- Interpreting ListLib.as:
diff --git a/samples/modules.as b/samples/modules.as
new file mode 100644
index 00000000000..7ca07c55531
--- /dev/null
+++ b/samples/modules.as
@@ -0,0 +1,15 @@
+module Collections = {
+  module List = {
+    type List<T> = ?(T, List<T>);
+    func nil<T>() : List<T> = null;
+    func cons<T>(x : T, l : List<T>) : List<T> = ?(x, l);
+  };
+};
+
+let List = Collections.List;
+
+type Stack = List.List<Int>;
+
+let empty : Stack = List.nil<Int>();
+func push(x : Int, s : Stack) : Stack = List.cons<Int>(x, s);
+
diff --git a/samples/modules.txt b/samples/modules.txt
new file mode 100644
index 00000000000..105e0bee9ff
--- /dev/null
+++ b/samples/modules.txt
@@ -0,0 +1,11 @@
+-- Parsing modules.as:
+-- Checking modules.as:
+type List<T> = ?(T, List<T>)
+type Stack = List<Int>
+let Collections : module {List : module {type List<T> = ?(T, List<T>); cons : <T>(T, List<T>) -> List<T>; nil : <T>() -> List<T>}}
+let List : module {type List<T> = ?(T, List<T>); cons : <T>(T, List<T>) -> List<T>; nil : <T>() -> List<T>}
+let empty : ?(Int, List<Int>)
+let push : (Int, Stack) -> Stack
+-- Interpreting modules.as:
+nil()
+  <= null
diff --git a/src/arrange.ml b/src/arrange.ml
index 6fdba84ef4e..8006bf40d68 100644
--- a/src/arrange.ml
+++ b/src/arrange.ml
@@ -128,6 +128,7 @@ and control c = match c with
 and obj_sort' s = match s with
   | Type.Object sh -> Atom ("Object " ^ sharing sh)
   | Type.Actor -> Atom "Actor"
+  | Type.Module -> Atom "Module"
 
 and obj_sort s = obj_sort' s.it
 
@@ -153,6 +154,10 @@ and exp_field (ef : exp_field)
 
 and operator_type t = Atom (Type.string_of_typ t)
 
+and path p = match p.it with
+  | IdH i -> "IdH" $$ [id i]
+  | DotH (p,i) -> "DotH" $$ [path p; id i]
+
 and typ t = match t.it with
   | VarT (s, ts)        -> "VarT" $$ [id s] @ List.map typ ts
   | PrimT p             -> "PrimT" $$ [Atom p]
@@ -164,6 +169,7 @@ and typ t = match t.it with
   | FuncT (s, tbs, at, rt) -> "FuncT" $$ [Atom (sharing s.it)] @ List.map typ_bind tbs @ [ typ at; typ rt]
   | AsyncT t            -> "AsyncT" $$ [typ t]
   | ParT t              -> "ParT" $$ [typ t]
+  | PathT (p, i, ts)         -> "PathT" $$ [path p; id i] @ List.map typ ts
 
 and dec d = match d.it with
   | ExpD e -> "ExpD" $$ [exp e ]
@@ -173,5 +179,7 @@ and dec d = match d.it with
     "TypD" $$ [id x] @ List.map typ_bind tp @ [typ t]
   | ClassD (x, tp, s, p, i', efs) ->
     "ClassD" $$ id x :: List.map typ_bind tp @ [obj_sort s; pat p; id i'] @ List.map exp_field efs
+  | ModuleD (i,ds) ->
+    "ModuleD" $$  [id i] @ List.map dec ds
 
 and prog prog = "BlockE"  $$ List.map dec prog.it
diff --git a/src/arrange_type.ml b/src/arrange_type.ml
index 7544986fb69..f9a32aa5d60 100644
--- a/src/arrange_type.ml
+++ b/src/arrange_type.ml
@@ -17,6 +17,7 @@ let control c = match c with
 let obj_sort s = match s with
   | Type.Object sh -> Atom ("Object " ^ sharing sh)
   | Type.Actor -> Atom "Actor"
+  | Type.Module -> Atom "Module"
 
 let prim p = match p with
   | Null -> Atom "Null"
@@ -50,6 +51,7 @@ let rec typ (t:Type.typ) = match t with
   | Any                   -> Atom "Any"
   | Non                   -> Atom "Non"
   | Pre                   -> Atom "Pre"
+  | Kind (c,k)            -> Atom "Kind ..." (* TBC *)
 
 and typ_bind (tb : Type.bind) =
   tb.var $$ [typ tb.bound]
diff --git a/src/async.ml b/src/async.ml
index 63c4d431381..caa7398f12b 100644
--- a/src/async.ml
+++ b/src/async.ml
@@ -167,6 +167,7 @@ module Transform() = struct
     | Any -> Any
     | Non -> Non
     | Pre -> Pre
+    | Kind (c,k) -> Kind (t_con c, t_kind k)
 
   and t_bind {var; bound} =
     {var; bound = t_typ bound}
diff --git a/src/check_ir.ml b/src/check_ir.ml
index b19b1ca8566..9917b62031a 100644
--- a/src/check_ir.ml
+++ b/src/check_ir.ml
@@ -87,12 +87,11 @@ let add_typs c cs =
 let adjoin c scope =
   { c with
     vals = T.Env.adjoin c.vals scope.val_env;
-    cons = T.ConSet.disjoint_union c.cons scope.con_env;
+    cons = T.ConSet.(*disjoint_*)union c.cons scope.con_env;
   }
 
 let adjoin_vals c ve = {c with vals = T.Env.adjoin c.vals ve}
 
-
 let adjoin_cons c ce =
   { c with
     cons = T.ConSet.disjoint_union c.cons ce;
@@ -178,14 +177,17 @@ let rec check_typ env typ : unit =
     let t' = T.promote typ in
     check_shared env no_region t'
   | T.Obj (sort, fields) ->
-    let rec sorted = function
-      | [] | [_] -> true
+    let rec strictly_sorted fields =
+      match fields with
+      | []
+      | [_] -> true
       | f1::((f2::_) as fields') ->
-        T.compare_field f1 f2  < 0 && sorted fields'
+        T.compare_field f1 f2  < 0 && strictly_sorted fields'
     in
-    check_ids env (List.map (fun (field : T.field) -> field.T.lab) fields);
     List.iter (check_typ_field env sort) fields;
-    check env no_region (sorted fields) "object type's fields are not sorted"
+    (* fields strictly sorted (and) distinct *)
+    if (not (strictly_sorted fields)) then
+      error env no_region "object type's fields are not distinct and sorted %s" (T.string_of_typ typ)
   | T.Variant cts ->
     let rec sorted = function
       | [] | [_] -> true
@@ -202,6 +204,19 @@ let rec check_typ env typ : unit =
       "Serialized in non-serialized flavor";
     check_typ env typ;
     check_sub env no_region typ T.Shared
+  | T.Kind (c,k) ->
+    check_kind env k
+
+and check_kind env k =
+  let (binds,typ) =
+    match k with
+    | T.Abs(binds,typ)
+      | T.Def(binds,typ) -> (binds,typ)
+  in
+  let cs,ce = check_typ_binds env binds in
+  let ts = List.map (fun c -> T.Con(c,[])) cs in
+  let env' = adjoin_cons env ce in
+  check_typ env' (T.open_ ts  typ);
 
 and check_typ_field env s typ_field : unit =
   let T.{lab; typ} = typ_field in
@@ -210,7 +225,7 @@ and check_typ_field env s typ_field : unit =
      (s <> T.Actor || T.is_func (T.promote typ))
     "actor field has non-function type";
   check env no_region
-     (s = T.Object T.Local || T.sub typ T.Shared)
+     (s = T.Object T.Local || s = T.Module || T.sub typ T.Shared)
     "shared object or actor field has non-shared type"
 
 and check_typ_summand env (c, typ) : unit =
@@ -358,10 +373,10 @@ let rec check_exp env (exp:Ir.exp) : unit =
              | ActorDotE _ -> sort = T.Actor
              | DotE _ -> sort <> T.Actor
              | _ -> false) "sort mismatch";
-      match List.find_opt (fun T.{lab; _} -> lab = n) tfs with
-      | Some {T.typ = tn;_} ->
+      match T.lookup_field n tfs with (*CRUSSO: FIX ME*)
+      | tn ->
         tn <~ t
-      | None ->
+      | exception _ ->
         error env exp1.at "field name %s does not exist in type\n  %s"
           n (T.string_of_typ_expand t1)
     end
@@ -539,11 +554,18 @@ let rec check_exp env (exp:Ir.exp) : unit =
     t1 <: t0;
     t0 <: t;
   | NewObjE (s, fs, t0) ->
-    let t1 = type_obj env s fs in
     check (T.is_obj t0) "bad annotation (object type expected)";
+    let is_typ_field {T.lab;T.typ} =
+      match typ with T.Kind _ -> true | _ -> false
+    in
+    let (_s,tfs0) = T.as_obj t0 in
+    let typ_tfs0, val_tfs0 = List.partition is_typ_field tfs0
+    in
+    let t1 = type_obj env s fs in
+    let (_s, tfs1) = T.as_obj t1 in
+    let t1 = T.Obj(s, List.sort T.compare_field (typ_tfs0 @ tfs1)) in
     t1 <: t0;
     t0 <: t
-
 (* Cases *)
 
 and check_cases env t_pat t cases =
@@ -670,7 +692,7 @@ and type_exp_field env s f : T.field =
   check_sub env f.at t f.note;
   check env f.at ((s = T.Actor) ==> T.is_func t)
     "public actor field is not a function";
-  check env f.at ((s <> T.Object T.Local) ==> T.sub t T.Shared)
+  check env f.at ((s <> T.Object T.Local && s <> T.Module) ==> T.sub t T.Shared)
     "public shared object or actor field has non-shared type";
   T.{lab = name; typ = t}
 
@@ -722,9 +744,10 @@ and gather_block_decs env decs =
 
 and gather_dec env scope dec : scope =
   match dec.it with
-  | LetD (pat, _) ->
+  | LetD (pat, exp) ->
     let ve = gather_pat env scope.val_env pat in
-    { scope with val_env = ve}
+    let ce' = gather_typ env scope.con_env exp.note.note_typ in
+    { val_env = ve; con_env = ce'}
   | VarD (id, exp) ->
     check env dec.at
       (not (T.Env.mem id.it scope.val_env))
@@ -738,6 +761,16 @@ and gather_dec env scope dec : scope =
     let ce' = T.ConSet.disjoint_add c scope.con_env in
     { scope with con_env = ce' }
 
+and gather_typ env ce typ =
+   match typ with
+   | T.Obj(T.Module,fs) ->
+     List.fold_right (fun {T.lab;T.typ = typ1} ce ->
+         match typ1 with
+         | T.Kind (c, k) -> T.ConSet.add c ce
+         | _ -> gather_typ env ce typ1
+       ) fs ce
+   | _ -> ce
+
 (* Programs *)
 
 let check_prog scope phase (((ds, exp), flavor) as prog) : unit =
diff --git a/src/compile.ml b/src/compile.ml
index 3468488cc95..c93cf86b88f 100644
--- a/src/compile.ml
+++ b/src/compile.ml
@@ -2826,6 +2826,7 @@ module Serialization = struct
         | Obj (_, fs) -> List.for_all (fun f -> go f.typ) fs
         | Mut t -> go t
         | Serialized t -> go t
+        | Kind (_c,_k) -> false
       end
     in go t
 
@@ -4531,8 +4532,8 @@ and compile_exp (env : E.t) exp =
     let prelude_names = find_prelude_names env in
     if Freevars.M.is_empty (Freevars.diff captured prelude_names)
     then actor_lit env i ds fs exp.at
-    else todo_trap env "non-closed actor" (Arrange_ir.exp exp) 
-  | NewObjE (Type.Object _ (*sharing*), fs, _) ->
+    else todo_trap env "non-closed actor" (Arrange_ir.exp exp)
+  | NewObjE ((Type.Object _ (*sharing*) | Type.Module), fs, _) ->
     SR.Vanilla,
     let fs' = fs |> List.map
       (fun (f : Ir.field) -> (f.it.name, fun env ->
diff --git a/src/con.ml b/src/con.ml
index 376cb46a92a..d8d442cc75e 100644
--- a/src/con.ml
+++ b/src/con.ml
@@ -34,3 +34,4 @@ let to_string c =
 
 let eq c1 c2 = (c1.name, c1.stamp) = (c2.name, c2.stamp)
 let compare c1 c2 = compare (c1.name, c1.stamp) (c2.name, c2.stamp)
+
diff --git a/src/definedness.ml b/src/definedness.ml
index 179dc457837..ae4616de360 100644
--- a/src/definedness.ml
+++ b/src/definedness.ml
@@ -155,6 +155,9 @@ and dec msgs d = match d.it with
   | TypD (i, tp, t) -> (M.empty, S.empty)
   | ClassD (i, tp, s, p, i', efs) ->
     (M.empty, S.singleton i.it) +++ delayify (exp_fields msgs efs /// pat msgs p // i'.it)
+  | ModuleD (i, ds) ->
+    (M.empty, S.singleton i.it) +++ decs msgs ds    (* TBR *)
+
 
 and decs msgs decs : f =
   (* Annotate the declarations with the analysis results *)
diff --git a/src/desugar.ml b/src/desugar.ml
index bb198112213..cc65f9958ff 100644
--- a/src/desugar.ml
+++ b/src/desugar.ml
@@ -100,19 +100,21 @@ and exp' at note = function
 
 and obj at s self_id es obj_typ =
   match s.it with
-  | Type.Object _ -> build_obj at s self_id es obj_typ
+  | Type.Object _ | T.Module -> build_obj at s self_id es obj_typ
   | Type.Actor -> build_actor at self_id es obj_typ
 
+and build_field {Type.lab; Type.typ} =
+  { it = { I.name = I.Name lab @@ no_region
+         ; I.var = lab @@ no_region
+         }
+  ; at = no_region
+  ; note = typ
+  }
+
 and build_fields obj_typ =
     match obj_typ with
     | Type.Obj (_, fields) ->
-      List.map (fun {Type.lab; Type.typ} ->
-        { it = { I.name = I.Name lab @@ no_region
-               ; I.var = lab @@ no_region
-               }
-        ; at = no_region
-        ; note = typ
-        }) fields
+      List.map build_field fields
     | _ -> assert false
 
 and build_actor at self_id es obj_typ =
@@ -155,6 +157,8 @@ and block force_unit ds =
   | false, S.LetD (p', e') ->
     let x = fresh_var "x" (e'.note.S.note_typ) in
     (extra @ List.map dec prefix @ [letD x (exp e'); letP (pat p') x], x)
+  | false, S.ModuleD (x, _) ->
+    (extra @ List.map dec ds, idE x last.note.S.note_typ)
   | _, _ ->
     (extra @ List.map dec ds, tupE [])
 
@@ -216,6 +220,24 @@ and dec' at n d = match d with
       note = { S.note_typ = fun_typ; S.note_eff = T.Triv }
     } in
     I.LetD (varPat, fn)
+  | S.ModuleD(id, ds) ->
+    (build_module id ds (n.S.note_typ)).it
+
+
+and field_typ_to_obj_entry (f: T.field) =
+  match f.T.typ with
+  | T.Kind _ -> []
+  | _ -> [ build_field f ]
+
+and build_module id ds typ =
+  let self = idE id typ in
+  let (s, fs) = T.as_obj typ in
+  letD self
+    (blockE
+       (decs ds)
+       (newObjE T.Module
+          (List.concat (List.map field_typ_to_obj_entry fs)) typ));
+          (* ^^^^ TBR: do these need to be sorted? *)
 
 and cases cs = List.map case cs
 
@@ -309,30 +331,46 @@ and prog (p : Syntax.prog) : Ir.prog =
     }
 
 
+let declare_import imp_env (f, (prog:Syntax.prog))  =
+  let open Source in
+  let t = Type.Env.find f imp_env in
+  let typ_note =  { Syntax.empty_typ_note with Syntax.note_typ = t } in
+  match prog.it with
+  |  [{it = Syntax.ExpD _;_}] ->
+     { it = Syntax.LetD
+              (
+                { it = Syntax.VarP (id_of_full_path f)
+                ; at = no_region
+                ; note = t
+                }
+              , { it = Syntax.BlockE prog.it
+                ; at = no_region
+                ; note = typ_note
+                }
+              )
+     ; at = no_region
+     ; note = typ_note
+     }
+  (* HACK: to be removed once we support module expressions *)
+  |  ds ->
+     { it = Syntax.ModuleD
+              (  id_of_full_path f
+               , ds
+              )
+     ; at = no_region
+     ; note = typ_note
+     }
+
 
 let combine_files imp_env libraries progs : Syntax.prog =
   (* This is a hack until the backend has explicit support for libraries *)
   let open Source in
-  { it = List.map (fun (f, prog) ->
-      let t = Type.Env.find f imp_env in
-      { it = Syntax.LetD
-        ( { it = Syntax.VarP (id_of_full_path f)
-          ; at = no_region
-          ; note = t
-          }
-        , { it = Syntax.BlockE prog.it
-          ; at = no_region
-          ; note = { Syntax.empty_typ_note with Syntax.note_typ = t }
-          }
-        )
-      ; at = no_region
-      ; note = { Syntax.empty_typ_note with Syntax.note_typ = t }
-      }) libraries
-    @ List.concat (List.map (fun p -> p.it) progs)
+  { it = List.map (declare_import imp_env) libraries
+         @ List.concat (List.map (fun p -> p.it) progs)
   ; at = no_region
   ; note = match progs with
-    | [prog] -> prog.Source.note
-    | _ -> "all"
+           | [prog] -> prog.Source.note
+           | _ -> "all"
   }
 
 let transform p = prog p
diff --git a/src/effect.ml b/src/effect.ml
index 780227c403d..572149aace1 100644
--- a/src/effect.ml
+++ b/src/effect.ml
@@ -104,6 +104,10 @@ and infer_effect_dec dec =
   | TypD _
   | ClassD _ ->
     T.Triv
+  | ModuleD (_,decs) ->
+    let es = List.map effect_dec decs in
+    List.fold_left max_eff Type.Triv es
+
 
 (* effect inference on Ir *)
 
diff --git a/src/env.ml b/src/env.ml
index fc2d8ecd674..95806081ba4 100644
--- a/src/env.ml
+++ b/src/env.ml
@@ -32,4 +32,5 @@ struct
   let disjoint_union env1 env2 = union (fun k _ _ -> raise (Clash k)) env1 env2
   let disjoint_unions envs = List.fold_left disjoint_union empty envs
   let disjoint_add k x env = disjoint_union env (singleton k x)
+
 end
diff --git a/src/interpret.ml b/src/interpret.ml
index 039897cade7..f4d35669aea 100644
--- a/src/interpret.ml
+++ b/src/interpret.ml
@@ -622,6 +622,7 @@ and declare_dec dec : val_env =
   | LetD (pat, _) -> declare_pat pat
   | VarD (id, _) -> declare_id id
   | ClassD (id, _, _, _, _, _) -> declare_id {id with note = ()}
+  | ModuleD (id, _) -> declare_id id
 
 and declare_decs decs ve : val_env =
   match decs with
@@ -658,6 +659,12 @@ and interpret_dec env dec (k : V.value V.cont) =
     let v = V.Func (V.call_conv_of_typ dec.note.note_typ, f) in
     define_id env {id with note = ()} v;
     k v
+  | ModuleD (id, decs) ->
+    let ve = ref V.Env.empty in
+    interpret_block env decs (Some ve) (fun v ->
+      let v = V.Obj (V.Env.map Lib.Promise.value (!ve)) in
+      define_id env id v;
+      k v)
 
 and interpret_decs env decs (k : V.value V.cont) =
   match decs with
@@ -712,6 +719,12 @@ let interpret_library scope (filename, p) : scope =
     interpret_block env p.it (Some ve) (fun v -> vo := Some v)
   );
   Scheduler.run ();
-  library_scope filename (Lib.Option.value !vo) scope
-
+  let v = match p.it with
+    | [ { it = ExpD _ ; _ } ] ->
+      Lib.Option.value !vo
+    (* HACK: to be remove once we support module expressions, remove ModuleD *)
+    | ds ->
+      V.Obj (V.Env.map Lib.Promise.value (!ve))
+  in
+  library_scope filename v scope
 
diff --git a/src/lexer.mll b/src/lexer.mll
index 1b7d1003baa..b68892b2454 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -199,6 +199,7 @@ rule token mode = parse
   | "if" { IF }
   | "in" { IN }
   | "import" { IMPORT }
+  | "module" { MODULE }
   | "new" { NEW }
   | "not" { NOT }
   | "null" { NULL }
diff --git a/src/parser.mly b/src/parser.mly
index cf224042140..4653071aa0a 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -98,7 +98,7 @@ let share_expfield (ef : exp_field) =
 %token FUNC TYPE OBJECT ACTOR CLASS PRIVATE NEW SHARED
 %token SEMICOLON SEMICOLON_EOL COMMA COLON SUB DOT QUEST
 %token AND OR NOT
-%token IMPORT
+%token IMPORT MODULE
 %token DEBUG_SHOW
 %token ASSERT
 %token ADDOP SUBOP MULOP DIVOP MODOP POWOP
@@ -195,6 +195,13 @@ seplist(X, SEP) :
   | (* empty *) { Type.Local @@ no_region }
   | SHARED { Type.Sharable @@ at $sloc }
 
+(* paths *)
+
+path :
+  | x=id
+    { IdH x @! at $sloc }
+  | p=path DOT x=id
+    { DotH (p, x) @! at $sloc }
 
 (* Types *)
 
@@ -215,6 +222,8 @@ typ_nullary :
     { (match ts with [t] -> ParT(t) | _ -> TupT(ts)) @! at $sloc }
   | x=id tso=typ_args?
     { VarT(x, Lib.Option.get tso []) @! at $sloc }
+  | p=path DOT x=id tso=typ_args?
+    { PathT(p, x, Lib.Option.get tso []) @! at $sloc }
   | LBRACKET m=var_opt t=typ RBRACKET
     { ArrayT(m, t) @! at $sloc }
   | tfs=typ_obj
@@ -584,6 +593,9 @@ dec_nonvar :
         then efs
         else List.map share_expfield efs
       in ClassD(xf "class" $sloc, tps, s, p, x, efs') @? at $sloc }
+  | MODULE xf=id_opt EQ? LCURLY ds=seplist(dec, semicolon) RCURLY
+    { let _named, id = xf "module" $sloc in
+      ModuleD(id, ds) @? at $sloc }
 
 dec :
   | d=dec_var
diff --git a/src/resolve_import.ml b/src/resolve_import.ml
index 5a2b041c722..e0bea8cf20d 100644
--- a/src/resolve_import.ml
+++ b/src/resolve_import.ml
@@ -104,6 +104,8 @@ and dec env d = match d.it with
     exp env e
   | ClassD (_, _, _, _ , _, efs) ->
     List.iter (fun ef -> dec env ef.it.dec) efs
+  | ModuleD(_, ds) ->
+    decs env ds
 
 let prog env p = decs env p.it
 
diff --git a/src/serialization.ml b/src/serialization.ml
index 162bf105412..5cae16ff2f0 100644
--- a/src/serialization.ml
+++ b/src/serialization.ml
@@ -88,7 +88,7 @@ module Transform() = struct
     | T.Variant cts -> T.(Variant (map_constr_typ t_typ cts))
     | T.Obj (s, fs) -> T.Obj (s, List.map t_field fs)
     | T.Mut t -> T.Mut (t_typ t)
-
+    | T.Kind(c,k) -> T.Kind(t_con c, t_kind k) (* TBR *)
     | T.Serialized t -> assert false (* This transformation should only run once *)
     | T.Async t -> assert false (* Should happen after async-translation *)
 
diff --git a/src/static.ml b/src/static.ml
index 6d893a02ebf..fa0919ae16b 100644
--- a/src/static.ml
+++ b/src/static.ml
@@ -78,6 +78,7 @@ and dec m d = match d.it with
   | ExpD e -> exp m e
   | LetD (p, e) -> triv m p; exp m e
   | VarD _ -> err m d.at
+  | ModuleD (_, ds) -> List.iter (dec m) ds
 
 and triv m p = match p.it with
   | (WildP | VarP _) -> ()
diff --git a/src/syntax.ml b/src/syntax.ml
index 1d3245b0129..aa3af95ca0d 100644
--- a/src/syntax.ml
+++ b/src/syntax.ml
@@ -19,7 +19,15 @@ type obj_sort = Type.obj_sort Source.phrase
 type mut = mut' Source.phrase
 and mut' = Const | Var
 
+
+and path = (path', Type.typ) Source.annotated_phrase
+
+and path' =
+  | IdH  of id
+  | DotH of path * id
+
 type typ = (typ', Type.typ) Source.annotated_phrase
+
 and typ' =
   | PrimT of string                                (* primitive *)
   | VarT of id * typ list                          (* constructor *)
@@ -31,6 +39,7 @@ and typ' =
   | FuncT of sharing * typ_bind list * typ * typ   (* function *)
   | AsyncT of typ                                  (* future *)
   | ParT of typ                                    (* parentheses, used to control function arity only *)
+  | PathT of path * id * typ list                  (* type projection *)
 (*
   | UnionT of type * typ                           (* union *)
   | AtomT of string                                (* atom *)
@@ -183,7 +192,7 @@ and dec' =
   | TypD of typ_id * typ_bind list * typ       (* type *)
   | ClassD of                                  (* class *)
       typ_id * typ_bind list * obj_sort * pat * id * exp_field list
-
+  | ModuleD of id * dec list
 
 (* Program *)
 
diff --git a/src/type.ml b/src/type.ml
index ea3b9622844..c4e728f1d08 100644
--- a/src/type.ml
+++ b/src/type.ml
@@ -5,7 +5,7 @@ type var = string
 
 type control = Returns | Promises (* Returns a computed value or immediate promise *)
 type sharing = Local | Sharable
-type obj_sort = Object of sharing | Actor
+type obj_sort = Object of sharing | Actor | Module
 type eff = Triv | Await
 
 type prim =
@@ -39,6 +39,7 @@ and typ =
   | Any                                       (* top *)
   | Non                                       (* bottom *)
   | Pre                                       (* pre-type *)
+  | Kind of con * kind
 
 and bind = {var : var; bound : typ}
 and field = {lab : lab; typ : typ}
@@ -85,7 +86,14 @@ let prim = function
 
 let seq = function [t] -> t | ts -> Tup ts
 
-let compare_field {lab = l1; _} {lab = l2; _} = compare l1 l2
+
+let compare_field f1 f2 =
+  match f1,f2 with
+  | {lab = l1; typ = Kind _}, {lab = l2; typ = Kind _ } -> compare l1 l2
+  | {lab = l1; typ = Kind _}, {lab = l2; typ = _ } -> -1
+  | {lab = l1; typ = _}, {lab = l2; typ = Kind _ } -> 1
+  | {lab = l1; typ = _}, {lab = l2; typ = _ } -> compare l1 l2
+
 let compare_summand (c1, _) (c2, _) = compare c1 c2
 
 let iter_obj t =
@@ -134,6 +142,7 @@ let rec shift i n t =
   | Any -> Any
   | Non -> Non
   | Pre -> Pre
+  | Kind (c,k) -> Kind (c, shift_kind i n k)
 
 and shift_bind i n {var; bound} =
   {var; bound = shift i n bound}
@@ -141,6 +150,14 @@ and shift_bind i n {var; bound} =
 and shift_field i n {lab; typ} =
   {lab; typ = shift i n typ}
 
+and shift_kind i n k =
+  match k with
+  | Def (tbs, t) ->
+    let i' = i + List.length tbs in
+    Def (List.map (shift_bind i' n) tbs, shift i' n t)
+  | Abs (tbs, t) ->
+    let i' = i + List.length tbs in
+    Abs (List.map (shift_bind i' n) tbs, shift i' n t)
 
 (* First-order substitution *)
 
@@ -170,6 +187,7 @@ let rec subst sigma t =
   | Any -> Any
   | Non -> Non
   | Pre -> Pre
+  | Kind (c,k) -> Kind (c, subst_kind sigma k)
 
 and subst_bind sigma {var; bound} =
   {var; bound = subst sigma bound}
@@ -177,6 +195,16 @@ and subst_bind sigma {var; bound} =
 and subst_field sigma {lab; typ} =
   {lab; typ = subst sigma typ}
 
+and subst_kind sigma k =
+  match k with
+  | Def (tbs, t) ->
+    let sigma' = ConEnv.map (shift 0 (List.length tbs)) sigma in
+    Def (List.map (subst_bind sigma') tbs,
+         subst sigma' t)
+  | Abs (tbs, t) ->
+    let sigma' = ConEnv.map (shift 0 (List.length tbs)) sigma in
+    Abs (List.map (subst_bind sigma') tbs,
+         subst sigma' t)
 
 (* Handling binders *)
 
@@ -211,6 +239,8 @@ let rec open' i ts t =
   | Any -> Any
   | Non -> Non
   | Pre -> Pre
+  | Kind (c,k) ->
+    Kind (c, open_kind i ts k)
 
 and open_bind i ts {var; bound} =
   {var; bound = open' i ts bound}
@@ -218,6 +248,15 @@ and open_bind i ts {var; bound} =
 and open_field i ts {lab; typ} =
   {lab; typ = open' i ts typ}
 
+and open_kind i ts k =
+  match k with
+  | Def (tbs, t) ->
+    let i' = i + List.length tbs in
+    Def (List.map (open_bind i' ts) tbs, open' i' ts t)
+  | Abs (tbs, t) ->
+    let i' = i + List.length tbs in
+    Abs (List.map (open_bind i' ts) tbs, open' i' ts t)
+
 let open_ ts t =
   if ts = [] then t else
   open' 0 ts t
@@ -328,7 +367,6 @@ let as_async_sub t = match promote t with
   | Non -> Non
   | _ -> invalid "as_async_sub"
 
-
 let inst_func_type fun_ty sort typs =
     let _, tbs, t2, t3 = as_func_sub sort (List.length typs) fun_ty in
     let t_arg = open_ typs t2 in
@@ -336,10 +374,20 @@ let inst_func_type fun_ty sort typs =
     t_arg, t_ret
 
 let lookup_field lab' tfs =
-  match List.find_opt (fun {lab; _} -> lab = lab') tfs with
+  match List.find_opt (fun {lab; typ } ->
+                          match typ with Kind _ -> false
+                          | _ -> lab = lab') tfs with
   | Some {typ = t; _} -> t
   | None -> invalid "lookup_field"
 
+let lookup_typ_field lab' tfs =
+  match List.find_opt (fun {lab; typ } ->
+            match typ with
+            | Kind (c, k) -> lab=lab'
+            | _ -> false) tfs with
+  | Some {typ = Kind (c,k); _} -> (c,k)
+  | Some _ -> assert false
+  | None -> invalid "lookup_typ_field"
 
 (* Span *)
 
@@ -359,7 +407,7 @@ let rec span = function
   | Mut t -> span t
   | Serialized t -> None
   | Non -> Some 0
-
+  | Kind _ -> assert false (* TBR *)
 
 (* Avoiding local constructors *)
 
@@ -393,6 +441,9 @@ let rec avoid' cons = function
   | Obj (s, fs) -> Obj (s, List.map (avoid_field cons) fs)
   | Mut t -> Mut (avoid' cons t)
   | Serialized t -> Serialized (avoid' cons t)
+  | Kind (c,k) -> Kind(c, avoid_kind cons k) (* TBR *)
+
+
 
 and avoid_bind cons {var; bound} =
   {var; bound = avoid' cons bound}
@@ -400,6 +451,15 @@ and avoid_bind cons {var; bound} =
 and avoid_field cons {lab; typ} =
   {lab; typ = avoid' cons typ}
 
+and avoid_kind cons k =
+  match k with
+  | Def (tbs, t) ->
+    Def (List.map (avoid_bind cons) tbs,
+         avoid' cons t)
+  | Abs (tbs, t) ->
+    Abs (List.map (avoid_bind cons) tbs,
+         avoid' cons t)
+
 let avoid cons t =
   if cons = ConSet.empty then t else
   avoid' cons t
@@ -438,12 +498,11 @@ let is_concrete t =
       | Async t -> go t
       | Obj (s, fs) -> List.for_all (fun f -> go f.typ) fs
       | Mut t -> go t
+      | Kind (c,k) -> assert false (* TBR *)
       | Serialized t -> go t
     end
   in go t
 
-
-
 (* Equivalence & Subtyping *)
 
 module S = Set.Make (struct type t = typ * typ let compare = compare end)
@@ -548,6 +607,8 @@ let rec rel_typ rel eq t1 t2 =
     eq_typ rel eq t1' t2'
   | Serialized t1', Serialized t2' ->
     eq_typ rel eq t1' t2' (* TBR: eq or sub? Does it matter? *)
+  | Kind (c1, k1), Kind (c2, k2) ->
+    Con.eq c1 c2 (* && eq_kind k1 k2 *)
   | _, _ -> false
   end
 
@@ -729,6 +790,8 @@ let rec string_of_typ_nullary vs = function
   | Variant [] -> "{#}"
   | Variant cts ->
     sprintf "{%s}" (String.concat "; " (List.map (string_of_summand vs) cts))
+  | Kind (c,k) ->
+    sprintf "= {%s}" (string_of_kind k)
   | t -> sprintf "(%s)" (string_of_typ' vs t)
 
 and string_of_dom vs ts =
@@ -769,6 +832,10 @@ and string_of_typ' vs t =
     sprintf "shared %s" (string_of_typ_nullary vs (Obj (Object Local, fs)))
   | Obj (Actor, fs) ->
     sprintf "actor %s" (string_of_typ_nullary vs (Obj (Object Local, fs)))
+  | Obj (Module, fs) ->
+    sprintf "module %s" (string_of_typ_nullary vs (Obj (Object Local, fs)))
+  | Kind (c,k) ->
+    sprintf "= (%s,%s)" (Con.to_string c) (string_of_kind k)
   | Mut t ->
     sprintf "var %s" (string_of_typ' vs t)
   | Serialized t ->
@@ -776,7 +843,12 @@ and string_of_typ' vs t =
   | t -> string_of_typ_nullary vs t
 
 and string_of_field vs {lab; typ} =
-  sprintf "%s : %s" lab (string_of_typ' vs typ)
+  match typ with
+  | Kind (c,k) ->
+    let op, sbs, st = strings_of_kind k in
+    sprintf "type %s%s %s %s" lab sbs op st
+  | _ ->
+    sprintf "%s : %s" lab (string_of_typ' vs typ)
 
 and string_of_summand vs = function
   | (tag, Tup []) -> sprintf "#%s" tag
@@ -798,10 +870,8 @@ and string_of_binds vs vs' = function
   | [] -> ""
   | tbs -> "<" ^ String.concat ", " (List.map2 (string_of_bind vs) vs' tbs) ^ ">"
 
-let string_of_typ = string_of_typ' []
-let _ = str := string_of_typ
 
-let strings_of_kind k =
+and strings_of_kind k =
   let op, tbs, t =
     match k with
     | Def (tbs, t) -> "=", tbs, t
@@ -810,10 +880,12 @@ let strings_of_kind k =
   let vs = vars_of_binds [] tbs in
   op, string_of_binds vs vs tbs, string_of_typ' vs t
 
-let string_of_kind k =
+and string_of_kind k =
   let op, sbs, st = strings_of_kind k in
   sprintf "%s %s%s" op sbs st
 
+let string_of_typ = string_of_typ' []
+let _ = str := string_of_typ
 
 let rec string_of_typ_expand t =
   let s = string_of_typ t in
diff --git a/src/type.mli b/src/type.mli
index a43f3196ff4..8059e530e3f 100644
--- a/src/type.mli
+++ b/src/type.mli
@@ -5,7 +5,7 @@ type var = string
 
 type control = Returns | Promises (* returns a computed value or immediate promise *)
 type sharing = Local | Sharable
-type obj_sort = Object of sharing | Actor
+type obj_sort = Object of sharing | Actor | Module
 type eff = Triv | Await
 
 type prim =
@@ -39,6 +39,9 @@ and typ =
   | Any                                       (* top *)
   | Non                                       (* bottom *)
   | Pre                                       (* pre-type *)
+  | Kind of con * kind
+
+
 
 and bind = {var : var; bound : typ}
 and field = {lab : lab; typ : typ}
@@ -49,6 +52,7 @@ and kind =
   | Abs of bind list * typ
 
 
+
 (* Short-hands *)
 
 val unit : typ
@@ -99,11 +103,20 @@ val as_func_sub : sharing -> int -> typ -> sharing * bind list * typ * typ
 val as_mono_func_sub : typ -> typ * typ
 val as_async_sub : typ -> typ
 
+(* n-ary argument/result sequences *)
+
 val seq : typ list -> typ
 val as_seq : typ -> typ list
 val inst_func_type : typ -> sharing -> typ list -> (typ * typ)
 
+(* field lookup, namespace sensitive *)
+
+val lookup_typ_field : string -> field list -> (con * kind)
+
 val lookup_field : string -> field list -> typ
+
+(* field ordering *)
+
 val compare_field : field -> field -> int
 
 val map_constr_typ : (typ -> typ) -> (lab * typ) list -> (lab * typ) list
@@ -112,13 +125,14 @@ val compare_summand : (lab * typ) -> (lab * typ) -> int
 val span : typ -> int option
 
 
+
+
 (* Constructors *)
 
 val set_kind : con -> kind -> unit
 
 module ConSet : Dom.S with type elt = con
 
-
 (* Normalization and Classification *)
 
 val normalize : typ -> typ
diff --git a/src/typing.ml b/src/typing.ml
index 1af0bf1ad98..61e09bdfbc0 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -40,12 +40,16 @@ let adjoin_scope scope1 scope2 =
   { val_env = T.Env.adjoin scope1.val_env scope2.val_env;
     lib_env = T.Env.adjoin scope1.lib_env scope2.lib_env;
     typ_env = T.Env.adjoin scope1.typ_env scope2.typ_env;
-    con_env = T.ConSet.disjoint_union scope1.con_env scope2.con_env;
+    con_env = T.ConSet.union scope1.con_env scope2.con_env;
   }
 
+
+let adjoin_val_env scope ve = {scope with val_env = T.Env.adjoin scope.val_env ve}
+
 let library_scope f t =
   { empty_scope with lib_env = T.Env.add f t empty_scope.lib_env }
 
+
 (* Contexts (internal) *)
 
 type lab_env = T.typ T.Env.t
@@ -75,14 +79,15 @@ let env_of_scope msgs scope =
     msgs;
   }
 
-
 (* Error bookkeeping *)
 
-let type_error at text : Diag.message = Diag.{sev = Diag.Error; at; cat = "type"; text}
+let type_error at text : Diag.message =
+  Diag.{sev = Diag.Error; at; cat = "type"; text}
 let type_warning at text : Diag.message = Diag.{sev = Diag.Warning; at; cat = "type"; text}
 
 let local_error env at fmt =
-  Printf.ksprintf (fun s -> Diag.add_msg env.msgs (type_error at s)) fmt
+ Printf.ksprintf (fun s -> Diag.add_msg env.msgs (type_error at s)) fmt
+
 let error env at fmt =
   Printf.ksprintf (fun s -> Diag.add_msg env.msgs (type_error at s); raise Recover) fmt
 let warn env at fmt =
@@ -105,7 +110,7 @@ let adjoin env scope =
     vals = T.Env.adjoin env.vals scope.val_env;
     libs = T.Env.adjoin env.libs scope.lib_env;
     typs = T.Env.adjoin env.typs scope.typ_env;
-    cons = T.ConSet.disjoint_union env.cons scope.con_env;
+    cons = T.ConSet.union env.cons scope.con_env;
   }
 
 let adjoin_vals env ve = {env with vals = T.Env.adjoin env.vals ve}
@@ -139,6 +144,32 @@ let infer_mut mut : T.typ -> T.typ =
   | Const -> fun t -> t
   | Var -> fun t -> T.Mut t
 
+let rec check_path env path : T.typ =
+  let t = check_path' env path in
+  path.note <- t;
+  t
+
+and check_path' env path : T.typ =
+  match path.it with
+  | IdH id ->
+    begin
+      match T.Env.find_opt id.it env.vals with
+      | Some t ->
+        t
+      | None -> error env id.at "unbound path identifier %s" id.it
+    end
+  | DotH(path, id) ->
+    let t = check_path env path in
+    match T.promote t with
+    | T.Obj (T.Module, flds) ->
+      begin
+        try T.lookup_field id.it flds with
+        | _ -> error env id.at "field name %s does not exist in module type\n  %s"
+                     id.it (T.string_of_typ_expand t)
+      end
+    | _ -> error env id.at "expecting path of module type, found %s"
+             (T.string_of_typ_expand t)
+
 let rec check_typ env typ : T.typ =
   let t = check_typ' env typ in
   typ.note <- t;
@@ -209,6 +240,22 @@ and check_typ' env typ : T.typ =
     check_ids env false (List.map (fun (field : typ_field) -> field.it.id) fields);
     let fs = List.map (check_typ_field env sort.it) fields in
     T.Obj (sort.it, List.sort T.compare_field fs)
+  | PathT (p, id, typs) ->
+    let t = check_path env p in
+    (match T.promote t with
+     | T.Obj(_,flds) ->
+      begin
+        match T.lookup_typ_field id.it flds with
+        | (c,T.Def (tbs, t))
+        | (c,T.Abs (tbs, t)) ->
+          let ts = (* if env.pre
+                   then List.map (check_typ env) typs
+                   else *) check_typ_bounds env tbs typs typ.at in
+          T.Con (c, ts)
+        | exception _ -> error env id.at "unbound type identifier %s" id.it
+      end
+     |  _ -> error env id.at "path of unexpected type %s" id.it
+    )
   | ParT typ ->
     check_typ env typ
 
@@ -451,15 +498,14 @@ and infer_exp'' env exp : T.typ =
   | DotE (exp1, id) ->
     let t1 = infer_exp_promote env exp1 in
     (try
-      let _, tfs = T.as_obj_sub id.it t1 in
-      match List.find_opt (fun T.{lab; _} -> lab = id.it) tfs with
-      | Some {T.typ = t; _} -> t
-      | None ->
-        error env exp1.at "field name %s does not exist in type\n  %s"
-          id.it (T.string_of_typ_expand t1)
-    with Invalid_argument _ ->
-      error env exp1.at "expected object type, but expression produces type\n  %s"
-        (T.string_of_typ_expand t1)
+      let s, tfs = T.as_obj_sub id.it t1 in
+      try T.lookup_field id.it tfs with
+      |  Invalid_argument _ ->
+         error env exp1.at "field name %s does not exist in type\n  %s"
+           id.it (T.string_of_typ_expand t1)
+     with Invalid_argument _ ->
+       error env exp1.at "expected object type, but expression produces type\n  %s"
+         (T.string_of_typ_expand t1)
     )
   | AssignE (exp1, exp2) ->
     if not env.pre then begin
@@ -1002,6 +1048,8 @@ and pub_dec dec xs : region T.Env.t * region T.Env.t =
   | ClassD (id, _, _, _, _, _) ->
     pub_val_id {id with note = ()} (pub_typ_id id xs)
   | TypD (id, _, _) -> pub_typ_id id xs
+  | ModuleD (id, _) -> pub_val_id id xs
+
 
 and pub_pat pat xs : region T.Env.t * region T.Env.t =
   match pat.it with
@@ -1071,14 +1119,14 @@ and infer_block env decs at : T.typ * scope =
 and infer_block_decs env decs : scope =
   let scope = gather_block_typdecs env decs in
   let env' = adjoin {env with pre = true} scope in
-  let ce = infer_block_typdecs env' decs in
-  let env'' = adjoin env {scope with con_env = ce} in
-  let _ce' = infer_block_typdecs env'' decs in
+  let scope_ce = infer_block_typdecs env' decs in
+  let env'' = adjoin env scope_ce in
+  let scope_ce' = infer_block_typdecs env'' decs in
   (* TBR: assertion does not work for types with binders, due to stamping *)
   (* assert (ce = ce'); *)
-  let pre_ve' = gather_block_valdecs env decs in
-  let ve = infer_block_valdecs (adjoin_vals env'' pre_ve') decs in
-  {scope with val_env = ve; con_env = ce}
+  let pre_scope_ve' = gather_block_valdecs env decs scope_ce' in
+  let full_scope = infer_block_valdecs (adjoin env'' pre_scope_ve') decs pre_scope_ve' in
+  full_scope
 
 and infer_block_exps env decs : T.typ =
   match decs with
@@ -1116,6 +1164,12 @@ and infer_dec env dec : T.typ =
     t
   | TypD _ ->
     T.unit
+  | ModuleD (id, decs) ->
+    let t = try T.Env.find id.it env.vals with Not_found -> assert false in
+    if not env.pre then begin
+        ignore (infer_block env decs id.at) (* TBR *)
+    end;
+    t
   in
   let eff = A.infer_effect_dec dec in
   dec.note <- {note_typ = t; note_eff = eff};
@@ -1174,10 +1228,76 @@ and check_dec env t dec =
         (T.string_of_typ_expand t')
         (T.string_of_typ_expand t)
 
+(* move me to type.ml *)
+and module_of_scope scope =
+  let typ_fields =
+    T.Env.fold
+      (fun id con flds ->
+        let kind = Con.kind con in
+        { T.lab = id; T.typ = T.Kind (con,kind) }::flds) scope.typ_env  []
+  in
+  let fields =
+    T.Env.fold
+      (fun id typ flds ->
+        { T.lab = id; T.typ = typ }::flds) scope.val_env typ_fields
+  in
+  T.Obj(T.Module, List.sort T.compare_field fields)
+
+(* move me to type.ml *)
+and scope_of_module t =
+  match t with
+  | T.Obj (T.Module, flds) ->
+    List.fold_right
+      (fun {T.lab;T.typ} scope ->
+        match typ with
+        | T.Kind (c,k) ->
+          { scope with con_env = T.ConSet.add c scope.con_env;
+                       typ_env = T.Env.add lab c scope.typ_env}
+        | typ ->
+          { scope with val_env = T.Env.add lab typ scope.val_env }) flds empty_scope
+  | _ -> assert false
+
+
 (* Pass 1: collect type identifiers and their arity *)
 and gather_block_typdecs env decs : scope =
   List.fold_left (gather_dec_typdecs env) empty_scope decs
 
+
+
+and infer_val_path env exp : T.typ option =
+  match exp.it with
+  | ImportE (_, fp) ->
+    if !fp = "" then assert false;
+    T.Env.find_opt !fp env.libs
+  | VarE id ->
+    T.Env.find_opt id.it env.vals
+  | DotE(path, id) ->
+    begin
+      match infer_val_path env path with
+      | None -> None
+      | Some t ->
+        match T.promote t with
+        | T.Obj (T.Module, flds) ->
+          begin
+            match T.lookup_field id.it flds with
+            | t -> Some t
+            | exception _ -> None
+          end
+        | _ -> None
+    end
+  | _ -> None
+
+
+and is_module_path env exp =
+  match infer_val_path env exp with
+  | Some t ->
+    begin
+      match T.promote t with
+      | T.Obj (T.Module, flds) -> true
+      | _ -> false
+    end
+  | None -> false
+
 and gather_dec_typdecs env scope dec : scope =
   match dec.it with
   | ExpD _ | LetD _ | VarD _ -> scope
@@ -1186,7 +1306,9 @@ and gather_dec_typdecs env scope dec : scope =
       error env dec.at "duplicate definition for type %s in block" id.it;
     let pre_tbs = List.map (fun bind -> {T.var = bind.it.var.it; bound = T.Pre}) binds in
     let pre_k = T.Abs (pre_tbs, T.Pre) in
-    let c = Con.fresh id.it pre_k in
+    let c = match id.note with
+      | None -> let c = Con.fresh id.it pre_k in id.note <- Some c; c
+      | Some c -> c  in
     let te' = T.Env.add id.it c scope.typ_env in
     let ce' = T.ConSet.disjoint_add c scope.con_env in
     let ve' =  match dec.it with
@@ -1195,39 +1317,66 @@ and gather_dec_typdecs env scope dec : scope =
       | _ -> scope.val_env
     in
     { typ_env = te'; lib_env = scope.lib_env; con_env = ce'; val_env = ve' }
-
+  | ModuleD (id, decs) ->
+    (* TODO: this won't catch shadowing of ordinary val and module; instead gather vals here too?*)
+    if T.Env.mem id.it scope.val_env then
+      error env dec.at "duplicate definition for module %s in block" id.it;
+    let scope' = gather_block_typdecs env decs in
+    let ve' = T.Env.add id.it (module_of_scope scope') scope.val_env in
+    {val_env = ve';
+     typ_env = scope.typ_env;
+     lib_env = scope.lib_env;
+     con_env = scope.con_env }
 
 (* Pass 2 and 3: infer type definitions *)
-and infer_block_typdecs env decs : con_env =
-  List.fold_left
-    (fun ce dec ->
-      let ce' = infer_dec_typdecs env dec in
-      T.ConSet.disjoint_union ce ce'
-    )  T.ConSet.empty decs
-
-and infer_dec_typdecs env dec : con_env =
+and infer_block_typdecs env decs : scope =
+  let _env', scope =
+    List.fold_left (fun (env, scope) dec ->
+      let scope' = infer_dec_typdecs env dec in
+      adjoin env scope', adjoin_scope scope scope'
+    ) (env, empty_scope) decs
+  in scope
+
+and infer_dec_typdecs env dec : scope =
   match dec.it with
+  | LetD ({ it = VarP id; _ }, exp) when is_module_path env exp ->
+    begin
+      match infer_val_path env exp with
+      | Some t -> { empty_scope with val_env = T.Env.singleton id.it t }
+      | None -> empty_scope
+    end
   | ExpD _ | LetD _ | VarD _ ->
-    T.ConSet.empty
-  | TypD (id, binds, typ) ->
-    let c = T.Env.find id.it env.typs in
+    empty_scope
+  | TypD (con_id, binds, typ) ->
+    let c = T.Env.find con_id.it env.typs in
     let cs, ts, te, ce = check_typ_binds {env with pre = true} binds in
     let env' = adjoin_typs env te ce in
     let t = check_typ env' typ in
     let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in
     let k = T.Def (tbs, T.close cs t) in
-    infer_id_typdecs id c k
+    { empty_scope with
+      typ_env = T.Env.singleton con_id.it c ;
+      con_env = infer_id_typdecs con_id c k }
   | ClassD (id, binds, sort, pat, self_id, fields) ->
     let c = T.Env.find id.it env.typs in
     let cs, ts, te, ce = check_typ_binds {env with pre = true} binds in
     let env' = adjoin_typs {env with pre = true} te ce in
     let _, ve = infer_pat env' pat in
     let self_typ = T.Con (c, List.map (fun c -> T.Con (c, [])) cs) in
-    let env'' = add_val (adjoin_vals env' ve) self_id.it self_typ in 
+    let env'' = add_val (adjoin_vals env' ve) self_id.it self_typ in
     let t = infer_obj env'' sort.it fields dec.at in
     let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in
     let k = T.Def (tbs, T.close cs t) in
-    infer_id_typdecs id c k
+    { empty_scope with
+      typ_env = T.Env.singleton id.it c ;
+      con_env =     infer_id_typdecs id c k }
+  | ModuleD (id, decs) ->
+    let t = T.Env.find id.it env.vals in
+    let scope = scope_of_module t in
+    let env' = adjoin env scope in
+    let mod_scope = infer_block_typdecs env' decs in
+    { empty_scope with con_env = mod_scope.con_env;
+                       val_env = T.Env.singleton id.it (module_of_scope mod_scope)}
 
 and infer_id_typdecs id c k : con_env =
   assert (match k with T.Abs (_, T.Pre) -> false | _ -> true);
@@ -1239,17 +1388,23 @@ and infer_id_typdecs id c k : con_env =
   );
   T.ConSet.singleton c
 
-
 (* Pass 4: collect value identifiers *)
-and gather_block_valdecs env decs : val_env =
-  List.fold_left (gather_dec_valdecs env) T.Env.empty decs
+(* TODO: consider merging with gather_dec_type_decs so we can reject duplicate mod and
+   val ids *)
+and gather_block_valdecs env decs scope : scope =
+  List.fold_left (gather_dec_valdecs env) scope decs
 
-and gather_dec_valdecs env ve dec : val_env =
+and gather_dec_valdecs env scope dec : scope =
   match dec.it with
-  | ExpD _ | TypD _ -> ve
-  | LetD (pat, _) -> gather_pat env ve pat
-  | VarD (id, _) -> gather_id env ve id
-  | ClassD (id, _ , _, _, _, _) -> gather_id env ve {id with note = ()}
+  | ExpD _ | TypD _ -> scope
+  | LetD (pat, _) -> adjoin_val_env scope (gather_pat env scope.val_env pat)
+  | VarD (id, _) -> adjoin_val_env scope (gather_id env scope.val_env id)
+  | ClassD (id, _ , _, _, _, _) ->  adjoin_val_env scope (gather_id env scope.val_env {id with note = ()})
+  | ModuleD (id, decs) ->
+    let t = T.Env.find id.it scope.val_env in
+    let mod_scope = scope_of_module t in
+    let mod_scope = gather_block_valdecs env decs mod_scope in
+    adjoin_val_env scope (T.Env.singleton id.it (module_of_scope mod_scope))
 
 and gather_pat env ve pat : val_env =
   match pat.it with
@@ -1263,32 +1418,46 @@ and gather_pat_field env ve pf : val_env =
   gather_pat env ve pf.it.pat
 
 and gather_id env ve id : val_env =
-  if T.Env.mem id.it ve then
-    error env id.at "duplicate definition for %s in block" id.it;
+  begin
+    match T.Env.find_opt id.it ve with
+    | Some t ->
+      begin
+        match T.promote t with
+        | T.Obj (T.Module, _flds) ->
+          ()
+        | t ->
+          error env id.at "duplicate definition for %s in block" id.it
+      end
+    | None -> ()
+  end;
   T.Env.add id.it T.Pre ve
 
 (* Pass 5: infer value types *)
-and infer_block_valdecs env decs : val_env =
-  let _, ve =
-    List.fold_left (fun (env, ve) dec ->
-      let ve' = infer_dec_valdecs env dec in
-      adjoin_vals env ve', T.Env.adjoin ve ve'
-    ) (env, T.Env.empty) decs
-  in ve
-
-and infer_dec_valdecs env dec : val_env =
+and infer_block_valdecs env decs scope : scope =
+  let _, scope' =
+    List.fold_left (fun (env, scope) dec ->
+      let scope' = infer_dec_valdecs env dec in
+      adjoin env scope', adjoin_scope scope scope'
+    ) (env, scope) decs
+  in scope'
+
+and infer_dec_valdecs env dec : scope =
   match dec.it with
   | ExpD _ ->
-    T.Env.empty
+    empty_scope
   | LetD (pat, exp) ->
     let t = infer_exp {env with pre = true} exp in
     let ve' = check_pat_exhaustive env t pat in
-    ve'
+    { empty_scope with val_env = ve' }
   | VarD (id, exp) ->
     let t = infer_exp {env with pre = true} exp in
-    T.Env.singleton id.it (T.Mut t)
-  | TypD _ ->
-    T.Env.empty
+    { empty_scope with val_env = T.Env.singleton id.it (T.Mut t) }
+  | TypD (con_id, binds, typ) ->
+    let c = match con_id.note with
+      | Some c -> c | _ -> assert false in
+    { empty_scope with
+      typ_env = T.Env.singleton con_id.it c;
+      con_env = T.ConSet.singleton c }
   | ClassD (id, typ_binds, sort, pat, self_id, fields) ->
     let cs, ts, te, ce = check_typ_binds env typ_binds in
     let env' = adjoin_typs env te ce in
@@ -1297,8 +1466,22 @@ and infer_dec_valdecs env dec : val_env =
     let ts1 = match pat.it with TupP _ -> T.as_seq t1 | _ -> [t1] in
     let t2 = T.Con (c, List.map (fun c -> T.Con (c, [])) cs) in
     let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in
-    T.Env.singleton id.it (T.Func (T.Local, T.Returns, tbs, List.map (T.close cs) ts1, [T.close cs t2]))
-
+    { empty_scope with
+      val_env = T.Env.singleton id.it
+                  (T.Func (T.Local, T.Returns, tbs, List.map (T.close cs) ts1, [T.close cs t2]));
+      typ_env = T.Env.singleton id.it c;
+      con_env = T.ConSet.singleton c
+    }
+  | ModuleD (id, decs) ->
+    let t = try T.Env.find id.it env.vals with _ -> assert false  in
+    let mod_scope = scope_of_module t in
+    let mod_scope' =
+      infer_block_valdecs
+        (adjoin {env with pre = true} mod_scope)
+        decs empty_scope
+    in
+    { empty_scope with
+      val_env = T.Env.singleton id.it (module_of_scope mod_scope')}
 
 (* Programs *)
 
@@ -1315,16 +1498,23 @@ let infer_prog scope prog : (T.typ * scope) Diag.result =
         prog
     )
 
+let infer_library env prog at =
+  let typ,scope = infer_block env prog at in
+  match prog with
+  |  [{it = Syntax.ExpD _;_}] ->
+     typ
+  (* HACK: to be removed once we support module expressions, remove ModuleD *)
+  |  ds ->
+     module_of_scope scope
 
 let check_library scope (filename, prog) : scope Diag.result =
   Diag.with_message_store (fun msgs ->
     recover_opt
       (fun prog ->
         let env = env_of_scope msgs scope in
-        let (typ, _scope) = infer_block env prog.it prog.at in
+        let typ = infer_library env prog.it prog.at in
         Definedness.check_prog msgs prog;
         library_scope filename typ
       )
       prog
     )
-
diff --git a/test/repl/ok/double-import.stdout.ok b/test/repl/ok/double-import.stdout.ok
index 4c3261d64d4..729462bd50a 100644
--- a/test/repl/ok/double-import.stdout.ok
+++ b/test/repl/ok/double-import.stdout.ok
@@ -6,11 +6,13 @@ ActorScript 0.1 interpreter
 -- Interpreting empty.as:
 -- Interpreting stdin:
 -- Finished stdin:
+{} : module {}
 
 -- Parsing stdin:
 > -- Checking stdin:
 -- Interpreting stdin:
 -- Finished stdin:
+{} : module {}
 
 -- Parsing stdin:
 > 
diff --git a/test/run/import-module.as b/test/run/import-module.as
new file mode 100644
index 00000000000..732dda0e536
--- /dev/null
+++ b/test/run/import-module.as
@@ -0,0 +1,4 @@
+let L = import "lib/ListM.as";
+type stack = L.t<Int>;
+let s = L.cons<Int>(1,L.nil<Int>());
+
diff --git a/test/run/lib/ListM.as b/test/run/lib/ListM.as
new file mode 100644
index 00000000000..7b4aa2fec98
--- /dev/null
+++ b/test/run/lib/ListM.as
@@ -0,0 +1,4 @@
+type t<T> = ?(T, t<T>);
+func nil<T>() : t<T> = null;
+func cons<T>(x : T, l : t<T>) : t<T> = ?(x, l);
+
diff --git a/test/run/module1.as b/test/run/module1.as
new file mode 100644
index 00000000000..78a2366cdc4
--- /dev/null
+++ b/test/run/module1.as
@@ -0,0 +1,63 @@
+{
+module X =
+{ type T = Int;
+  let x:T = 1;
+};
+
+type T = X.T;
+let x = X.x;
+let y = X.x + 1;
+};
+
+
+{
+module X = {
+  type T<A> = (A,A);
+  let x:T<Int> = (1,2);
+};
+
+type T<A> = X.T<A>;
+
+let x = X.x;
+let (x1,x2) : T<Int> = X.x;
+assert (x1 == 1);
+assert (x2 == 2);
+
+};
+
+
+{
+module X = {
+  module X = {
+    type T<A> = (A,A);
+    let x:T<Int> = (1,2);
+  };
+};
+type T<A> = X.X.T<A>;
+
+let x = X.X.x;
+let (x1,x2) : T<Int> = X.X.x;
+assert (x1 == 1);
+assert (x2 == 2);
+};
+
+{
+module X = {
+  module X = {
+    type T<A> = (A,A);
+    let x:T<Int> = (1,2);
+  };
+};
+
+module Y = {
+  type T<A> = X.X.T<A>;
+
+  let x = X.X.x;
+  let (x1,x2) : T<Int> = X.X.x;
+  assert (x1 == 1);
+  assert (x2 == 2);
+};
+
+type U<A> = (X.X.T<A>,Y.T<A>);
+
+};
diff --git a/test/run/module2.as b/test/run/module2.as
new file mode 100644
index 00000000000..1edf73a741c
--- /dev/null
+++ b/test/run/module2.as
@@ -0,0 +1,5 @@
+// check types and terms have separate namespaces
+module X = { type x = Int; let x = 1; };
+type x = X.x;
+let x = X.x;
+/* assert (x == 1); */
\ No newline at end of file
diff --git a/test/run/module3.as b/test/run/module3.as
new file mode 100644
index 00000000000..baa59ecaebc
--- /dev/null
+++ b/test/run/module3.as
@@ -0,0 +1,12 @@
+
+// test equivalence of various type references
+module List = {
+  type List<A> = ?(A,List.List<A>);
+  func rev<A>(x : List<A>, acc : List.List<A>) : List<A> {
+    switch (x) {
+      case (null) acc;
+      case (?(h,t)) rev<A>(t,?(h,acc));
+    };
+  };
+};
+