diff --git a/samples/counter.txt b/samples/counter.txt
index e08a4bf2357..7fc902ec363 100644
--- a/samples/counter.txt
+++ b/samples/counter.txt
@@ -1,7 +1,7 @@
 -- Checking counter.as:
-type Counter <: actor {dec : shared () -> (); read : shared () -> async Int}
-let Counter : class Int -> Counter
-let c : Counter
+type Counter = actor {dec : shared () -> (); read : shared () -> async Int}
+let Counter : Int -> Counter
+let c : actor {dec : shared () -> (); read : shared () -> async Int}
 let show : (Text, Int) -> ()
 let showAsync : (Text, async Int) -> ()
 let testDec : () -> ()
@@ -287,8 +287,8 @@ testRead()
     <= ()
   <= ()
 -- Finished counter.as:
-let Counter : class Int -> Counter = func
-let c : Counter = {dec = func; read = func}
+let Counter : Int -> Counter = func
+let c : actor {dec : shared () -> (); read : shared () -> async Int} = {dec = func; read = func}
 let show : (Text, Int) -> () = func
 let showAsync : (Text, async Int) -> () = func
 let testDec : () -> () = func
diff --git a/samples/quicksort.txt b/samples/quicksort.txt
index b93dfa1e982..cc743310f44 100644
--- a/samples/quicksort.txt
+++ b/samples/quicksort.txt
@@ -1,10 +1,10 @@
 -- Checking quicksort.as:
 type Array<T> = [var T]
-type QS<T> <: {quicksort : (Array<T>, Nat, Nat) -> ()}
-let QS : class <T>((T, T) -> Int) -> QS<T>
+type QS<T> = {quicksort : (Array<T>, Nat, Nat) -> ()}
+let QS : <T>((T, T) -> Int) -> QS<T>
 let a : [var Int]
 let cmpi : (Int, Int) -> Int
-let qs : QS<Int>
+let qs : {quicksort : (Array<Int>, Nat, Nat) -> ()}
 -- Interpreting quicksort.as:
 QS(func)
   <= {quicksort = func}
@@ -97,8 +97,8 @@ quicksort([8, 3, 9, 5, 2], 0, 4)
     <= ()
   <= ()
 -- Finished quicksort.as:
-let QS : class <T>((T, T) -> Int) -> QS<T> = func
+let QS : <T>((T, T) -> Int) -> QS<T> = func
 let a : [var Int] = [2, 3, 5, 8, 9]
 let cmpi : (Int, Int) -> Int = func
-let qs : QS<Int> = {quicksort = func}
+let qs : {quicksort : (Array<Int>, Nat, Nat) -> ()} = {quicksort = func}
 
diff --git a/src/arrange_ir.ml b/src/arrange_ir.ml
index a9d50251f53..f10346b4e5a 100644
--- a/src/arrange_ir.ml
+++ b/src/arrange_ir.ml
@@ -67,8 +67,8 @@ and dec d = match d.it with
   | VarD (i, e) -> "VarD" $$ [id i; exp e]
   | FuncD (cc, i, tp, p, t, e) ->
     "FuncD" $$ [call_conv cc; id i] @ List.map typ_bind tp @ [pat p; typ t; exp e]
-  | TypD (c,k) ->
-    "TypD" $$ [con c; kind k]
+  | TypD c ->
+    "TypD" $$ [con c; kind (Type.kind c)]
 
 and typ_bind (tb : typ_bind) =
   Con.to_string tb.it.con $$ [typ tb.it.bound]
diff --git a/src/async.ml b/src/async.ml
index 8bb92b8e5bc..c2edab1eaa0 100644
--- a/src/async.ml
+++ b/src/async.ml
@@ -1,4 +1,4 @@
-
+module E = Env
 open Source
 module Ir = Ir
 open Ir
@@ -6,7 +6,7 @@ open Effect
 module T = Type
 open T
 open Construct
-   
+
 (* lower the async type itself
    - adds a final callback argument to every awaitable shared function, replace the result by unit
    - transforms types, introductions and eliminations awaitable shared functions only, leaving non-awaitable shared functions unchanged.
@@ -15,374 +15,405 @@ open Construct
    (for debugging, the `flattening` function can be used to disable argument flattening and use uniform pairing instead)
  *)
 
-let unary typ = [typ]
-
-let nary typ = T.as_seq typ
-
-let replyT as_seq typ = T.Func(T.Sharable, T.Returns, [], as_seq typ, [])
-
-let fullfillT as_seq typ = T.Func(T.Local, T.Returns, [], as_seq typ, [])
-
-let t_async as_seq t =
-  T.Func (T.Local, T.Returns, [], [T.Func(T.Local, T.Returns, [],as_seq t,[])], [])
-
-let new_async_ret as_seq t = [t_async as_seq t;fullfillT as_seq t]
-
-let new_asyncT =
-  T.Func (
-    T.Local,
-    T.Returns,
-    [ { var = "T"; bound = T.Shared } ],
-    [],
-    new_async_ret unary (T.Var ("T", 0))
-  )
-
-let new_asyncE =
-  idE ("@new_async"@@no_region) new_asyncT
-
-let new_async t1 =
-  let call_new_async =
-    callE new_asyncE
-      [t1]
-      (tupE [])
-      (T.seq (new_async_ret unary t1)) in
-  let async  = fresh_id (typ (projE call_new_async 0)) in
-  let fullfill = fresh_id (typ (projE call_new_async 1)) in
-  (async,fullfill),call_new_async
-
-let letP p e =  {it = LetD(p, e);
-                 at = no_region;
-                 note = {e.note with note_typ = T.unit}}
-
-let new_nary_async_reply t1 =
-  let (unary_async,unary_fullfill),call_new_async = new_async t1 in
-  let v' = fresh_id t1 in
-  let ts1 = T.as_seq t1 in
-  (* construct the n-ary async value, coercing the continuation, if necessary *)
-  let nary_async =
-    let k' = fresh_id (contT t1) in
-    match ts1 with
-    | [t] ->
-      unary_async
-    | ts ->
-      let seq_of_v' = tupE (List.mapi (fun i _ -> projE v' i) ts) in
-      k' --> (unary_async -*- ([v'] -->* (k' -*- seq_of_v')))
-  in
-  (* construct the n-ary reply message that sends a sequence of value to fullfill the async *)
-  let nary_reply =
-    let vs,seq_of_vs =
+(* written as a functor so we can allocate some temporary shared state without making it global *)
+
+module Transform() = struct
+
+  module ConRenaming = E.Make(struct type t = T.con let compare = Con.compare end)
+
+  (* the state *)
+
+  (* maps constructors to clones with the same stamp & name,
+     but fresh annotation state (think parallel universe ;->) *)
+
+  (* ensures that program fragments from corresponding passes have consistent constructor
+     definitions
+     (note, the actual state of the definition may be duplicated but always should be equivalent
+  *)
+
+  let con_renaming = ref ConRenaming.empty
+
+  let unary typ = [typ]
+
+  let nary typ = T.as_seq typ
+
+  let replyT as_seq typ = T.Func(T.Sharable, T.Returns, [], as_seq typ, [])
+
+  let fullfillT as_seq typ = T.Func(T.Local, T.Returns, [], as_seq typ, [])
+
+  let t_async as_seq t =
+    T.Func (T.Local, T.Returns, [], [T.Func(T.Local, T.Returns, [],as_seq t,[])], [])
+
+  let new_async_ret as_seq t = [t_async as_seq t;fullfillT as_seq t]
+
+  let new_asyncT =
+    T.Func (
+        T.Local,
+        T.Returns,
+        [ { var = "T"; bound = T.Shared } ],
+        [],
+        new_async_ret unary (T.Var ("T", 0))
+      )
+
+  let new_asyncE =
+    idE ("@new_async"@@no_region) new_asyncT
+
+  let new_async t1 =
+    let call_new_async =
+      callE new_asyncE
+        [t1]
+        (tupE [])
+        (T.seq (new_async_ret unary t1)) in
+    let async  = fresh_id (typ (projE call_new_async 0)) in
+    let fullfill = fresh_id (typ (projE call_new_async 1)) in
+    (async,fullfill),call_new_async
+
+  let letP p e =  {it = LetD(p, e);
+                   at = no_region;
+                   note = {e.note with note_typ = T.unit}}
+
+  let new_nary_async_reply t1 =
+    let (unary_async,unary_fullfill),call_new_async = new_async t1 in
+    let v' = fresh_id t1 in
+    let ts1 = T.as_seq t1 in
+    (* construct the n-ary async value, coercing the continuation, if necessary *)
+    let nary_async =
+      let k' = fresh_id (contT t1) in
       match ts1 with
       | [t] ->
-        let v = fresh_id t in
-        [v],v
+        unary_async
       | ts ->
-        let vs = List.map fresh_id ts in
-        vs, tupE vs
+        let seq_of_v' = tupE (List.mapi (fun i _ -> projE v' i) ts) in
+        k' --> (unary_async -*- ([v'] -->* (k' -*- seq_of_v')))
     in
-    vs -@>* (unary_fullfill -*-  seq_of_vs)
-  in
-  let async,reply = fresh_id (typ nary_async), fresh_id (typ nary_reply) in
-  (async,reply),blockE [letP (tupP [varP unary_async;varP unary_fullfill])  call_new_async;
-                    expD (tupE [nary_async;nary_reply])]
-
-
-let letEta e scope =
-  match e.it with
-  | VarE _ -> scope e (* pure, so reduce *)
-  | _  -> let f = fresh_id (typ e) in
-          letD f e :: (scope f) (* maybe impure; sequence *)
-
-let isAwaitableFunc exp =
-  match typ exp with
-  | T.Func (T.Sharable,T.Promises,_,_,[T.Async _]) -> true
-  | _ -> false
-
-let extendTup ts t2 = ts @ [t2]
-
-let extendTupP p1 p2 =
-  match p1.it with
-  | TupP ps ->
-    begin
-      match ps with
-      | [] -> p2, fun d -> (letP p1 (tupE [])::d)
-      | ps ->
-           tupP (ps@[p2]), fun d -> d
-    end
-  | _ -> tupP [p1;p2], fun d -> d
-
-(* Given sequence type ts, bind e of type (seq ts) to a
+    (* construct the n-ary reply message that sends a sequence of value to fullfill the async *)
+    let nary_reply =
+      let vs,seq_of_vs =
+        match ts1 with
+        | [t] ->
+          let v = fresh_id t in
+          [v],v
+        | ts ->
+          let vs = List.map fresh_id ts in
+          vs, tupE vs
+      in
+      vs -@>* (unary_fullfill -*-  seq_of_vs)
+    in
+    let async,reply = fresh_id (typ nary_async), fresh_id (typ nary_reply) in
+    (async,reply),blockE [letP (tupP [varP unary_async;varP unary_fullfill])  call_new_async;
+                          expD (tupE [nary_async;nary_reply])]
+
+
+  let letEta e scope =
+    match e.it with
+    | VarE _ -> scope e (* pure, so reduce *)
+    | _  -> let f = fresh_id (typ e) in
+            letD f e :: (scope f) (* maybe impure; sequence *)
+
+  let isAwaitableFunc exp =
+    match typ exp with
+    | T.Func (T.Sharable,T.Promises,_,_,[T.Async _]) -> true
+    | _ -> false
+
+  let extendTup ts t2 = ts @ [t2]
+
+  let extendTupP p1 p2 =
+    match p1.it with
+    | TupP ps ->
+      begin
+        match ps with
+        | [] -> p2, fun d -> (letP p1 (tupE [])::d)
+        | ps ->
+          tupP (ps@[p2]), fun d -> d
+      end
+    | _ -> tupP [p1;p2], fun d -> d
+
+  (* Given sequence type ts, bind e of type (seq ts) to a
    sequence of expressions supplied to decs d_of_es,
    preserving effects of e when the sequence type is empty.
    d_of_es must not duplicate or discard the evaluation of es.
- *)
-let letSeq ts e d_of_vs =
-  match ts with
-  | [] ->
-    (expD e)::d_of_vs []
-  | [t] ->
+   *)
+  let letSeq ts e d_of_vs =
+    match ts with
+    | [] ->
+      (expD e)::d_of_vs []
+    | [t] ->
       let x = fresh_id t in
       let p = varP x in
       (letP p e)::d_of_vs [x]
-  | ts ->
+    | ts ->
       let xs = List.map fresh_id ts in
       let p = tupP (List.map varP xs) in
       (letP p e)::d_of_vs (xs)
 
-let rec t_typ (t:T.typ) =
-  match t with
-  | T.Prim _
-  | Var _ -> t
-  | Con (c, ts) ->
-    Con (c, List.map t_typ ts)
-  | Array t -> Array (t_typ t)
-  | Tup ts -> Tup (List.map t_typ ts)
-  | Func (s, c, tbs, t1, t2) ->
-     begin
-       match s with
-       |  T.Sharable ->
-         begin
-           match t2 with
-           | [] ->
-              assert (c = T.Returns);
-              Func(s, c, List.map t_bind tbs, List.map t_typ t1, List.map t_typ t2)
-           | [Async t2] ->
-              assert (c = T.Promises);
-              Func (s, T.Returns, List.map t_bind tbs,
-                    extendTup (List.map t_typ t1) (replyT nary (t_typ t2)), [])
-           | _ -> assert false
-         end
-       | _ ->
+  let rec t_typ (t:T.typ) =
+    match t with
+    | T.Prim _
+      | Var _ -> t
+    | Con (c, ts) ->
+      Con (t_con c, List.map t_typ ts)
+    | Array t -> Array (t_typ t)
+    | Tup ts -> Tup (List.map t_typ ts)
+    | Func (s, c, tbs, t1, t2) ->
+      begin
+        match s with
+        |  T.Sharable ->
+           begin
+             match t2 with
+             | [] ->
+               assert (c = T.Returns);
+               Func(s, c, List.map t_bind tbs, List.map t_typ t1, List.map t_typ t2)
+             | [Async t2] ->
+               assert (c = T.Promises);
+               Func (s, T.Returns, List.map t_bind tbs,
+                     extendTup (List.map t_typ t1) (replyT nary (t_typ t2)), [])
+             | _ -> assert false
+           end
+        | _ ->
           Func (s, c, List.map t_bind tbs, List.map t_typ t1, List.map t_typ t2)
-     end
-  | Opt t -> Opt (t_typ t)
-  | Async t -> t_async nary (t_typ t)
-  | Obj (s, fs) -> Obj (s, List.map t_field  fs)
-  | Mut t -> Mut (t_typ t)
-  | Shared -> Shared
-  | Any -> Any
-  | Non -> Non
-  | Pre -> Pre
-
-and t_bind {var; bound} =
-  {var; bound = t_typ bound}
-
-and t_binds typbinds = List.map t_bind typbinds
-
-and t_kind k =
-  match k with
-  | T.Abs(typ_binds,typ) ->
-    T.Abs(t_binds typ_binds, t_typ typ)
-  | T.Def(typ_binds,typ) ->
-    T.Def(t_binds typ_binds, t_typ typ)
-
-and t_operator_type ot =
-  (* We recreate the reference here. That is ok, because it
+      end
+    | Opt t -> Opt (t_typ t)
+    | Async t -> t_async nary (t_typ t)
+    | Obj (s, fs) -> Obj (s, List.map t_field  fs)
+    | Mut t -> Mut (t_typ t)
+    | Shared -> Shared
+    | Any -> Any
+    | Non -> Non
+    | Pre -> Pre
+
+  and t_bind {var; bound} =
+    {var; bound = t_typ bound}
+
+  and t_binds typbinds = List.map t_bind typbinds
+
+  and t_kind k =
+    match k with
+    | T.Abs(typ_binds,typ) ->
+      T.Abs(t_binds typ_binds, t_typ typ)
+    | T.Def(typ_binds,typ) ->
+      T.Def(t_binds typ_binds, t_typ typ)
+
+  and t_con c =
+    match  ConRenaming.find_opt c (!con_renaming) with
+    | Some c' -> c'
+    | None ->
+      let clone = T.clone_con c (T.kind c) in
+      con_renaming := ConRenaming.add c clone (!con_renaming);
+      T.modify_kind clone t_kind;
+      clone
+
+  and t_operator_type ot =
+    (* We recreate the reference here. That is ok, because it
      we run after type inference. Once we move async past desugaring,
      it will be a pure value anyways. *)
-  t_typ ot
-
-and t_field {name; typ} =
-  { name; typ = t_typ typ }
-let rec t_exp (exp: exp) =
-  { it = t_exp' exp;
-    note = { note_typ = t_typ exp.note.note_typ;
-             note_eff = exp.note.note_eff};
-    at = exp.at;
-  }
-and t_exp' (exp:exp) =
-  let exp' = exp.it in
-  match exp' with
-  | PrimE _
-  | LitE _ -> exp'
-  | VarE id -> exp'
-  | UnE (ot, op, exp1) ->
-    UnE (t_operator_type ot, op, t_exp exp1)
-  | BinE (ot, exp1, op, exp2) ->
-    BinE (t_operator_type ot, t_exp exp1, op, t_exp exp2)
-  | RelE (ot, exp1, op, exp2) ->
-    RelE (t_operator_type ot, t_exp exp1, op, t_exp exp2)
-  | TupE exps ->
-    TupE (List.map t_exp exps)
-  | OptE exp1 ->
-    OptE (t_exp exp1)
-  | ProjE (exp1, n) ->
-    ProjE (t_exp exp1, n)
-  | ActorE (id, fields, typ) ->
-    let fields' = t_fields fields in
-    ActorE (id, fields', t_typ typ)
-  | DotE (exp1, id) ->
-    DotE (t_exp exp1, id)
-  | ActorDotE (exp1, id) ->
-    ActorDotE (t_exp exp1, id)
-  | AssignE (exp1, exp2) ->
-    AssignE (t_exp exp1, t_exp exp2)
-  | ArrayE (mut, t, exps) ->
-    ArrayE (mut, t_typ t, List.map t_exp exps)
-  | IdxE (exp1, exp2) ->
-    IdxE (t_exp exp1, t_exp exp2)
-  | CallE (cc,{it=PrimE "@await";_}, typs, exp2) ->
-    begin
-     match exp2.it with
-     | TupE [a;k] -> ((t_exp a) -*- (t_exp k)).it
-     | _ -> assert false
-    end
-  | CallE (cc,{it=PrimE "@async";_}, typs, exp2) ->
-    let t1, contT = match typ exp2 with
-      | Func(_,_,
-             [],
-             [Func(_,_,[],ts1,[]) as contT],
-             []) -> (* TBR, why isn't this []? *)
-        (t_typ (T.seq ts1),t_typ contT)
-      | t -> assert false in
-    let k = fresh_id contT in
-    let v1 = fresh_id t1 in
-    let post = fresh_id (T.Func(T.Sharable,T.Returns,[],[],[])) in
-    let u = fresh_id T.unit in
-    let ((nary_async,nary_reply),def) = new_nary_async_reply t1 in
-    (blockE [letP (tupP [varP nary_async; varP nary_reply]) def;
-             funcD k v1 (nary_reply -*- v1);
-             funcD post u (t_exp exp2 -*- k);
-             expD (post -*- tupE[]);
-             expD nary_async])
-      .it
-  | CallE (cc,exp1, typs, exp2) when isAwaitableFunc exp1 ->
-    let ts1,t2 =
-      match typ exp1 with
-      | T.Func (T.Sharable,T.Promises,tbs,ts1,[T.Async t2]) ->
-           List.map t_typ ts1, t_typ t2
-      | _ -> assert(false)
-    in
-    let exp1' = t_exp exp1 in
-    let exp2' = t_exp exp2 in
-    let typs = List.map t_typ typs in
-    let ((nary_async,nary_reply),def) = new_nary_async_reply t2 in
-    let _ = letEta in
-    (blockE (letP (tupP [varP nary_async; varP nary_reply]) def::
-               letEta exp1' (fun v1 ->
-                   letSeq ts1 exp2' (fun vs ->
-                       [expD (callE v1 typs (seqE (vs@[nary_reply])) T.unit);
-                        expD nary_async]))))
-      .it
-  | CallE (cc, exp1, typs, exp2)  ->
-    CallE(cc, t_exp exp1, List.map t_typ typs, t_exp exp2)
-  | BlockE (decs, ot) ->
-    BlockE (t_decs decs, t_typ ot)
-  | IfE (exp1, exp2, exp3) ->
-    IfE (t_exp exp1, t_exp exp2, t_exp exp3)
-  | SwitchE (exp1, cases) ->
-    let cases' = List.map
-                  (fun {it = {pat;exp}; at; note} ->
-                    {it = {pat = t_pat pat ;exp = t_exp exp}; at; note})
-                  cases
-    in
-    SwitchE (t_exp exp1, cases')
-  | WhileE (exp1, exp2) ->
-    WhileE (t_exp exp1, t_exp exp2)
-  | LoopE (exp1, exp2_opt) ->
-    LoopE (t_exp exp1, Lib.Option.map t_exp exp2_opt)
-  | ForE (pat, exp1, exp2) ->
-    ForE (t_pat pat, t_exp exp1, t_exp exp2)
-  | LabelE (id, typ, exp1) ->
-    LabelE (id, t_typ typ, t_exp exp1)
-  | BreakE (id, exp1) ->
-    BreakE (id, t_exp exp1)
-  | RetE exp1 ->
-    RetE (t_exp exp1)
-  | AsyncE _ -> assert false
-  | AwaitE _ -> assert false
-  | AssertE exp1 ->
-    AssertE (t_exp exp1)
-  | DeclareE (id, typ, exp1) ->
-    DeclareE (id, t_typ typ, t_exp exp1)
-  | DefineE (id, mut ,exp1) ->
-    DefineE (id, mut, t_exp exp1)
-  | NewObjE (sort, ids, t) ->
-    NewObjE (sort, ids, t_typ t)
-
-and t_dec dec =
-  { it = t_dec' dec.it;
-    note = { note_typ = t_typ dec.note.note_typ;
-             note_eff = dec.note.note_eff };
-    at = dec.at }
-
-and t_dec' dec' =
-  match dec' with
-  | ExpD exp -> ExpD (t_exp exp)
-  | TypD (con_id, k) ->
-    TypD (con_id, t_kind k)
-  | LetD (pat,exp) -> LetD (t_pat pat,t_exp exp)
-  | VarD (id,exp) -> VarD (id,t_exp exp)
-  | FuncD (cc, id, typbinds, pat, typT, exp) ->
-    let s = cc.Value.sort in
-    begin
-      match s with
-      | T.Local  ->
-         FuncD (cc, id, t_typ_binds typbinds, t_pat pat, t_typ typT, t_exp exp)
-      | T.Sharable ->
-         begin
-           match typ exp with
-           | T.Tup [] ->
+    t_typ ot
+
+  and t_field {name; typ} =
+    { name; typ = t_typ typ }
+  let rec t_exp (exp: exp) =
+    { it = t_exp' exp;
+      note = { note_typ = t_typ exp.note.note_typ;
+               note_eff = exp.note.note_eff};
+      at = exp.at;
+    }
+  and t_exp' (exp:exp) =
+    let exp' = exp.it in
+    match exp' with
+    | PrimE _
+      | LitE _ -> exp'
+    | VarE id -> exp'
+    | UnE (ot, op, exp1) ->
+      UnE (t_operator_type ot, op, t_exp exp1)
+    | BinE (ot, exp1, op, exp2) ->
+      BinE (t_operator_type ot, t_exp exp1, op, t_exp exp2)
+    | RelE (ot, exp1, op, exp2) ->
+      RelE (t_operator_type ot, t_exp exp1, op, t_exp exp2)
+    | TupE exps ->
+      TupE (List.map t_exp exps)
+    | OptE exp1 ->
+      OptE (t_exp exp1)
+    | ProjE (exp1, n) ->
+      ProjE (t_exp exp1, n)
+    | ActorE (id, fields, typ) ->
+      let fields' = t_fields fields in
+      ActorE (id, fields', t_typ typ)
+    | DotE (exp1, id) ->
+      DotE (t_exp exp1, id)
+    | ActorDotE (exp1, id) ->
+      ActorDotE (t_exp exp1, id)
+    | AssignE (exp1, exp2) ->
+      AssignE (t_exp exp1, t_exp exp2)
+    | ArrayE (mut, t, exps) ->
+      ArrayE (mut, t_typ t, List.map t_exp exps)
+    | IdxE (exp1, exp2) ->
+      IdxE (t_exp exp1, t_exp exp2)
+    | CallE (cc,{it=PrimE "@await";_}, typs, exp2) ->
+      begin
+        match exp2.it with
+        | TupE [a;k] -> ((t_exp a) -*- (t_exp k)).it
+        | _ -> assert false
+      end
+    | CallE (cc,{it=PrimE "@async";_}, typs, exp2) ->
+      let t1, contT = match typ exp2 with
+        | Func(_,_,
+               [],
+               [Func(_,_,[],ts1,[]) as contT],
+               []) -> (* TBR, why isn't this []? *)
+          (t_typ (T.seq ts1),t_typ contT)
+        | t -> assert false in
+      let k = fresh_id contT in
+      let v1 = fresh_id t1 in
+      let post = fresh_id (T.Func(T.Sharable,T.Returns,[],[],[])) in
+      let u = fresh_id T.unit in
+      let ((nary_async,nary_reply),def) = new_nary_async_reply t1 in
+      (blockE [letP (tupP [varP nary_async; varP nary_reply]) def;
+               funcD k v1 (nary_reply -*- v1);
+               funcD post u (t_exp exp2 -*- k);
+               expD (post -*- tupE[]);
+               expD nary_async])
+        .it
+    | CallE (cc,exp1, typs, exp2) when isAwaitableFunc exp1 ->
+      let ts1,t2 =
+        match typ exp1 with
+        | T.Func (T.Sharable,T.Promises,tbs,ts1,[T.Async t2]) ->
+          List.map t_typ ts1, t_typ t2
+        | _ -> assert(false)
+      in
+      let exp1' = t_exp exp1 in
+      let exp2' = t_exp exp2 in
+      let typs = List.map t_typ typs in
+      let ((nary_async,nary_reply),def) = new_nary_async_reply t2 in
+      let _ = letEta in
+      (blockE (letP (tupP [varP nary_async; varP nary_reply]) def::
+                 letEta exp1' (fun v1 ->
+                     letSeq ts1 exp2' (fun vs ->
+                         [expD (callE v1 typs (seqE (vs@[nary_reply])) T.unit);
+                          expD nary_async]))))
+        .it
+    | CallE (cc, exp1, typs, exp2)  ->
+      CallE(cc, t_exp exp1, List.map t_typ typs, t_exp exp2)
+    | BlockE (decs, ot) ->
+      BlockE (t_decs decs, t_typ ot)
+    | IfE (exp1, exp2, exp3) ->
+      IfE (t_exp exp1, t_exp exp2, t_exp exp3)
+    | SwitchE (exp1, cases) ->
+      let cases' = List.map
+                     (fun {it = {pat;exp}; at; note} ->
+                       {it = {pat = t_pat pat ;exp = t_exp exp}; at; note})
+                     cases
+      in
+      SwitchE (t_exp exp1, cases')
+    | WhileE (exp1, exp2) ->
+      WhileE (t_exp exp1, t_exp exp2)
+    | LoopE (exp1, exp2_opt) ->
+      LoopE (t_exp exp1, Lib.Option.map t_exp exp2_opt)
+    | ForE (pat, exp1, exp2) ->
+      ForE (t_pat pat, t_exp exp1, t_exp exp2)
+    | LabelE (id, typ, exp1) ->
+      LabelE (id, t_typ typ, t_exp exp1)
+    | BreakE (id, exp1) ->
+      BreakE (id, t_exp exp1)
+    | RetE exp1 ->
+      RetE (t_exp exp1)
+    | AsyncE _ -> assert false
+    | AwaitE _ -> assert false
+    | AssertE exp1 ->
+      AssertE (t_exp exp1)
+    | DeclareE (id, typ, exp1) ->
+      DeclareE (id, t_typ typ, t_exp exp1)
+    | DefineE (id, mut ,exp1) ->
+      DefineE (id, mut, t_exp exp1)
+    | NewObjE (sort, ids, t) ->
+      NewObjE (sort, ids, t_typ t)
+
+  and t_dec dec =
+    { it = t_dec' dec.it;
+      note = { note_typ = t_typ dec.note.note_typ;
+               note_eff = dec.note.note_eff };
+      at = dec.at }
+
+  and t_dec' dec' =
+    match dec' with
+    | ExpD exp -> ExpD (t_exp exp)
+    | TypD con_id ->
+      TypD (t_con con_id)
+    | LetD (pat,exp) -> LetD (t_pat pat,t_exp exp)
+    | VarD (id,exp) -> VarD (id,t_exp exp)
+    | FuncD (cc, id, typbinds, pat, typT, exp) ->
+      let s = cc.Value.sort in
+      begin
+        match s with
+        | T.Local  ->
+          FuncD (cc, id, t_typ_binds typbinds, t_pat pat, t_typ typT, t_exp exp)
+        | T.Sharable ->
+          begin
+            match typ exp with
+            | T.Tup [] ->
               FuncD (cc, id, t_typ_binds typbinds, t_pat pat, t_typ typT, t_exp exp)
-           | T.Async res_typ ->
-             let cc' = Value.message_cc (cc.Value.n_args + 1) in
-             let res_typ = t_typ res_typ in
-             let pat = t_pat pat in
-             let reply_typ = replyT nary res_typ in
-             let typ' = T.Tup []  in
-             let k = fresh_id reply_typ in
-             let pat',d = extendTupP pat (varP k) in
-             let typbinds' = t_typ_binds typbinds in
-             let x = fresh_id res_typ in
-             let exp' =
-               match exp.it with
-               | CallE(_, async,_,cps) ->
-                 begin
-                   match async.it with
-                   | PrimE("@async") ->
-                     blockE
-                          (d [expD ((t_exp cps) -*- (x --> (k -*- x)))])
-                     | _ -> assert false
-                 end
-               | _ -> assert false
-             in
-             FuncD (cc', id, typbinds', pat', typ', exp')
-           | _ -> assert false
-         end
-    end
-
-and t_decs decs = List.map t_dec decs
-
-and t_fields fields =
-  List.map (fun (field:exp_field) ->
-      { field with it = { field.it with exp = t_exp field.it.exp } })
-    fields
-
-and t_pat pat =
-  { pat with
-    it = t_pat' pat.it;
-    note = t_typ pat.note }
-
-and t_pat' pat =
-  match pat with
-  | WildP
-  | LitP _
-  | VarP _ ->
-    pat
-  | TupP pats ->
-    TupP (List.map t_pat pats)
-  | OptP pat1 ->
-    OptP (t_pat pat1)
-  | AltP (pat1, pat2) ->
-    AltP (t_pat pat1, t_pat pat2)
-
-and t_typ_bind' {con; bound} =
-  {con; bound = t_typ bound}
-
-and t_typ_bind typ_bind =
-  { typ_bind with it = t_typ_bind' typ_bind.it }
-
-and t_typ_binds typbinds = List.map t_typ_bind typbinds
-
-and t_prog (prog, flavor) =  (t_decs prog, { flavor with has_async_typ = false } )
-
-let transform prog = t_prog prog
+            | T.Async res_typ ->
+              let cc' = Value.message_cc (cc.Value.n_args + 1) in
+              let res_typ = t_typ res_typ in
+              let pat = t_pat pat in
+              let reply_typ = replyT nary res_typ in
+              let typ' = T.Tup []  in
+              let k = fresh_id reply_typ in
+              let pat',d = extendTupP pat (varP k) in
+              let typbinds' = t_typ_binds typbinds in
+              let x = fresh_id res_typ in
+              let exp' =
+                match exp.it with
+                | CallE(_, async,_,cps) ->
+                  begin
+                    match async.it with
+                    | PrimE("@async") ->
+                      blockE
+                        (d [expD ((t_exp cps) -*- (x --> (k -*- x)))])
+                    | _ -> assert false
+                  end
+                | _ -> assert false
+              in
+              FuncD (cc', id, typbinds', pat', typ', exp')
+            | _ -> assert false
+          end
+      end
+
+  and t_decs decs = List.map t_dec decs
+
+  and t_fields fields =
+    List.map (fun (field:exp_field) ->
+        { field with it = { field.it with exp = t_exp field.it.exp } })
+      fields
+
+  and t_pat pat =
+    { pat with
+      it = t_pat' pat.it;
+      note = t_typ pat.note }
+
+  and t_pat' pat =
+    match pat with
+    | WildP
+      | LitP _
+      | VarP _ ->
+      pat
+    | TupP pats ->
+      TupP (List.map t_pat pats)
+    | OptP pat1 ->
+      OptP (t_pat pat1)
+    | AltP (pat1, pat2) ->
+      AltP (t_pat pat1, t_pat pat2)
+
+  and t_typ_bind' {con; bound} =
+    {con = t_con con; bound = t_typ bound}
+
+  and t_typ_bind typ_bind =
+    { typ_bind with it = t_typ_bind' typ_bind.it }
+
+  and t_typ_binds typbinds = List.map t_typ_bind typbinds
+
+  and t_prog (prog, flavor) =  (t_decs prog, { flavor with has_async_typ = false } )
+
+end
+
+let transform prog =
+  let module T = Transform()
+  in T.t_prog prog
diff --git a/src/awaitopt.ml b/src/awaitopt.ml
index 04d7633a321..5074f31cb9d 100644
--- a/src/awaitopt.ml
+++ b/src/awaitopt.ml
@@ -564,3 +564,4 @@ and t_prog (prog, flavor) = (t_decs LabelEnv.empty prog, { flavor with has_await
 
 let transform prog = t_prog prog
 
+
diff --git a/src/check_ir.ml b/src/check_ir.ml
index 2e0b680a49d..7f32b1d7e83 100644
--- a/src/check_ir.ml
+++ b/src/check_ir.ml
@@ -25,7 +25,7 @@ let immute_typ p =
 (* Scope *)
 
 type val_env = T.typ T.Env.t
-type con_env = T.con_env
+type con_env = T.ConSet.t
 
 type scope =
   { val_env : val_env;
@@ -34,7 +34,7 @@ type scope =
 
 let empty_scope : scope =
   { val_env = T.Env.empty;
-    con_env = Con.Env.empty
+    con_env = T.ConSet.empty
   }
 
 (* Contexts (internal) *)
@@ -60,6 +60,7 @@ let env_of_scope scope flavor : env =
     async = false;
   }
 
+
 (* More error bookkeeping *)
 
 exception CheckFailed of string
@@ -73,21 +74,23 @@ let error env at fmt =
 let add_lab c x t = {c with labs = T.Env.add x t c.labs}
 let add_val c x t = {c with vals = T.Env.add x t c.vals}
 
-let add_typs c cs ks =
+let add_typs c cs =
   { c with
-    cons = List.fold_right2 Con.Env.add cs ks c.cons;
+    cons = List.fold_right (fun c -> T.ConSet.disjoint_add c) cs c.cons;
   }
 
 let adjoin c scope =
   { c with
     vals = T.Env.adjoin c.vals scope.val_env;
-    cons = Con.Env.adjoin 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_typs c ce =
+
+
+let adjoin_cons c ce =
   { c with
-    cons = Con.Env.adjoin c.cons ce;
+    cons = T.ConSet.disjoint_union c.cons ce;
   }
 
 let disjoint_union env at fmt env1 env2 =
@@ -110,10 +113,10 @@ let check env at p =
   else error env at
 
 let check_sub env at t1 t2 =
-  if T.sub env.cons t1 t2
+  if T.sub t1 t2
   then ()
   else error env at "subtype violation:\n  %s\n  %s\n"
-    (T.string_of_typ_expand env.cons t1) (T.string_of_typ_expand env.cons t2)
+    (T.string_of_typ_expand t1) (T.string_of_typ_expand t2)
 
 let make_mut mut : T.typ -> T.typ =
   match mut.it with
@@ -126,11 +129,11 @@ let rec check_typ env typ : unit =
     error env no_region "illegal T.Pre type"
   | T.Var (s,i) ->
     error env no_region "free type variable %s, index %i" s  i
-  | T.Con(c,typs) ->
-    (match Con.Env.find_opt c env.cons with
-    | Some (T.Def (tbs, t) | T.Abs (tbs, t))  ->
+  | T.Con (c,typs) ->
+    if not (T.ConSet.mem c env.cons) then
+       error env no_region "free type constructor %s" (Con.name c);
+    (match T.kind c with | T.Def (tbs, t) | T.Abs (tbs, t)  ->
       check_typ_bounds env tbs typs no_region
-    | None -> error env no_region "unbound type constructor %s" (Con.to_string c)
     )
   | T.Any -> ()
   | T.Non -> ()
@@ -142,7 +145,7 @@ let rec check_typ env typ : unit =
     List.iter (check_typ env) typs
   | T.Func (sort, control, binds, ts1, ts2) ->
     let cs, ce = check_typ_binds env binds in
-    let env' = adjoin_typs env  ce in
+    let env' = adjoin_cons env  ce in
     let ts = List.map (fun c -> T.Con(c,[])) cs in
     let ts1 = List.map (T.open_ ts) ts1 in
     let ts2 = List.map (T.open_ ts) ts2 in
@@ -154,7 +157,7 @@ let rec check_typ env typ : unit =
       | _ ->
         let t2 = T.seq ts2 in
         error env no_region "promising function with non-async result type \n  %s"
-          (T.string_of_typ_expand env'.cons t2)
+          (T.string_of_typ_expand t2)
     end;
     if sort = T.Sharable then begin
       let t1 = T.seq ts1 in
@@ -164,13 +167,13 @@ let rec check_typ env typ : unit =
       | [T.Async t2] ->
         check_sub env' no_region t2 T.Shared;
       | _ -> error env no_region "shared function has non-async result type\n  %s"
-          (T.string_of_typ_expand env'.cons (T.seq ts2))
+          (T.string_of_typ_expand (T.seq ts2))
     end
   | T.Opt typ ->
     check_typ env typ
   | T.Async typ ->
     check env no_region env.flavor.Ir.has_async_typ "async in non-async flavor";
-    let t' = T.promote env.cons typ in
+    let t' = T.promote typ in
     check_sub env no_region t' T.Shared
   | T.Obj (sort, fields) ->
     let rec sorted fields =
@@ -190,31 +193,30 @@ and check_typ_field env s typ_field : unit =
   let {T.name; T.typ} = typ_field in
   check_typ env typ;
   check env no_region
-     (s <> T.Actor || T.is_func (T.promote env.cons typ))
+     (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 env.cons typ T.Shared)
+     (s = T.Object T.Local || T.sub typ T.Shared)
     "shared object or actor field has non-shared type"
 
 
 and check_typ_binds env typ_binds : T.con list * con_env =
-  let ts,ce = Type.open_binds env.cons typ_binds in
+  let ts = Type.open_binds typ_binds in
   let cs = List.map (function T.Con(c,[]) ->  c | _ -> assert false) ts in
-  let ks = List.map2 (fun c t -> T.Abs ([], t)) cs ts in
-  let env' = add_typs env cs ks in
+  let env' = add_typs env cs in
   let _ = List.map
             (fun typ_bind ->
               let bd = T.open_ ts typ_bind.T.bound  in
               check_typ env' bd)
             typ_binds
   in
-  cs, Con.Env.from_list2 cs ks
+  cs, T.ConSet.of_list cs
 
 and check_typ_bounds env (tbs : T.bind list) typs at : unit =
   match tbs, typs with
   | tb::tbs', typ::typs' ->
     check_typ env typ;
-    check env at (T.sub env.cons typ tb.T.bound)
+    check env at (T.sub typ tb.T.bound)
       "type argument does not match parameter bound";
     check_typ_bounds env tbs' typs' at
   | [], [] -> ()
@@ -305,21 +307,21 @@ let rec check_exp env (exp:Ir.exp) : unit =
   | ProjE (exp1, n) ->
     begin
     check_exp env exp1;
-    let t1 = T.promote env.cons (immute_typ exp1) in
-    let ts = try T.as_tup_sub n env.cons t1
+    let t1 = T.promote (immute_typ exp1) in
+    let ts = try T.as_tup_sub n t1
              with Invalid_argument _ ->
                error env exp1.at "expected tuple type, but expression produces type\n  %s"
-                 (T.string_of_typ_expand env.cons t1) in
+                 (T.string_of_typ_expand t1) in
     let tn = try List.nth ts n with
              | Invalid_argument _ ->
                error env exp.at "tuple projection %n is out of bounds for type\n  %s"
-                 n (T.string_of_typ_expand env.cons t1) in
+                 n (T.string_of_typ_expand t1) in
     tn <: t
     end
   | ActorE ( id, fields, t0) ->
     let env' = { env with async = false } in
     let t1 =  type_obj env' T.Actor id t fields in
-    let t2 = T.promote env.cons t in
+    let t2 = T.promote t in
     check (T.is_obj t2) "bad annotation (object type expected)";
     t1 <: t2;
     t0 <: t;
@@ -329,10 +331,10 @@ let rec check_exp env (exp:Ir.exp) : unit =
       check_exp env exp1;
       let t1 = typ exp1 in
       let sort, tfs =
-        try T.as_obj_sub n env.cons t1 with
+        try T.as_obj_sub n t1 with
         | Invalid_argument _ ->
           error env exp1.at "expected object type, but expression produces type\n  %s"
-            (T.string_of_typ_expand env.cons t1)
+            (T.string_of_typ_expand t1)
       in
       check (match exp.it with
              | ActorDotE _ -> sort = T.Actor
@@ -343,7 +345,7 @@ let rec check_exp env (exp:Ir.exp) : unit =
         tn <~ t
       | None ->
         error env exp1.at "field name %s does not exist in type\n  %s"
-          n (T.string_of_typ_expand env.cons t1)
+          n (T.string_of_typ_expand t1)
     end
   | AssignE (exp1, exp2) ->
     check_exp env exp1;
@@ -361,11 +363,11 @@ let rec check_exp env (exp:Ir.exp) : unit =
   | IdxE (exp1, exp2) ->
     check_exp env exp1;
     check_exp env exp2;
-    let t1 = T.promote env.cons (typ exp1) in
-    let t2 = try T.as_array_sub env.cons t1 with
+    let t1 = T.promote (typ exp1) in
+    let t2 = try T.as_array_sub t1 with
              | Invalid_argument _ ->
                error env exp1.at "expected array type, but expression produces type\n  %s"
-                                       (T.string_of_typ_expand env.cons t1)
+                                       (T.string_of_typ_expand t1)
     in
     typ exp2 <: T.nat;
     t2 <~ t
@@ -373,12 +375,12 @@ let rec check_exp env (exp:Ir.exp) : unit =
     check_exp env exp1;
     check_exp env exp2;
     (* TODO: check call_conv (assuming there's something to check) *)
-    let t1 = T.promote env.cons (typ exp1) in
+    let t1 = T.promote (typ exp1) in
     let tbs, t2, t3 =
-      try T.as_func_sub (List.length insts) env.cons t1 with
+      try T.as_func_sub (List.length insts) t1 with
       |  Invalid_argument _ ->
          error env exp1.at "expected function type, but expression produces type\n  %s"
-           (T.string_of_typ_expand env.cons t1)
+           (T.string_of_typ_expand t1)
     in
     check_inst_bounds env tbs insts exp.at;
     check_exp env exp2;
@@ -386,9 +388,8 @@ let rec check_exp env (exp:Ir.exp) : unit =
     T.open_ insts t3 <: t;
   | BlockE (decs, t0) ->
     let t1, scope = type_block env decs exp.at in
-    let env' = adjoin env scope in
     check_typ env t0;
-    check (T.eq env.cons t T.unit || T.eq env'.cons t1 t0) "unexpected expected block type";
+    check (T.eq t T.unit || T.eq t1 t0) "unexpected expected block type";
     t0 <: t;
   | IfE (exp1, exp2, exp3) ->
     check_exp env exp1;
@@ -399,7 +400,7 @@ let rec check_exp env (exp:Ir.exp) : unit =
     typ exp3 <: t;
   | SwitchE (exp1, cases) ->
     check_exp env exp1;
-    let t1 = T.promote env.cons (typ exp1) in
+    let t1 = T.promote (typ exp1) in
 (*    if not env.pre then
       if not (Coverage.check_cases env.cons cases t1) then
         warn env exp.at "the cases in this switch do not cover all possible values";
@@ -424,13 +425,13 @@ let rec check_exp env (exp:Ir.exp) : unit =
   | ForE (pat, exp1, exp2) ->
     begin
       check_exp env exp1;
-      let t1 = T.promote env.cons (typ exp1) in
+      let t1 = T.promote (typ exp1) in
       try
-        let _, tfs = T.as_obj_sub "next" env.cons t1 in
+        let _, tfs = T.as_obj_sub "next" t1 in
         let t0 = T.lookup_field "next" tfs in
-        let t1, t2 = T.as_mono_func_sub env.cons t0 in
+        let t1, t2 = T.as_mono_func_sub t0 in
         T.unit <: t1;
-        let t2' = T.as_opt_sub env.cons t2 in
+        let t2' = T.as_opt_sub t2 in
         let ve = check_pat_exhaustive env pat in
         pat.note <: t2';
         check_exp (adjoin_vals env ve) exp2;
@@ -438,7 +439,7 @@ let rec check_exp env (exp:Ir.exp) : unit =
         T.unit <: t
       with Invalid_argument _ ->
         error env exp1.at "expected iterable type, but expression has type\n  %s"
-          (T.string_of_typ_expand env.cons t1)
+          (T.string_of_typ_expand t1)
     end;
   | LabelE (id, t0, exp1) ->
     assert (t0 <> T.Pre);
@@ -479,11 +480,11 @@ let rec check_exp env (exp:Ir.exp) : unit =
     check env.flavor.has_await "await in non-await flavor";
     check env.async "misplaced await";
     check_exp env exp1;
-    let t1 = T.promote env.cons (typ exp1) in
-    let t2 = try T.as_async_sub env.cons t1
+    let t1 = T.promote (typ exp1) in
+    let t2 = try T.as_async_sub t1
              with Invalid_argument _ ->
                error env exp1.at "expected async type, but expression has type\n  %s"
-                 (T.string_of_typ_expand env.cons t1)
+                 (T.string_of_typ_expand t1)
     in
     t2 <: t;
   | AssertE exp1 ->
@@ -519,7 +520,7 @@ let rec check_exp env (exp:Ir.exp) : unit =
                                            {T.name = Syntax.string_of_name name.it;
                                             T.typ = T.Env.find id.it env.vals}) labids))
     in
-    let t2 = T.promote env.cons t in
+    let t2 = T.promote t in
     check (T.is_obj t2) "bad annotation (object type expected)";
     t1 <: t2;
     t0 <: t;
@@ -533,7 +534,7 @@ and check_case env t_pat t {it = {pat; exp}; _} =
   let ve = check_pat env pat in
   check_sub env pat.at pat.note t_pat;
   check_exp (adjoin_vals env ve) exp;
-  if not (T.sub env.cons (typ exp)  t) then
+  if not (T.sub (typ exp)  t) then
     error env exp.at "bad case"
 
 (* Patterns *)
@@ -648,7 +649,7 @@ and type_exp_field env s (tfs, ve) field : T.field list * val_env =
     "public actor field is not a function";
   check env field.at
     (if (s <> T.Object T.Local && priv.it = Syntax.Public)
-     then T.sub env.cons t T.Shared
+     then T.sub t T.Shared
      else true)
     "public shared object or actor field has non-shared type";
   let ve' = T.Env.add id.it t ve in
@@ -678,8 +679,7 @@ and type_block_exps env decs : T.typ =
 
 and check_open_typ_binds env typ_binds =
   let cs = List.map (fun tp -> tp.it.con) typ_binds in
-  let ks = List.map (fun tp -> T.Abs([],tp.it.bound)) typ_binds in
-  let ce = List.fold_right2 Con.Env.add cs ks Con.Env.empty in
+  let ce = List.fold_right (fun c ce -> T.ConSet.disjoint_add c ce) cs T.ConSet.empty in
   let binds = close_typ_binds cs (List.map (fun tb -> tb.it) typ_binds) in
   let _,_ = check_typ_binds env binds in
   cs,ce
@@ -706,7 +706,7 @@ and check_dec env dec  =
   | FuncD (cc, id, typ_binds, pat, t2, exp) ->
     let t0 = T.Env.find id.it env.vals in
     let _cs,ce = check_open_typ_binds env typ_binds in
-    let env' = adjoin_typs env ce in
+    let env' = adjoin_cons env ce in
     let ve = check_pat_exhaustive env' pat in
     check_typ env' t2;
     check ((cc.Value.sort = T.Sharable && Type.is_async t2)
@@ -717,15 +717,16 @@ and check_dec env dec  =
     check_exp (adjoin_vals env'' ve) exp;
     check_sub env' dec.at (typ exp) t2;
     t0 <: t;
-  | TypD (c, k) ->
+  | TypD c ->
+    check (T.ConSet.mem c env.cons) "free type constructor";
     let (binds,typ) =
-      match k with
+      match T.kind c with
       | T.Abs(binds,typ)
       | T.Def(binds,typ) -> (binds,typ)
     in
-    let cs,ce = check_typ_binds env binds in
+    let cs, ce = check_typ_binds env binds in
     let ts = List.map (fun c -> T.Con(c,[])) cs in
-    let env' = adjoin_typs env ce in
+    let env' = adjoin_cons env ce in
     check_typ env' (T.open_ ts  typ);
     T.unit <: t;
 
@@ -740,7 +741,7 @@ and check_block_exps env t decs at =
     check_sub env at T.unit t
   | [dec] ->
     check_dec env dec;
-    check env at (T.is_unit t || T.sub env.cons (typ dec) t)
+    check env at (T.is_unit t || T.sub (typ dec) t)
       "declaration does not produce expect type"
   | dec::decs' ->
     check_dec env dec;
@@ -783,13 +784,13 @@ and gather_dec env scope dec : scope =
     let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = T.close cs t}) cs ts in
     let t = T.Func (func_sort, c, tbs, List.map (T.close cs) ts1, List.map (T.close cs) ts2) in
     let ve' =  T.Env.add id.it t scope.val_env in
-    {scope with val_env = ve'}
-  | TypD (c, k) ->
+    { scope with val_env = ve' }
+  | TypD c ->
     check env dec.at
-      (not (Con.Env.mem c scope.con_env))
+      (not (T.ConSet.mem c scope.con_env))
       "duplicate definition of type in block";
-    let ce' = Con.Env.add c k scope.con_env in
-    {scope with con_env = ce'}
+    let ce' = T.ConSet.disjoint_add c scope.con_env in
+    { scope with con_env = ce' }
 
 (* Programs *)
 
diff --git a/src/check_ir.mli b/src/check_ir.mli
index 36bb7ec6b2f..9203122e85a 100644
--- a/src/check_ir.mli
+++ b/src/check_ir.mli
@@ -1 +1,2 @@
 val check_prog : Typing.scope -> Ir.prog -> unit
+
diff --git a/src/compile.ml b/src/compile.ml
index 414203325bd..fdce65f21f1 100644
--- a/src/compile.ml
+++ b/src/compile.ml
@@ -157,7 +157,6 @@ module E = struct
 
     (* Immutable *)
     local_vars_env : t varloc NameEnv.t; (* variables ↦ their location *)
-    con_env : Type.con_env;
 
     (* Mutable *)
     func_types : func_type list ref;
@@ -190,7 +189,6 @@ module E = struct
     mode;
     prelude;
     local_vars_env = NameEnv.empty;
-    con_env = Con.Env.empty;
     func_types = ref [];
     func_imports = ref [];
     other_imports = ref [];
@@ -233,21 +231,6 @@ module E = struct
 
   let mode (env : t) = env.mode
 
-  let con_env (env : t) = env.con_env
-
-  let add_con (env : t) c k =
-    { env with con_env = Con.Env.add c k env.con_env }
-
-  let add_typ_binds (env : t) typ_binds =
-    (* There is some code duplication with Check_ir.check_open_typ_binds.
-       This shoulds be extracte into Type.add_open_typ_binds
-       and maybe we need a type open_typ_bind that can be used inside the IR.
-    *)
-    let cs = List.map (fun tp -> tp.it.con) typ_binds in
-    let ks = List.map (fun tp -> Type.Abs([],tp.it.bound)) typ_binds in
-    let ce = List.fold_right2 Con.Env.add cs ks Con.Env.empty in
-    { env with con_env = Con.Env.adjoin env.con_env ce }
-
   let lookup_var env var =
     match NameEnv.find_opt var env.local_vars_env with
       | Some l -> Some l
@@ -1336,7 +1319,7 @@ module Object = struct
 
   (* Determines whether the field is mutable (and thus needs an indirection) *)
   let is_mut_field env obj_type ({it = Syntax.Name s; _}) =
-    let _, fields = Type.as_obj_sub "" (E.con_env env) obj_type in
+    let _, fields = Type.as_obj_sub "" obj_type in
     let field_typ = Type.lookup_field s fields in
     let mut = Type.is_mut field_typ in
     mut
@@ -3775,9 +3758,8 @@ and compile_dec pre_env how dec : E.t * G.t * (E.t -> (SR.t * G.t)) =
        (pre_env, G.with_region dec.at alloc_code, fun env ->
          (fun (sr, code) -> (sr, G.with_region dec.at code)) (mk_code env))) @@
   match dec.it with
-  | TypD (c,k) ->
-    let pre_env1 = E.add_con pre_env c k in
-    (pre_env1, G.nop, fun _ -> SR.unit, G.nop)
+  | TypD _ ->
+    (pre_env, G.nop, fun _ -> SR.unit, G.nop)
   | ExpD e ->(pre_env, G.nop, fun env -> compile_exp env e)
 
   (* A special case for static expressions *)
@@ -3811,9 +3793,8 @@ and compile_dec pre_env how dec : E.t * G.t * (E.t -> (SR.t * G.t)) =
       let (pre_env1, alloc_code, mk_code) = FuncDec.dec pre_env how name cc captured mk_pat mk_body dec.at in
       (pre_env1, alloc_code, fun env ->
         (* Bring type parameters into scope *)
-        let env1 = E.add_typ_binds env typ_binds in
-        let sr, code = Var.get_val env1 name.it in
-        sr, mk_code env1 ^^ code
+        let sr, code = Var.get_val env name.it in
+        sr, mk_code env ^^ code
       )
 
 and compile_decs env decs : SR.t * G.t =
diff --git a/src/con.ml b/src/con.ml
index 7bc633d0756..9b6a5df2a8a 100644
--- a/src/con.ml
+++ b/src/con.ml
@@ -1,23 +1,27 @@
-type con = {name : string; stamp : int}
-type t = con
+type 'a con = {name : string; stamp : int; kind : 'a}
+type 'a t = 'a con
 
 module Stamps = Env.Make(String)
 
 let stamps : int Stamps.t ref = ref Stamps.empty
 
-let fresh name =
+let fresh name kind =
   let n =
     match Stamps.find_opt name !stamps with
     | Some n -> n
     | None -> 0
   in
   stamps := Stamps.add name (n + 1) !stamps;
-  {name; stamp = n}
+  {name; stamp = n; kind}
 
 let name c = c.name
 
+let kind c = c.kind
+
 let to_string c =
   if c.stamp = 0 then c.name else Printf.sprintf "%s/%i" c.name c.stamp
 
+let compare c1 c2 = compare (c1.name, c1.stamp) (c2.name, c2.stamp)
+let eq c1 c2 = (c1.name, c1.stamp) = (c2.name, c2.stamp)
 
-module Env = Env.Make(struct type t = con let compare = compare end)
+let clone c k = { c with kind = k }
diff --git a/src/con.mli b/src/con.mli
index 9f2718a530b..36a7eb0342e 100644
--- a/src/con.mli
+++ b/src/con.mli
@@ -1,9 +1,11 @@
 (* Generative constructors *)
 
-type t
+type 'a t
 
-val fresh : string -> t
-val name : t -> string
-val to_string : t -> string
-
-module Env : Env.S with type key = t
+val fresh : string -> 'a -> 'a t
+val kind : 'a t -> 'a
+val name : 'a t -> string
+val to_string : 'a t -> string
+val eq : 'a t -> 'a t -> bool
+val compare : 'a t -> 'a t -> int
+val clone: 'a t -> 'a -> 'a t
diff --git a/src/coverage.ml b/src/coverage.ml
index 16d2a2ff54a..3a278091253 100644
--- a/src/coverage.ml
+++ b/src/coverage.ml
@@ -55,92 +55,92 @@ let skip_pat pat sets =
   sets.alts <- AtSet.add pat.at sets.alts;
   true
 
-let rec match_pat ce ctxt desc pat t sets =
-  Type.span ce t = Some 0 && skip_pat pat sets ||
+let rec match_pat ctxt desc pat t sets =
+  Type.span t = Some 0 && skip_pat pat sets ||
   match pat.it with
   | WildP | VarP _ ->
-    succeed ce ctxt desc sets
+    succeed ctxt desc sets
   | LitP lit ->
-    match_lit ce ctxt desc (value_of_lit !lit) t sets
+    match_lit ctxt desc (value_of_lit !lit) t sets
   | SignP (op, lit) ->
     let f = Operator.unop pat.note op in
-    match_lit ce ctxt desc (f (value_of_lit !lit)) t sets
+    match_lit ctxt desc (f (value_of_lit !lit)) t sets
   | TupP pats ->
-    let ts = Type.as_tup (Type.promote ce t) in
+    let ts = Type.as_tup (Type.promote t) in
     let descs =
       match desc with
       | Tup descs -> descs
       | Any -> List.map (fun _ -> Any) pats
       | _ -> assert false
-    in match_tup ce ctxt [] descs pats ts sets
+    in match_tup ctxt [] descs pats ts sets
 	| OptP pat1 ->
-    let t' = Type.as_opt (Type.promote ce t) in
+    let t' = Type.as_opt (Type.promote t) in
     (match desc with
     | Val Value.Null ->
-      fail ce ctxt desc sets
+      fail ctxt desc sets
     | NotVal vs when ValSet.mem Value.Null vs ->
-      match_pat ce (InOpt ctxt) Any pat1 t' sets
+      match_pat (InOpt ctxt) Any pat1 t' sets
     | Opt desc' ->
-      match_pat ce (InOpt ctxt) desc' pat1 t' sets
+      match_pat (InOpt ctxt) desc' pat1 t' sets
     | Any ->
-      fail ce ctxt (Val Value.Null) sets &&
-      match_pat ce (InOpt ctxt) Any pat1 t' sets
+      fail ctxt (Val Value.Null) sets &&
+      match_pat (InOpt ctxt) Any pat1 t' sets
     | _ -> assert false
     )
   | AltP (pat1, pat2) ->
     sets.alts <- AtSet.add pat1.at (AtSet.add pat2.at sets.alts);
-    match_pat ce (InAlt1 (ctxt, pat1.at, pat2, t)) desc pat1 t sets
+    match_pat (InAlt1 (ctxt, pat1.at, pat2, t)) desc pat1 t sets
   | AnnotP (pat1, _) ->
-    match_pat ce ctxt desc pat1 t sets
+    match_pat ctxt desc pat1 t sets
 
-and match_lit ce ctxt desc v t sets =
+and match_lit ctxt desc v t sets =
   let desc_succ = Val v in
   let desc_fail vs = NotVal (ValSet.add v vs) in
   match desc with
   | Any ->
-    if Type.span ce t = Some 1 then
-      succeed ce ctxt desc_succ sets
+    if Type.span t = Some 1 then
+      succeed ctxt desc_succ sets
     else
-      succeed ce ctxt desc_succ sets &&
-      fail ce ctxt (desc_fail ValSet.empty) sets
+      succeed ctxt desc_succ sets &&
+      fail ctxt (desc_fail ValSet.empty) sets
   | Val v' ->
     if Value.equal v v'
-    then succeed ce ctxt desc sets
-    else fail ce ctxt desc sets
+    then succeed ctxt desc sets
+    else fail ctxt desc sets
   | NotVal vs ->
     if ValSet.mem v vs then
-      fail ce ctxt desc sets
-    else if Type.span ce t = Some (ValSet.cardinal vs + 1) then
-      succeed ce ctxt desc_succ sets
+      fail ctxt desc sets
+    else if Type.span t = Some (ValSet.cardinal vs + 1) then
+      succeed ctxt desc_succ sets
     else
-      succeed ce ctxt desc_succ sets && fail ce ctxt (desc_fail vs) sets
+      succeed ctxt desc_succ sets && fail ctxt (desc_fail vs) sets
   | Opt _ ->
-    fail ce ctxt desc sets
+    fail ctxt desc sets
   | _ ->
     assert false
 
-and match_tup ce ctxt descs_r descs pats ts sets =
+and match_tup ctxt descs_r descs pats ts sets =
   match descs, pats, ts with
   | [], [], [] ->
-    succeed ce ctxt (Tup (List.rev descs_r)) sets
+    succeed ctxt (Tup (List.rev descs_r)) sets
   | desc::descs', pat::pats', t::ts' ->
-    match_pat ce (InTup (ctxt, descs_r, descs', pats', ts')) desc pat t sets
+    match_pat (InTup (ctxt, descs_r, descs', pats', ts')) desc pat t sets
   | _ ->
     assert false
     
 
-and succeed ce ctxt desc sets : bool =
+and succeed ctxt desc sets : bool =
   match ctxt with
   | InOpt ctxt' ->
-    succeed ce ctxt' (Opt desc) sets
+    succeed ctxt' (Opt desc) sets
   | InTup (ctxt', descs_r, descs, pats, ts) ->
-    match_tup ce ctxt' (desc::descs_r) descs pats ts sets
+    match_tup ctxt' (desc::descs_r) descs pats ts sets
   | InAlt1 (ctxt', at1, _pat2, _t) ->
     sets.reached_alts <- AtSet.add at1 sets.reached_alts;
-    succeed ce ctxt' desc sets
+    succeed ctxt' desc sets
   | InAlt2 (ctxt', at2) ->
     sets.reached_alts <- AtSet.add at2 sets.reached_alts;
-    succeed ce ctxt' desc sets
+    succeed ctxt' desc sets
   | InCase (at, cases, _t) ->
     sets.reached_cases <- AtSet.add at sets.reached_cases;
     skip cases sets
@@ -153,21 +153,21 @@ and skip cases sets : bool =
     sets.cases <- AtSet.add case.at sets.cases;
     skip cases' sets
 
-and fail ce ctxt desc sets : bool =
+and fail ctxt desc sets : bool =
   match ctxt with
   | InOpt ctxt' ->
-    fail ce ctxt' (Opt desc) sets
+    fail ctxt' (Opt desc) sets
   | InTup (ctxt', descs', descs, pats, _ts) ->
-    fail ce ctxt' (Tup (List.rev descs' @ [desc] @ descs)) sets
+    fail ctxt' (Tup (List.rev descs' @ [desc] @ descs)) sets
   | InAlt1 (ctxt', at1, pat2, t) ->
-    match_pat ce (InAlt2 (ctxt', pat2.at)) desc pat2 t sets
+    match_pat (InAlt2 (ctxt', pat2.at)) desc pat2 t sets
   | InAlt2 (ctxt', at2) ->
-    fail ce ctxt' desc sets
+    fail ctxt' desc sets
   | InCase (at, [], t) ->
-    Type.span ce t = Some 0
+    Type.span t = Some 0
   | InCase (at, case::cases, t) ->
-    Type.span ce t = Some 0 && skip (case::cases) sets ||
-    match_pat ce (InCase (case.at, cases, t)) desc case.it.pat t sets
+    Type.span t = Some 0 && skip (case::cases) sets ||
+    match_pat (InCase (case.at, cases, t)) desc case.it.pat t sets
 
 
 let warn at fmt =
@@ -176,9 +176,9 @@ let warn at fmt =
       Printf.eprintf "%s: warning, %s\n%!" (Source.string_of_region at) s;
   ) fmt
 
-let check_cases ce cases t : bool =
+let check_cases cases t : bool =
 	let sets = make_sets () in
-  let exhaustive = fail ce (InCase (Source.no_region, cases, t)) Any sets in
+  let exhaustive = fail (InCase (Source.no_region, cases, t)) Any sets in
   let unreached_cases = AtSet.diff sets.cases sets.reached_cases in
   let unreached_alts = AtSet.diff sets.alts sets.reached_alts in
   AtSet.iter (fun at -> warn at "this case is never reached") unreached_cases;
@@ -188,6 +188,5 @@ let check_cases ce cases t : bool =
 
 let (@?) it at = {it; at; note = empty_typ_note}
 
-let check_pat ce pat t : bool =
-	check_cases ce
-	  [{pat; exp = TupE [] @? Source.no_region} @@ Source.no_region] t
+let check_pat pat t : bool =
+  check_cases [{pat; exp = TupE [] @? Source.no_region} @@ Source.no_region] t
diff --git a/src/coverage.mli b/src/coverage.mli
index 60862fb0b49..b0833624403 100644
--- a/src/coverage.mli
+++ b/src/coverage.mli
@@ -1,2 +1,2 @@
-val check_pat : Type.con_env -> Syntax.pat -> Type.typ -> bool
-val check_cases : Type.con_env -> Syntax.case list -> Type.typ -> bool
+val check_pat : Syntax.pat -> Type.typ -> bool
+val check_cases : Syntax.case list -> Type.typ -> bool
diff --git a/src/desugar.ml b/src/desugar.ml
index 7d8af75942f..03dbefc6332 100644
--- a/src/desugar.ml
+++ b/src/desugar.ml
@@ -144,8 +144,8 @@ and decs ds =
   | d::ds ->
     match d.it with
     | S.ClassD(_, con_id, _, _, _, _, _) ->
-      let (c,k) = match con_id.note with Some p -> p | _ -> assert false in
-      let typD = { it = I.TypD (c,k);
+      let c = Lib.Option.value con_id.note in
+      let typD = { it = I.TypD c;
                    at = d.at;
                    note = { S.note_typ = T.unit;
                             S.note_eff = T.Triv }
@@ -162,8 +162,8 @@ and dec' at n d = match d with
     let cc = Value.call_conv_of_typ n.S.note_typ in
     I.FuncD (cc, i, typ_binds tbs, pat p, ty.note, exp e)
   | S.TypD (con_id, typ_bind, t) ->
-    let (c,k) = Lib.Option.value con_id.note in
-    I.TypD (c,k)
+    let c = Lib.Option.value con_id.note in
+    I.TypD c
   | S.ClassD (fun_id, typ_id, tbs, s, p, self_id, es) ->
     let cc = Value.call_conv_of_typ n.S.note_typ in
     let inst = List.map
diff --git a/src/effect.ml b/src/effect.ml
index eec17c93a2a..deeae6e46a1 100644
--- a/src/effect.ml
+++ b/src/effect.ml
@@ -196,7 +196,7 @@ module Ir =
       | LetD (_,e)
       | VarD (_, e) ->
         effect_exp e
-      | TypD (c,k) ->
+      | TypD _ ->
         T.Triv
       | FuncD (s, v, tps, p, t, e) ->
         T.Triv
diff --git a/src/env.ml b/src/env.ml
index 1749cb55b64..7450a8a0a0b 100644
--- a/src/env.ml
+++ b/src/env.ml
@@ -26,5 +26,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/freevars.ml b/src/freevars.ml
index a12db427ecc..6ae4438b1b2 100644
--- a/src/freevars.ml
+++ b/src/freevars.ml
@@ -122,7 +122,7 @@ and dec d = match d.it with
     (M.empty, S.singleton i.it) +++ exp e
   | FuncD (cc, i, tp, p, t, e) ->
     (M.empty, S.singleton i.it) +++ under_lambda (exp e /// pat p)
-  | TypD (c,k) -> (M.empty, S.empty)
+  | TypD c -> (M.empty, S.empty)
 
 (* The variables captured by a function. May include the function itself! *)
 and captured p e =
diff --git a/src/ir.ml b/src/ir.ml
index e8e14f9dfcf..0561506c958 100644
--- a/src/ir.ml
+++ b/src/ir.ml
@@ -3,7 +3,7 @@ type type_note = Syntax.typ_note = {note_typ : Type.typ; note_eff : Type.eff}
 
 type 'a phrase = ('a, Syntax.typ_note) Source.annotated_phrase
 
-and typ_bind' = {con : Con.t; bound : Type.typ}
+type typ_bind' = {con : Type.con; bound : Type.typ}
 type typ_bind = typ_bind' Source.phrase
 
 type pat = (pat', Type.typ) Source.annotated_phrase
@@ -72,7 +72,7 @@ and dec' =
   | VarD of Syntax.id * exp                    (* mutable *)
   | FuncD of                                   (* function *)
       Value.call_conv * Syntax.id * typ_bind list * pat * Type.typ * exp
-  | TypD of Type.con * Type.kind               (* type *)
+  | TypD of Type.con                           (* type *)
 
 
 (* Flavor *)
diff --git a/src/pipeline.ml b/src/pipeline.ml
index 7c0d3b02657..d512bec7c3c 100644
--- a/src/pipeline.ml
+++ b/src/pipeline.ml
@@ -16,8 +16,8 @@ let error at cat text =
   Error { Diag.sev = Diag.Error; at; cat; text }
 
 let print_ce =
-  Con.Env.iter (fun c k ->
-    let eq, params, typ = Type.strings_of_kind k in
+  Type.ConSet.iter (fun c ->
+    let eq, params, typ = Type.strings_of_kind (Type.kind c) in
     printf "type %s%s %s %s\n" (Con.to_string c) params eq typ
   )
 
@@ -123,7 +123,8 @@ let transform_ir transform_name transform flag env prog name =
       phase transform_name name;
       let prog' : Ir.prog = transform prog in
       dump_ir Flags.dump_lowering prog';
-      Check_ir.check_prog env prog;
+      (* Check_ir.check_prog env prog; *)
+      Check_ir.check_prog env prog';
       prog'
     end
   else prog
diff --git a/src/rename.ml b/src/rename.ml
index 8e14eccfef0..655ddec0f9f 100644
--- a/src/rename.ml
+++ b/src/rename.ml
@@ -145,7 +145,7 @@ and dec' rho d = match d with
        let e' = exp rho'' e in
        FuncD (s, i', tp, p', t, e')),
      rho
-  | TypD (c,k) -> (* we don't rename type names *)
+  | TypD c -> (* we don't rename type names *)
      (fun rho -> d),
      rho
 
diff --git a/src/syntax.ml b/src/syntax.ml
index 01fa40b3ad1..a6060832601 100644
--- a/src/syntax.ml
+++ b/src/syntax.ml
@@ -7,7 +7,7 @@ let empty_typ_note = {note_typ = Type.Pre; note_eff = Type.Triv}
 (* Identifiers *)
 
 type id = string Source.phrase
-type con_id = (string, (Type.con * Type.kind) option) Source.annotated_phrase
+type con_id = (string, Type.con option) Source.annotated_phrase
 
 (* Names (not alpha-convertible), used for field and class names *)
 type name = name' Source.phrase
@@ -42,7 +42,7 @@ and typ' =
 and typ_field = typ_field' Source.phrase
 and typ_field' = {id : id; typ : typ; mut : mut}
 
-and typ_bind = (typ_bind', Con.t option) Source.annotated_phrase
+and typ_bind = (typ_bind', Type.con option) Source.annotated_phrase
 and typ_bind' = {var : id; bound : typ}
 
 
diff --git a/src/tailcall.ml b/src/tailcall.ml
index 6e387a8339a..eb8409c5b53 100644
--- a/src/tailcall.ml
+++ b/src/tailcall.ml
@@ -62,10 +62,10 @@ let bind env i (info:func_info option) : env =
     | _ -> env (* preserve existing, non-shadowed info *)
 
 
-let are_generic_insts tbs insts =
-  List.for_all2 (fun tb inst ->
+let are_generic_insts (tbs : typ_bind list) insts =
+  List.for_all2 (fun (tb : typ_bind) inst ->
       match inst with
-      | Con(c2,[]) -> tb.it.con = c2 (* conservative, but safe *)
+      | Con(c2,[]) -> Con.eq tb.it.con c2 (* conservative, but safe *)
       |  _ -> false
       ) tbs insts
 
@@ -210,7 +210,7 @@ and dec' env d =
       in
       let env3 = pat env2 p  in (* shadow id if necessary *)
       let exp0' = tailexp env3 exp0 in
-      let cs = List.map (fun tb -> Con (tb.it.con, [])) tbs in
+      let cs = List.map (fun (tb : typ_bind) -> Con (tb.it.con, [])) tbs in
       if !tail_called then
         let ids = match typ d with
           | Func( _, _, _, dom, _) -> List.map (fun t -> fresh_id (open_ cs t)) dom
@@ -238,7 +238,7 @@ and dec' env d =
       let e' = tailexp env2 e in
       FuncD(cc, i, tbs, p, t, e')),
     env
-  | TypD (_, _) ->
+  | TypD _ ->
     (fun env -> d.it),
     env
 
diff --git a/src/type.ml b/src/type.ml
index 4726ff5aea9..45aa5d21c06 100644
--- a/src/type.ml
+++ b/src/type.ml
@@ -1,6 +1,5 @@
 (* Representation *)
 
-type con = Con.t
 type control = Returns | Promises (* Returns a computed value or immediate promise *)
 type sharing = Local | Sharable
 type obj_sort = Object of sharing | Actor
@@ -37,18 +36,32 @@ and typ =
   | Non                                       (* bottom *)
   | Pre                                       (* pre-type *)
 
+and con_annot = kind ref (* the con annotation is abstract to the outside world *)
+and con = con_annot Con.t
+
 and bind = {var : string; bound : typ}
 and field = {name : string; typ : typ}
 
-(* field ordering *)
-
-let compare_field {name=n;_} {name=m;_} = compare n m
-
-type kind =
+and kind =
   | Def of bind list * typ
   | Abs of bind list * typ
 
-type con_env = kind Con.Env.t
+(* cons *)
+
+(* The con field is a reference to break the recursion in open_binds,
+   and to allow the multiple passes in typing *)
+let kind con = !(Con.kind con)
+
+let fresh_con n k = Con.fresh n (ref k)
+let modify_kind c f = Con.kind c := f !(Con.kind c)
+let clone_con c (k:kind)  = Con.clone c (ref k)
+let set_kind c k = match !(Con.kind c) with
+  | Abs (_, Pre) -> Con.kind c := k
+  | _ -> raise (Invalid_argument "set_kind")
+
+(* field ordering *)
+
+let compare_field f1 f2 = compare f1.name f2.name
 
 let seq ts =
     match ts with
@@ -129,20 +142,22 @@ and shift_field i n {name; typ} =
 
 (* First-order substitution *)
 
+module ConEnv = Env.Make(struct type t = con let compare = Con.compare end)
+
 let rec subst sigma t =
-  if sigma = Con.Env.empty then t else
+  if sigma = ConEnv.empty then t else
   match t with
   | Prim _
   | Var _ -> t
   | Con (c, ts) ->
-    (match Con.Env.find_opt c sigma with
+    (match ConEnv.find_opt c sigma with
     | Some t -> assert (List.length ts = 0); t
     | None -> Con (c, List.map (subst sigma) ts)
     )
   | Array t -> Array (subst sigma t)
   | Tup ts -> Tup (List.map (subst sigma) ts)
   | Func (s, c, tbs, ts1, ts2) ->
-    let sigma' = Con.Env.map (shift 0 (List.length tbs)) sigma in
+    let sigma' = ConEnv.map (shift 0 (List.length tbs)) sigma in
     Func (s, c, List.map (subst_bind sigma') tbs,
           List.map (subst sigma') ts1, List.map (subst sigma') ts2)
   | Opt t -> Opt (subst sigma t)
@@ -166,7 +181,7 @@ and subst_field sigma {name; typ} =
 let close cs t =
   if cs = [] then t else
   let ts = List.mapi (fun i c -> Var (Con.name c, i)) cs in
-  let sigma = List.fold_right2 Con.Env.add cs ts Con.Env.empty in
+  let sigma = List.fold_right2 ConEnv.add cs ts ConEnv.empty in
   subst sigma t
 
 let close_binds cs tbs =
@@ -203,12 +218,13 @@ let open_ ts t =
   if ts = [] then t else
   open' 0 ts t
 
-let open_binds env tbs =
-  if tbs = [] then [], env else
-  let cs = List.map (fun {var; _} -> Con.fresh var) tbs in
-  let ts = List.map (fun c -> Con (c, [])) cs in
+let open_binds tbs =
+  if tbs = [] then [] else
+  let cs = List.map (fun {var; _} -> fresh_con var (Abs ([], Pre))) tbs in
+  let ts = List.map (fun con -> Con (con, [])) cs in
   let ks = List.map (fun {bound; _} -> Abs ([], open_ ts bound)) tbs in
-  ts, List.fold_right2 Con.Env.add cs ks env
+  List.iter2 (fun c k -> Con.kind c := k) cs ks;
+  ts
 
 
 (* Normalization and Classification *)
@@ -217,22 +233,19 @@ let reduce tbs t ts =
   assert (List.length ts = List.length tbs);
   open_ ts t
 
-let rec normalize env = function
+let rec normalize = function
   | Con (con, ts) as t ->
-    (match Con.Env.find_opt con env with
-    | Some (Def (tbs, t)) -> normalize env (reduce tbs t ts)
-    | Some _ -> t
-    | None -> assert false
+    (match kind con with
+    | Def (tbs, t) -> normalize (reduce tbs t ts)
+    | _ -> t
     )
-  | Mut t -> Mut (normalize env t)
+  | Mut t -> Mut (normalize t)
   | t -> t
 
-let rec promote env = function
+let rec promote = function
   | Con (con, ts) ->
-    (match Con.Env.find_opt con env with
-    | Some (Def (tbs, t) | Abs (tbs, t)) -> promote env (reduce tbs t ts)
-    | None -> assert false
-    )
+    let Def (tbs, t) | Abs (tbs, t) = kind con
+    in promote (reduce tbs t ts)
   | t -> t
 
 
@@ -263,43 +276,43 @@ let as_async = function Async t -> t | _ -> invalid "as_async"
 let as_mut = function Mut t -> t | _ -> invalid "as_mut"
 let as_immut = function Mut t -> t | t -> t
 
-let as_prim_sub p env t = match promote env t with
+let as_prim_sub p t = match promote t with
   | Prim p' when p = p' -> ()
   | Non -> ()
   | _ -> invalid "as_prim_sub"
-let rec as_obj_sub name env t = match promote env t with
+let rec as_obj_sub name t = match promote t with
   | Obj (s, tfs) -> s, tfs
-  | Array t -> as_obj_sub name env (array_obj t)
+  | Array t -> as_obj_sub name (array_obj t)
   | Non -> Object Sharable, [{name; typ = Non}]
   | _ -> invalid "as_obj_sub"
-let as_array_sub env t = match promote env t with
+let as_array_sub t = match promote t with
   | Array t -> t
   | Non -> Non
   | _ -> invalid "as_array_sub"
-let as_opt_sub env t = match promote env t with
+let as_opt_sub t = match promote t with
   | Opt t -> t
   | _ -> invalid "as_opt_sub"
-let as_tup_sub n env t = match promote env t with
+let as_tup_sub n t = match promote t with
   | Tup ts -> ts
   | Non -> Lib.List.make n Non
   | _ -> invalid "as_tup_sub"
-let as_unit_sub env t = match promote env t with
+let as_unit_sub t = match promote t with
   | Tup []
   | Non -> ()
   | _ -> invalid "as_unit_sub"
-let as_pair_sub env t = match promote env t with
+let as_pair_sub t = match promote t with
   | Tup [t1; t2] -> t1, t2
   | Non -> Non, Non
   | _ -> invalid "as_pair_sub"
-let as_func_sub n env t = match promote env t with
+let as_func_sub n t = match promote t with
   | Func (_, _, tbs, ts1, ts2) -> tbs, seq ts1,  seq ts2
   | Non -> Lib.List.make n {var = "X"; bound = Any}, Any, Non
   | _ -> invalid "as_func_sub"
-let as_mono_func_sub env t = match promote env t with
+let as_mono_func_sub t = match promote t with
   | Func (_, _, [], ts1, ts2) -> seq ts1, seq ts2
   | Non -> Any, Non
   | _ -> invalid "as_func_sub"
-let as_async_sub env t = match promote env t with
+let as_async_sub t = match promote t with
   | Async t -> t
   | Non -> Non
   | _ -> invalid "as_async_sub"
@@ -312,9 +325,9 @@ let lookup_field name' tfs =
 
 (* Span *)
 
-let rec span env = function
+let rec span = function
   | Var _ | Pre -> assert false
-  | Con _ as t -> span env (promote env t)
+  | Con _ as t -> span (promote t)
   | Prim Null -> Some 1
   | Prim Bool -> Some 2
   | Prim (Nat | Int | Float | Text) -> None
@@ -324,7 +337,7 @@ let rec span env = function
   | Obj _ | Tup _ | Async _ -> Some 1
   | Array _ | Func _ | Shared | Any -> None
   | Opt _ -> Some 2
-  | Mut t -> span env t
+  | Mut t -> span t
   | Non -> Some 0
 
 
@@ -332,52 +345,67 @@ let rec span env = function
 
 exception Unavoidable of con
 
-let rec avoid' env env' = function
+module ConSet =
+  struct
+    include Set.Make(struct type t = con let compare = Con.compare end)
+    exception Clash of elt
+    let disjoint_add e set =
+      if mem e set then raise (Clash e)
+      else add e set
+    let disjoint_union set1 set2 =
+      fold (fun e s -> disjoint_add e s) set2 set1
+  end
+
+type con_set = ConSet.t
+
+let rec avoid' cons = function
   | (Prim _ | Var _ | Any | Non | Shared | Pre) as t -> t
   | Con (c, ts) ->
-    (match Con.Env.find_opt c env' with
-    | Some (Abs _) -> raise (Unavoidable c)
-    | Some (Def (tbs, t)) -> avoid' env env' (reduce tbs t ts)
-    | None ->
-      try
-        Con (c, List.map (avoid' env env') ts)
-      with Unavoidable _ ->
-        match Con.Env.find c env with
-        | Abs _ -> raise (Unavoidable c)
-        | Def (tbs, t) -> avoid' env env' (reduce tbs t ts)
-    )
-  | Array t -> Array (avoid' env env' t)
-  | Tup ts -> Tup (List.map (avoid' env env') ts)
+    if ConSet.mem c cons
+    then match kind c with
+      | Abs _ -> raise (Unavoidable c)
+      | Def (tbs, t) -> avoid' cons (reduce tbs t ts)
+    else
+      begin try
+        Con (c, List.map (avoid' cons) ts)
+      with Unavoidable d ->
+        begin match kind c with
+        | Def (tbs, t) -> avoid' cons (reduce tbs t ts)
+        | Abs _ -> raise (Unavoidable d)
+        end
+      end
+  | Array t -> Array (avoid' cons t)
+  | Tup ts -> Tup (List.map (avoid' cons) ts)
   | Func (s, c, tbs, ts1, ts2) ->
     Func (s,
           c,
-          List.map (avoid_bind env env') tbs,
-          List.map (avoid' env env') ts1, List.map (avoid' env env') ts2)
-  | Opt t -> Opt (avoid' env env' t)
-  | Async t -> Async (avoid' env env' t)
-  | Obj (s, fs) -> Obj (s, List.map (avoid_field env env') fs)
-  | Mut t -> Mut (avoid' env env' t)
+          List.map (avoid_bind cons) tbs,
+          List.map (avoid' cons) ts1, List.map (avoid' cons) ts2)
+  | Opt t -> Opt (avoid' cons t)
+  | Async t -> Async (avoid' cons t)
+  | Obj (s, fs) -> Obj (s, List.map (avoid_field cons) fs)
+  | Mut t -> Mut (avoid' cons t)
 
-and avoid_bind env env' {var; bound} =
-  {var; bound = avoid' env env' bound}
+and avoid_bind cons {var; bound} =
+  {var; bound = avoid' cons bound}
 
-and avoid_field env env' {name; typ} =
-  {name; typ = avoid' env env' typ}
+and avoid_field cons {name; typ} =
+  {name; typ = avoid' cons typ}
 
-let avoid env env' t =
-  if env' = Con.Env.empty then t else
-  avoid' env env' t
+let avoid cons t =
+  if cons = ConSet.empty then t else
+  avoid' cons t
 
 
 (* Equivalence & Subtyping *)
 
 module S = Set.Make (struct type t = typ * typ let compare = compare end)
 
-let rel_list p env rel eq xs1 xs2 =
-  try List.for_all2 (p env rel eq) xs1 xs2 with Invalid_argument _ -> false
+let rel_list p rel eq xs1 xs2 =
+  try List.for_all2 (p rel eq) xs1 xs2 with Invalid_argument _ -> false
 
 let str = ref (fun _ -> failwith "")
-let rec rel_typ env rel eq t1 t2 =
+let rec rel_typ rel eq t1 t2 =
 (*Printf.printf "[sub] %s == %s\n%!" (!str t1) (!str t2);*)
   t1 == t2 || S.mem (t1, t2) !rel || begin
   rel := S.add (t1, t2) !rel;
@@ -391,30 +419,30 @@ let rec rel_typ env rel eq t1 t2 =
   | Non, _ when rel != eq ->
     true
   | Con (con1, ts1), Con (con2, ts2) ->
-    (match Con.Env.find con1 env, Con.Env.find con2 env with
+    (match kind con1, kind con2 with
     | Def (tbs, t), _ -> (* TBR this may fail to terminate *)
-      rel_typ env rel eq (open_ ts1 t) t2
+      rel_typ rel eq (open_ ts1 t) t2
     | _, Def (tbs, t) -> (* TBR this may fail to terminate *)
-      rel_typ env rel eq t1 (open_ ts2 t)
-    | _ when con1 = con2 ->
-      rel_list eq_typ env rel eq ts1 ts2
+      rel_typ rel eq t1 (open_ ts2 t)
+    | _ when Con.eq con1 con2 ->
+      rel_list eq_typ rel eq ts1 ts2
     | Abs (tbs, t), _ when rel != eq ->
-      rel_typ env rel eq (open_ ts1 t) t2
+      rel_typ rel eq (open_ ts1 t) t2
     | _ ->
       false
     )
   | Con (con1, ts1), t2 ->
-    (match Con.Env.find con1 env, t2 with
+    (match kind con1, t2 with
     | Def (tbs, t), _ -> (* TBR this may fail to terminate *)
-      rel_typ env rel eq (open_ ts1 t) t2
+      rel_typ rel eq (open_ ts1 t) t2
     | Abs (tbs, t), _ when rel != eq ->
-      rel_typ env rel eq (open_ ts1 t) t2
+      rel_typ rel eq (open_ ts1 t) t2
     | _ -> false
     )
   | t1, Con (con2, ts2) ->
-    (match Con.Env.find con2 env with
+    (match kind con2 with
     | Def (tbs, t) -> (* TBR this may fail to terminate *)
-      rel_typ env rel eq t1 (open_ ts2 t)
+      rel_typ rel eq t1 (open_ ts2 t)
     | _ -> false
     )
   | Prim p1, Prim p2 when p1 = p2 ->
@@ -425,31 +453,31 @@ let rec rel_typ env rel eq t1 t2 =
     true
   | Obj (s1, tfs1), Obj (s2, tfs2) ->
     s1 = s2 &&
-    rel_fields env rel eq tfs1 tfs2
+    rel_fields rel eq tfs1 tfs2
   | Obj (s, _), Shared when rel != eq ->
     s <> Object Local
   | Array t1', Array t2' ->
-    rel_typ env rel eq t1' t2'
+    rel_typ rel eq t1' t2'
   | Array t1', Obj _ when rel != eq ->
-    rel_typ env rel eq (array_obj t1') t2
+    rel_typ rel eq (array_obj t1') t2
   | Array t, Shared when rel != eq ->
-    rel_typ env rel eq t Shared
+    rel_typ rel eq t Shared
   | Opt t1', Opt t2' ->
-    rel_typ env rel eq t1' t2'
+    rel_typ rel eq t1' t2'
   | Opt t1', Shared ->
-    rel_typ env rel eq t1' Shared
+    rel_typ rel eq t1' Shared
   | Prim Null, Opt t2' when rel != eq ->
     true
   | Tup ts1, Tup ts2 ->
-    rel_list rel_typ env rel eq ts1 ts2
+    rel_list rel_typ rel eq ts1 ts2
   | Tup ts1, Shared ->
-    rel_list rel_typ env rel eq ts1 (List.map (fun _ -> Shared) ts1)
+    rel_list rel_typ rel eq ts1 (List.map (fun _ -> Shared) ts1)
   | Func (s1, c1, tbs1, t11, t12), Func (s2, c2, tbs2, t21, t22) ->
     c1 = c2 && s1 = s2 &&
-    (match rel_binds env rel eq tbs1 tbs2 with
-    | Some (ts, env') ->
-      rel_list rel_typ env' rel eq (List.map (open_ ts) t21) (List.map (open_ ts) t11) &&
-      rel_list rel_typ env' rel eq (List.map (open_ ts) t12) (List.map (open_ ts) t22)
+    (match rel_binds rel eq tbs1 tbs2 with
+    | Some ts ->
+      rel_list rel_typ rel eq (List.map (open_ ts) t21) (List.map (open_ ts) t11) &&
+      rel_list rel_typ rel eq (List.map (open_ ts) t12) (List.map (open_ ts) t22)
     | None -> false
     )
   | Func (Sharable, _,  _, _, _), Shared when rel != eq ->
@@ -457,13 +485,13 @@ let rec rel_typ env rel eq t1 t2 =
   | Shared, Shared ->
     true
   | Async t1', Async t2' ->
-    rel_typ env rel eq t1' t2'
+    rel_typ rel eq t1' t2'
   | Mut t1', Mut t2' ->
-    eq_typ env rel eq t1' t2'
+    eq_typ rel eq t1' t2'
   | _, _ -> false
   end
 
-and rel_fields env rel eq tfs1 tfs2 =
+and rel_fields rel eq tfs1 tfs2 =
   (* Assume that tf1 and tf2 are sorted. *)
   match tfs1, tfs2 with
   | [], [] ->
@@ -473,37 +501,48 @@ and rel_fields env rel eq tfs1 tfs2 =
   | tf1::tfs1', tf2::tfs2' ->
     (match compare_field tf1 tf2 with
     | 0 ->
-      rel_typ env rel eq tf1.typ tf2.typ &&
-      rel_fields env rel eq tfs1' tfs2'
+      rel_typ rel eq tf1.typ tf2.typ &&
+      rel_fields rel eq tfs1' tfs2'
     | -1 when rel != eq ->
-      rel_fields env rel eq tfs1' tfs2
+      rel_fields rel eq tfs1' tfs2
     | _ -> false
     )
   | _, _ -> false
 
-and rel_binds env rel eq tbs1 tbs2 =
-  let ts, env' = open_binds env tbs2 in
-  if rel_list (rel_bind ts) env' rel eq tbs2 tbs1
-  then Some (ts, env')
+and rel_binds rel eq tbs1 tbs2 =
+  let ts = open_binds tbs2 in
+  if rel_list (rel_bind ts) rel eq tbs2 tbs1
+  then Some ts
   else None
 
-and rel_bind ts env rel eq tb1 tb2 =
-  rel_typ env rel eq (open_ ts tb1.bound) (open_ ts tb2.bound)
+and rel_bind ts rel eq tb1 tb2 =
+  rel_typ rel eq (open_ ts tb1.bound) (open_ ts tb2.bound)
+
+and eq_typ rel eq t1 t2 = rel_typ eq eq t1 t2
 
-and eq_typ env rel eq t1 t2 = rel_typ env eq eq t1 t2
+and eq t1 t2 : bool =
+  let eq = ref S.empty in eq_typ eq eq t1 t2
 
-and eq (env : con_env) t1 t2 : bool =
-  let eq = ref S.empty in eq_typ env eq eq t1 t2
-and sub (env : con_env) t1 t2 : bool =
-  rel_typ env (ref S.empty) (ref S.empty) t1 t2
+and sub  t1 t2 : bool =
+  rel_typ (ref S.empty) (ref S.empty) t1 t2
 
+and eq_kind k1 k2 : bool =
+  let eq = ref S.empty in
+  match k1, k2 with
+  | Def (tbs1, t1), Def (tbs2, t2)
+  | Abs (tbs1, t1), Abs (tbs2, t2) ->
+  begin match rel_binds eq eq tbs1 tbs2 with
+    | Some ts -> eq_typ eq eq  (open_ ts t1) (open_ ts t2)
+    | None -> false
+  end
+  | _ -> false
 
 (* Least upper bound and greatest lower bound *)
 
-let rec lub env t1 t2 =
+let rec lub t1 t2 =
   if t1 == t2 then t1 else
   (* TBR: this is just a quick hack *)
-  match normalize env t1, normalize env t2 with
+  match normalize t1, normalize t2 with
   | _, Pre
   | Pre, _ -> Pre
   | _, Any
@@ -512,19 +551,19 @@ let rec lub env t1 t2 =
   | Non, _ -> t2
   | Prim Nat, Prim Int
   | Prim Int, Prim Nat -> Prim Int
-  | Opt t1', Opt t2' -> Opt (lub env t1' t2')
+  | Opt t1', Opt t2' -> Opt (lub t1' t2')
   | Prim Null, Opt t'
   | Opt t', Prim Null -> Opt t'
-  | Array t1', (Obj _ as t2) -> lub env (array_obj t1') t2
-  | (Obj _ as t1), Array t2' -> lub env t1 (array_obj t2')
-  | t1', t2' when eq env t1' t2' -> t1
+  | Array t1', (Obj _ as t2) -> lub (array_obj t1') t2
+  | (Obj _ as t1), Array t2' -> lub t1 (array_obj t2')
+  | t1', t2' when eq t1' t2' -> t1
   | _ -> Any
 
 
-let rec glb env t1 t2 =
+let rec glb t1 t2 =
   if t1 == t2 then t1 else
   (* TBR: this is just a quick hack *)
-  match normalize env t1, normalize env t2 with
+  match normalize t1, normalize t2 with
   | _, Pre
   | Pre, _ -> Pre
   | _, Any -> t1
@@ -533,10 +572,10 @@ let rec glb env t1 t2 =
   | Non, _ -> Non
   | Prim Nat, Prim Int
   | Prim Int, Prim Nat -> Prim Nat
-  | Opt t1', Opt t2' -> Opt (glb env t1' t2')
+  | Opt t1', Opt t2' -> Opt (glb t1' t2')
   | Prim Null, Opt _
   | Opt _, Prim Null -> Prim Null
-  | t1', t2' when eq env t1' t2' -> t1
+  | t1', t2' when eq t1' t2' -> t1
   | _ -> Non
 
 
@@ -669,16 +708,16 @@ let string_of_kind k =
   sprintf "%s %s%s" op sbs st
 
 
-let rec string_of_typ_expand env t =
+let rec string_of_typ_expand t =
   let s = string_of_typ t in
   match t with
   | Con (c, ts) ->
-    (match Con.Env.find c env with
+    (match kind c with
     | Abs _ -> s
     | Def _ ->
-      match normalize env t with
+      match normalize t with
       | Prim _ | Any | Non -> s
-      | t' -> s ^ " = " ^ string_of_typ_expand env t'
+      | t' -> s ^ " = " ^ string_of_typ_expand t'
     )
   | _ -> s
 
diff --git a/src/type.mli b/src/type.mli
index 884ac714070..7d4caa10137 100644
--- a/src/type.mli
+++ b/src/type.mli
@@ -1,6 +1,5 @@
 (* Representation *)
 
-type con = Con.t
 type control = Returns | Promises (* returns a computed value or immediate promise *)
 type sharing = Local | Sharable
 type obj_sort = Object of sharing | Actor
@@ -40,15 +39,35 @@ and typ =
 and bind = {var : string; bound : typ}
 and field = {name : string; typ : typ}
 
-(* field ordering *)
-
-val compare_field : field -> field -> int
+(* cons and kinds *)
 
-type kind =
+and con_annot (* abstract *)
+and con = con_annot Con.t
+and kind =
   | Def of bind list * typ
   | Abs of bind list * typ
 
-type con_env = kind Con.Env.t
+
+val kind : con -> kind
+val fresh_con : string -> kind -> con
+val set_kind : con -> kind -> unit
+val modify_kind : con -> (kind -> kind) -> unit
+val clone_con : con -> kind -> con
+
+module ConSet :
+sig
+  include Set.S with type elt = con
+  exception Clash of elt
+  val disjoint_add : elt -> t -> t (* raises Clash *)
+  val disjoint_union : t -> t -> t (* raises Clash *)
+end
+
+type con_set = ConSet.t
+
+(* field ordering *)
+
+val compare_field : field -> field -> int
+
 
 (* n-ary argument/result sequences *)
 
@@ -91,39 +110,40 @@ val as_async : typ -> typ
 val as_mut : typ -> typ
 val as_immut : typ -> typ
 
-val as_prim_sub : prim -> con_env -> typ -> unit
-val as_obj_sub : string -> con_env -> typ -> obj_sort * field list
-val as_array_sub : con_env -> typ -> typ
-val as_opt_sub : con_env -> typ -> typ
-val as_tup_sub : int -> con_env -> typ -> typ list
-val as_unit_sub : con_env -> typ -> unit
-val as_pair_sub : con_env -> typ -> typ * typ
-val as_func_sub : int -> con_env -> typ -> bind list * typ * typ
-val as_mono_func_sub : con_env -> typ -> typ * typ
-val as_async_sub : con_env -> typ -> typ
+val as_prim_sub : prim -> typ -> unit
+val as_obj_sub : string -> typ -> obj_sort * field list
+val as_array_sub : typ -> typ
+val as_opt_sub : typ -> typ
+val as_tup_sub : int -> typ -> typ list
+val as_unit_sub : typ -> unit
+val as_pair_sub : typ -> typ * typ
+val as_func_sub : int -> typ -> bind list * typ * typ
+val as_mono_func_sub : typ -> typ * typ
+val as_async_sub : typ -> typ
 
 val lookup_field : string -> field list -> typ
 
-val span : con_env -> typ -> int option
+val span : typ -> int option
 
 
 (* Normalization and Classification *)
 
-val normalize : con_env -> typ -> typ
-val promote : con_env -> typ -> typ
+val normalize : typ -> typ
+val promote : typ -> typ
 
 exception Unavoidable of con
-val avoid : con_env -> con_env -> typ -> typ (* raise Unavoidable *)
+val avoid : con_set -> typ -> typ (* raise Unavoidable *)
 
 
 (* Equivalence and Subtyping *)
 
-val eq : con_env -> typ -> typ -> bool
-val sub : con_env -> typ -> typ -> bool
+val eq : typ -> typ -> bool
+val eq_kind : kind -> kind -> bool
 
-val lub : con_env -> typ -> typ -> typ
-val glb : con_env -> typ -> typ -> typ
+val sub : typ -> typ -> bool
 
+val lub : typ -> typ -> typ
+val glb : typ -> typ -> typ
 
 (* First-order substitution *)
 
@@ -131,7 +151,7 @@ val close : con list -> typ -> typ
 val close_binds : con list -> bind list -> bind list
 
 val open_ : typ list -> typ -> typ
-val open_binds : con_env -> bind list -> typ list * con_env
+val open_binds : bind list -> typ list
 
 
 (* Environments *)
@@ -147,4 +167,4 @@ val string_of_typ : typ -> string
 val string_of_kind : kind -> string
 val strings_of_kind : kind -> string * string * string
 
-val string_of_typ_expand : con_env -> typ -> string
+val string_of_typ_expand : typ -> string
diff --git a/src/typing.ml b/src/typing.ml
index 0d61df20c8e..35e1327b742 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -19,7 +19,8 @@ let recover f y = recover_with () f y
 
 type val_env = T.typ T.Env.t
 type typ_env = T.con T.Env.t
-type con_env = T.con_env
+type con_env = T.con_set
+
 
 type scope =
   { val_env : val_env;
@@ -30,13 +31,13 @@ type scope =
 let empty_scope : scope =
   { val_env = T.Env.empty;
     typ_env = T.Env.empty;
-    con_env = Con.Env.empty
+    con_env = T.ConSet.empty
   }
 
 let adjoin_scope scope1 scope2 =
   { val_env = T.Env.adjoin scope1.val_env scope2.val_env;
     typ_env = T.Env.adjoin scope1.typ_env scope2.typ_env;
-    con_env = Con.Env.adjoin scope1.con_env scope2.con_env;
+    con_env = T.ConSet.disjoint_union scope1.con_env scope2.con_env;
   }
 
 (* Contexts (internal) *)
@@ -80,35 +81,28 @@ let warn env at fmt =
 
 
 let add_lab c x t = {c with labs = T.Env.add x t c.labs}
+
 let add_val c x t = {c with vals = T.Env.add x t c.vals}
-(*
-let add_con c con k = {c with cons = Con.Env.add con k c.cons}
-let add_typ c x con k =
-  { c with
-    typs = T.Env.add x con c.typs;
-    cons = Con.Env.add con k c.cons;
-  }
-*)
 
-let add_typs c xs cs ks =
+let add_typs c xs cs =
   { c with
     typs = List.fold_right2 T.Env.add xs cs c.typs;
-    cons = List.fold_right2 Con.Env.add cs ks c.cons;
+    cons = List.fold_right T.ConSet.disjoint_add cs c.cons;
   }
 
 let adjoin c scope =
   { c with
     vals = T.Env.adjoin c.vals scope.val_env;
     typs = T.Env.adjoin c.typs scope.typ_env;
-    cons = Con.Env.adjoin 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 = Con.Env.adjoin c.cons ce}
+
 let adjoin_typs c te ce =
   { c with
     typs = T.Env.adjoin c.typs te;
-    cons = Con.Env.adjoin c.cons ce;
+    cons = T.ConSet.disjoint_union c.cons ce;
   }
 
 let disjoint_union env at fmt env1 env2 =
@@ -141,10 +135,11 @@ and check_typ' env typ : T.typ =
   match typ.it with
   | VarT (id, typs) ->
     (match T.Env.find_opt id.it env.typs with
-    | Some c ->
-      let T.Def (tbs, t) | T.Abs (tbs, t) = Con.Env.find c env.cons in
+    | Some con ->
+      let kind = T.kind con in
+      let T.Def (tbs, t) | T.Abs (tbs, t) = kind in
       let ts = check_typ_bounds env tbs typs typ.at in
-	    T.Con (c, ts)
+      T.Con (con, ts)
     | None -> error env id.at "unbound type identifier %s" id.it
     )
   | PrimT "Any" -> T.Any
@@ -169,17 +164,17 @@ and check_typ' env typ : T.typ =
     let c = match typs2 with [{it = AsyncT _; _}] -> T.Promises | _ -> T.Returns in
     if sort.it = T.Sharable then begin
       let t1 = T.seq ts1 in
-      if not (T.sub env'.cons t1 T.Shared) then
+      if not (T.sub t1 T.Shared) then
         error env typ1.at "shared function has non-shared parameter type\n  %s"
-          (T.string_of_typ_expand env'.cons t1);
+          (T.string_of_typ_expand t1);
       (match ts2 with
       | [] -> ()
       | [T.Async t2] ->
-        if not (T.sub env'.cons t2 T.Shared) then
+        if not (T.sub t2 T.Shared) then
           error env typ1.at "shared function has non-shared result type\n  %s"
-            (T.string_of_typ_expand env'.cons t2);
+            (T.string_of_typ_expand t2);
       | _ -> error env typ1.at "shared function has non-async result type\n  %s"
-          (T.string_of_typ_expand env'.cons (T.seq ts2))
+          (T.string_of_typ_expand (T.seq ts2))
       )
     end;
     let tbs = List.map2 (fun c t -> {T.var = Con.name c; bound = t}) cs ts in
@@ -188,10 +183,10 @@ and check_typ' env typ : T.typ =
     T.Opt (check_typ env typ)
   | AsyncT typ ->
     let t = check_typ env typ in
-    let t' = T.promote env.cons t in
-    if t' <> T.Pre && not (T.sub env.cons t' T.Shared) then
+    let t' = T.promote t in
+    if t' <> T.Pre && not (T.sub t' T.Shared) then
       error env typ.at "async type has non-shared parameter type\n  %s"
-        (T.string_of_typ_expand env.cons t');
+        (T.string_of_typ_expand t');
     T.Async t
   | ObjT (sort, fields) ->
     check_ids env (List.map (fun (field : typ_field) -> field.it.id) fields);
@@ -203,41 +198,41 @@ and check_typ' env typ : T.typ =
 and check_typ_field env s typ_field : T.field =
   let {id; mut; typ} = typ_field.it in
   let t = infer_mut mut (check_typ env typ) in
-  if s = T.Actor && not (T.is_func (T.promote env.cons t)) then
+  if s = T.Actor && not (T.is_func (T.promote t)) then
     error env typ.at "actor field %s has non-function type\n  %s"
-      id.it (T.string_of_typ_expand env.cons t);
-  if s <> T.Object T.Local && not (T.sub env.cons t T.Shared) then
+      id.it (T.string_of_typ_expand t);
+  if s <> T.Object T.Local && not (T.sub t T.Shared) then
     error env typ.at "shared object or actor field %s has non-shared type\n  %s"
-      id.it (T.string_of_typ_expand env.cons t);
+      id.it (T.string_of_typ_expand t);
   {T.name = id.it; typ = t}
 
 and check_typ_binds env typ_binds : T.con list * T.typ list * typ_env * con_env =
   let xs = List.map (fun typ_bind -> typ_bind.it.var.it) typ_binds in
-  let cs = List.map (fun x -> Con.fresh x) xs in
-  List.iter2 (fun typ_bind c -> typ_bind.note <- Some c) typ_binds cs;
+  let cs = List.map (fun n -> T.fresh_con n (T.Abs ([], T.Pre))) xs in
   let te = List.fold_left2 (fun te typ_bind c ->
       let id = typ_bind.it.var in
       if T.Env.mem id.it te then
         error env id.at "duplicate type name %s in type parameter list" id.it;
       T.Env.add id.it c te
     ) T.Env.empty typ_binds cs in
-  let pre_ks = List.map (fun c -> T.Abs ([], T.Pre)) cs in
-  let pre_env' = add_typs {env with pre = true} xs cs pre_ks in
+  let pre_env' = add_typs {env with pre = true} xs cs  in
   let ts = List.map (fun typ_bind -> check_typ pre_env' typ_bind.it.bound) typ_binds in
-  let ks = List.map2 (fun c t -> T.Abs ([], t)) cs ts in
-  let env' = add_typs env xs cs ks in
+  let ks = List.map (fun t -> T.Abs ([], t)) ts in
+  List.iter2 T.set_kind cs ks;
+  let env' = add_typs env xs cs in
   let _ = List.map (fun typ_bind -> check_typ env' typ_bind.it.bound) typ_binds in
-  cs, ts, te, Con.Env.from_list2 cs ks
+  List.iter2 (fun typ_bind c -> typ_bind.note <- Some c) typ_binds cs;
+  cs, ts, te, T.ConSet.of_list cs
 
 and check_typ_bounds env (tbs : T.bind list) typs at : T.typ list =
   match tbs, typs with
   | tb::tbs', typ::typs' ->
     let t = check_typ env typ in
     if not env.pre then begin
-      if not (T.sub env.cons t tb.T.bound) then
+      if not (T.sub t tb.T.bound) then
         local_error env typ.at "type argument\n  %s\ndoes not match parameter bound\n  %s"
-          (T.string_of_typ_expand env.cons t)
-          (T.string_of_typ_expand env.cons tb.T.bound)
+          (T.string_of_typ_expand t)
+          (T.string_of_typ_expand tb.T.bound)
     end;
     let ts' = check_typ_bounds env tbs' typs' at in
     t::ts'
@@ -291,7 +286,7 @@ let infer_lit env lit at : T.prim =
     assert false
 
 let check_lit env t lit at =
-  match T.normalize env.cons t, !lit with
+  match T.normalize t, !lit with
   | T.Opt _, NullLit -> ()
   | T.Prim T.Nat, PreLit (s, T.Nat) ->
     lit := NatLit (check_nat env at s)
@@ -309,9 +304,9 @@ let check_lit env t lit at =
     lit := FloatLit (check_float env at s)
   | t, _ ->
     let t' = T.Prim (infer_lit env lit at) in
-    if not (T.sub env.cons t' t) then
+    if not (T.sub t' t) then
       local_error env at "literal of type\n  %s\ndoes not have expected type\n  %s"
-        (T.string_of_typ t') (T.string_of_typ_expand env.cons t)
+        (T.string_of_typ t') (T.string_of_typ_expand t)
 
 
 (* Expressions *)
@@ -329,10 +324,10 @@ let rec infer_exp env exp : T.typ =
 
 and infer_exp_promote env exp : T.typ =
   let t = infer_exp env exp in
-  let t' = T.promote env.cons t in
+  let t' = T.promote t in
   if t' = T.Pre then
     error env exp.at "cannot infer type of expression while trying to infer surrounding class type,\nbecause its type is a forward reference to type\n  %s"
-      (T.string_of_typ_expand env.cons t);
+      (T.string_of_typ_expand  t);
   t'
 
 and infer_exp_mut env exp : T.typ =
@@ -341,7 +336,7 @@ and infer_exp_mut env exp : T.typ =
   assert (t <> T.Pre);
   if not env.pre then begin
     let e = A.infer_effect_exp exp in
-    exp.note <- {note_typ = T.normalize env.cons t; note_eff = e}
+    exp.note <- {note_typ = T.normalize t; note_eff = e}
   end;
   t
 
@@ -366,33 +361,33 @@ and infer_exp' env exp : T.typ =
       assert (!ot = Type.Pre);
       if not (Operator.has_unop t op) then
         error env exp.at "operator is not defined for operand type\n  %s"
-          (T.string_of_typ_expand env.cons t);
+          (T.string_of_typ_expand t);
       ot := t;
     end;
     t
   | BinE (ot, exp1, op, exp2) ->
     let t1 = infer_exp_promote env exp1 in
     let t2 = infer_exp_promote env exp2 in
-    let t = T.lub env.cons t1 t2 in
+    let t = T.lub t1 t2 in
     if not env.pre then begin
       assert (!ot = Type.Pre);
       if not (Operator.has_binop t op) then
         error env exp.at "operator not defined for operand types\n  %s and\n  %s"
-          (T.string_of_typ_expand env.cons t1)
-          (T.string_of_typ_expand env.cons t2);
+          (T.string_of_typ_expand t1)
+          (T.string_of_typ_expand t2);
       ot := t
     end;
     t
   | RelE (ot, exp1, op, exp2) ->
     let t1 = infer_exp_promote env exp1 in
     let t2 = infer_exp_promote env exp2 in
-    let t = T.lub env.cons t1 t2 in
+    let t = T.lub t1 t2 in
     if not env.pre then begin
       assert (!ot = Type.Pre);
       if not (Operator.has_relop t op) then
         error env exp.at "operator not defined for operand types\n  %s and\n  %s"
-          (T.string_of_typ_expand env.cons t1)
-          (T.string_of_typ_expand env.cons t2);
+          (T.string_of_typ_expand t1)
+          (T.string_of_typ_expand t2);
       ot := t;
     end;
     T.bool
@@ -405,15 +400,15 @@ and infer_exp' env exp : T.typ =
   | ProjE (exp1, n) ->
     let t1 = infer_exp_promote env exp1 in
     (try
-      let ts = T.as_tup_sub n env.cons t1 in
+      let ts = T.as_tup_sub n t1 in
       match List.nth_opt ts n with
       | Some t -> t
       | None ->
         error env exp.at "tuple projection %n is out of bounds for type\n  %s"
-          n (T.string_of_typ_expand env.cons t1)
+          n (T.string_of_typ_expand t1)
     with Invalid_argument _ ->
       error env exp1.at "expected tuple type, but expression produces type\n  %s"
-        (T.string_of_typ_expand env.cons t1)
+        (T.string_of_typ_expand t1)
     )
   | ObjE (sort, id, fields) ->
     let env' = if sort.it = T.Actor then {env with async = false} else env in
@@ -421,16 +416,16 @@ and infer_exp' env exp : T.typ =
   | DotE (exp1, sr, {it = Name n; _}) ->
     let t1 = infer_exp_promote env exp1 in
     (try
-      let s, tfs = T.as_obj_sub n env.cons t1 in
+      let s, tfs = T.as_obj_sub n t1 in
       sr := s;
       match List.find_opt (fun {T.name; _} -> name = n) tfs with
       | Some {T.typ = t; _} -> t
       | None ->
         error env exp1.at "field name %s does not exist in type\n  %s"
-          n (T.string_of_typ_expand env.cons t1)
+          n (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 env.cons t1)
+        (T.string_of_typ_expand t1)
     )
   | AssignE (exp1, exp2) ->
     if not env.pre then begin
@@ -444,9 +439,9 @@ and infer_exp' env exp : T.typ =
     T.unit
   | ArrayE (mut, exps) ->
     let ts = List.map (infer_exp env) exps in
-    let t1 = List.fold_left (T.lub env.cons) T.Non ts in
+    let t1 = List.fold_left T.lub T.Non ts in
     if
-      t1 = T.Any && List.for_all (fun t -> T.promote env.cons t <> T.Any) ts
+      t1 = T.Any && List.for_all (fun t -> T.promote t <> T.Any) ts
     then
       warn env exp.at "this array has type %s because elements have inconsistent types"
         (T.string_of_typ (T.Array t1));
@@ -454,31 +449,31 @@ and infer_exp' env exp : T.typ =
   | IdxE (exp1, exp2) ->
     let t1 = infer_exp_promote env exp1 in
     (try
-      let t = T.as_array_sub env.cons t1 in
+      let t = T.as_array_sub t1 in
       if not env.pre then check_exp env T.nat exp2;
       t
     with Invalid_argument _ ->
       error env exp1.at "expected array type, but expression produces type\n  %s"
-        (T.string_of_typ_expand env.cons t1)
+        (T.string_of_typ_expand t1)
     )
   | CallE (exp1, insts, exp2) ->
     let t1 = infer_exp_promote env exp1 in
     (try
-      let tbs, t2, t = T.as_func_sub (List.length insts) env.cons t1 in
+      let tbs, t2, t = T.as_func_sub (List.length insts) t1 in
       let ts = check_inst_bounds env tbs insts exp.at in
       if not env.pre then check_exp env (T.open_ ts t2) exp2;
       T.open_ ts t
     with Invalid_argument _ ->
       error env exp1.at "expected function type, but expression produces type\n  %s"
-        (T.string_of_typ_expand env.cons t1)
+        (T.string_of_typ_expand t1)
     )
   | BlockE (decs, ot) ->
     let t, scope = infer_block env decs exp.at in
     let t' =
-      try T.avoid env.cons scope.con_env t with T.Unavoidable c ->
+      try T.avoid scope.con_env t with T.Unavoidable c ->
         error env exp.at "local class type %s is contained in inferred block type\n  %s"
           (Con.to_string c)
-          (T.string_of_typ_expand (Con.Env.adjoin env.cons scope.con_env) t)
+          (T.string_of_typ_expand t)
     in
     ot := t';
     t'
@@ -501,21 +496,21 @@ and infer_exp' env exp : T.typ =
     if not env.pre then check_exp env T.bool exp1;
     let t2 = infer_exp env exp2 in
     let t3 = infer_exp env exp3 in
-    let t = T.lub env.cons t2 t3 in
+    let t = T.lub t2 t3 in
     if
       t = T.Any &&
-      T.promote env.cons t2 <> T.Any && T.promote env.cons t3 <> T.Any
+      T.promote t2 <> T.Any && T.promote t3 <> T.Any
     then
       warn env exp.at "this if has type %s because branches have inconsistent types,\ntrue produces\n  %s\nfalse produces\n  %s"
         (T.string_of_typ t)
-        (T.string_of_typ_expand env.cons t2)
-        (T.string_of_typ_expand env.cons t3);
+        (T.string_of_typ_expand t2)
+        (T.string_of_typ_expand t3);
     t
   | SwitchE (exp1, cases) ->
     let t1 = infer_exp_promote env exp1 in
     let t = infer_cases env t1 T.Non cases in
     if not env.pre then
-      if not (Coverage.check_cases env.cons cases t1) then
+      if not (Coverage.check_cases cases t1) then
         warn env exp.at "the cases in this switch do not cover all possible values";
     t
   | WhileE (exp1, exp2) ->
@@ -534,16 +529,16 @@ and infer_exp' env exp : T.typ =
     if not env.pre then begin
       let t1 = infer_exp_promote env exp1 in
       (try
-        let _, tfs = T.as_obj_sub "next" env.cons t1 in
+        let _, tfs = T.as_obj_sub "next" t1 in
         let t = T.lookup_field "next" tfs in
-        let t1, t2 = T.as_mono_func_sub env.cons t in
-        if not (T.sub env.cons T.unit t1) then raise (Invalid_argument "");
-        let t2' = T.as_opt_sub env.cons t2 in
+        let t1, t2 = T.as_mono_func_sub t in
+        if not (T.sub T.unit t1) then raise (Invalid_argument "");
+        let t2' = T.as_opt_sub t2 in
         let ve = check_pat_exhaustive env t2' pat in
         check_exp (adjoin_vals env ve) T.unit exp2
       with Invalid_argument _ ->
         local_error env exp1.at "expected iterable type, but expression has type\n  %s"
-          (T.string_of_typ_expand env.cons t1)
+          (T.string_of_typ_expand t1)
       );
     end;
     T.unit
@@ -578,19 +573,19 @@ and infer_exp' env exp : T.typ =
     let env' =
       {env with labs = T.Env.empty; rets = Some T.Pre; async = true} in
     let t = infer_exp env' exp1 in
-    if not (T.sub env.cons t T.Shared) then
+    if not (T.sub t T.Shared) then
       error env exp1.at "async type has non-shared parameter type\n  %s"
-        (T.string_of_typ_expand env.cons t);
+        (T.string_of_typ_expand t);
     T.Async t
   | AwaitE exp1 ->
     if not env.async then
       error env exp.at "misplaced await";
     let t1 = infer_exp_promote env exp1 in
     (try
-      T.as_async_sub env.cons t1
+      T.as_async_sub t1
     with Invalid_argument _ ->
       error env exp1.at "expected async type, but expression has type\n  %s"
-        (T.string_of_typ_expand env.cons t1)
+        (T.string_of_typ_expand t1)
     )
   | AssertE exp1 ->
     if not env.pre then check_exp env T.bool exp1;
@@ -602,9 +597,9 @@ and infer_exp' env exp : T.typ =
   | DecE (dec, ot) ->
     let t, scope = infer_block env [dec] exp.at in
     let t' =
-      try T.avoid env.cons scope.con_env t with T.Unavoidable c ->
+      try T.avoid scope.con_env t with T.Unavoidable c ->
         error env exp.at "local class name %s is contained in inferred declaration type\n  %s"
-          (Con.to_string c) (T.string_of_typ_expand env.cons t)
+          (Con.to_string c) (T.string_of_typ_expand t)
     in
     ot := t';
     t'
@@ -613,7 +608,7 @@ and check_exp env t exp =
   assert (not env.pre);
   assert (exp.note.note_typ = T.Pre);
   assert (t <> T.Pre);
-  let t' = T.normalize env.cons t in
+  let t' = T.normalize t in
   check_exp' env t' exp;
   let e = A.infer_effect_exp exp in
   exp.note <- {note_typ = t'; note_eff = e}
@@ -642,7 +637,7 @@ and check_exp' env t exp =
     if (mut.it = Var) <> T.is_mut t' then
       local_error env exp.at "%smutable array expression cannot produce expected type\n  %s"
         (if mut.it = Const then "im" else "")
-        (T.string_of_typ_expand env.cons (T.Array t'));
+        (T.string_of_typ_expand (T.Array t'));
     List.iter (check_exp env (T.as_immut t')) exps
   | AsyncE exp1, T.Async t' ->
     let env' = {env with labs = T.Env.empty; rets = Some t'; async = true} in
@@ -657,14 +652,14 @@ and check_exp' env t exp =
   | SwitchE (exp1, cases), _ ->
     let t1 = infer_exp_promote env exp1 in
     check_cases env t1 t cases;
-    if not (Coverage.check_cases env.cons cases t1) then
+    if not (Coverage.check_cases cases t1) then
       warn env exp.at "the cases in this switch do not cover all possible values";
   | _ ->
     let t' = infer_exp env exp in
-    if not (T.sub env.cons t' t) then
+    if not (T.sub t' t) then
       local_error env exp.at "expression of type\n  %s\ncannot produce expected type\n  %s"
-        (T.string_of_typ_expand env.cons t')
-        (T.string_of_typ_expand env.cons t)
+        (T.string_of_typ_expand t')
+        (T.string_of_typ_expand t)
 
 
 (* Cases *)
@@ -675,15 +670,15 @@ and infer_cases env t_pat t cases : T.typ =
 and infer_case env t_pat t {it = {pat; exp}; at; _} =
   let ve = check_pat env t_pat pat in
   let t' = recover_with T.Non (infer_exp (adjoin_vals env ve)) exp in
-  let t'' = T.lub env.cons t t' in
+  let t'' = T.lub t t' in
   if
     t'' = T.Any &&
-    T.promote env.cons t <> T.Any && T.promote env.cons t' <> T.Any
+    T.promote t <> T.Any && T.promote t' <> T.Any
   then
     warn env at "the switch has type %s because branches have inconsistent types,\nthis case produces type\n  %s\nthe previous produce type\n  %s"
       (T.string_of_typ t'')
-      (T.string_of_typ_expand env.cons t)
-      (T.string_of_typ_expand env.cons t');
+      (T.string_of_typ_expand t)
+      (T.string_of_typ_expand t');
   t''
 
 and check_cases env t_pat t cases =
@@ -718,7 +713,7 @@ and gather_pat env ve0 pat : val_env =
 and infer_pat_exhaustive env pat : T.typ * val_env =
   let t, ve = infer_pat env pat in
   if not env.pre then
-    if not (Coverage.check_pat env.cons pat t) then
+    if not (Coverage.check_pat pat t) then
       warn env pat.at "this pattern does not cover all possible values";
   t, ve
 
@@ -726,7 +721,7 @@ and infer_pat env pat : T.typ * val_env =
   assert (pat.note = T.Pre);
   let t, ve = infer_pat' env pat in
   if not env.pre then
-    pat.note <- T.normalize env.cons t;
+    pat.note <- T.normalize t;
   t, ve
 
 and infer_pat' env pat : T.typ * val_env =
@@ -743,7 +738,7 @@ and infer_pat' env pat : T.typ * val_env =
     let t = if t1 = T.Prim T.Nat then T.Prim T.Int else t1 in
     if not (Operator.has_unop t op) then
       local_error env pat.at "operator is not defined for operand type\n  %s"
-        (T.string_of_typ_expand env.cons t);
+        (T.string_of_typ_expand t);
     t, T.Env.empty
   | TupP pats ->
     let ts, ve = infer_pats pat.at env pats [] T.Env.empty in
@@ -754,7 +749,7 @@ and infer_pat' env pat : T.typ * val_env =
   | AltP (pat1, pat2) ->
     let t1, ve1 = infer_pat env pat1 in
     let t2, ve2 = infer_pat env pat2 in
-    let t = T.lub env.cons t1 t2 in
+    let t = T.lub t1 t2 in
     if ve1 <> T.Env.empty || ve2 <> T.Env.empty then
       error env pat.at "variables are not allowed in pattern alternatives";
     t, T.Env.empty
@@ -774,14 +769,14 @@ and infer_pats at env pats ts ve : T.typ list * val_env =
 and check_pat_exhaustive env t pat : val_env =
   let ve = check_pat env t pat in
   if not env.pre then
-    if not (Coverage.check_pat env.cons pat t) then
+    if not (Coverage.check_pat pat t) then
       warn env pat.at "this pattern does not cover all possible values";
   ve
 
 and check_pat env t pat : val_env =
   assert (pat.note = T.Pre);
   if t = T.Pre then snd (infer_pat env pat) else
-  let t' = T.normalize env.cons t in
+  let t' = T.normalize t in
   let ve = check_pat' env t' pat in
   if not env.pre then pat.note <- t';
   ve
@@ -798,20 +793,20 @@ and check_pat' env t pat : val_env =
     T.Env.empty
   | SignP (op, lit) ->
     if not env.pre then begin
-      let t' = T.normalize env.cons t in
+      let t' = T.normalize t in
       if not (Operator.has_unop t op) then
         local_error env pat.at "operator cannot consume expected type\n  %s"
-          (T.string_of_typ_expand env.cons t');
+          (T.string_of_typ_expand t');
       check_lit env t' lit pat.at
     end;
     T.Env.empty
   | TupP pats ->
     (try
-      let ts = T.as_tup_sub (List.length pats) env.cons t in
+      let ts = T.as_tup_sub (List.length pats) t in
       check_pats env ts pats T.Env.empty pat.at
     with Invalid_argument _ ->
       error env pat.at "tuple pattern cannot consume expected type\n  %s"
-        (T.string_of_typ_expand env.cons t)
+        (T.string_of_typ_expand t)
     )
   | OptP pat1 ->
     (try
@@ -819,7 +814,7 @@ and check_pat' env t pat : val_env =
       check_pat env t1 pat1
     with Invalid_argument _ ->
       error env pat.at "option pattern cannot consume expected type\n  %s"
-        (T.string_of_typ_expand env.cons t)
+        (T.string_of_typ_expand t)
     )
   | AltP (pat1, pat2) ->
     let ve1 = check_pat env t pat1 in
@@ -829,10 +824,10 @@ and check_pat' env t pat : val_env =
     T.Env.empty
   | _ ->
     let t', ve = infer_pat env pat in
-    if not (T.sub env.cons t t') then
+    if not (T.sub t t') then
       error env pat.at "pattern of type\n  %s\ncannot consume expected type\n  %s"
-        (T.string_of_typ_expand env.cons t')
-        (T.string_of_typ_expand env.cons t);
+        (T.string_of_typ_expand t')
+        (T.string_of_typ_expand t);
     ve
 
 and check_pats env ts pats ve at : val_env =
@@ -874,7 +869,7 @@ and check_obj env s tfs id fields at : T.typ =
       if not (T.Env.mem name ve) then
         error env at "%s expression without field %s cannot produce expected type\n  %s"
           (if s = T.Actor then "actor" else "object") name
-          (T.string_of_typ_expand env.cons t);
+          (T.string_of_typ_expand t);
       T.Env.add name t ve
     ) pre_ve tfs
   in
@@ -928,16 +923,16 @@ and infer_exp_field env s (tfs, ve) field : T.field list * val_env =
             "%smutable field %s cannot produce expected %smutable field of type\n  %s"
             (if mut.it = Var then "" else "im") id.it
             (if T.is_mut t then "" else "im")
-            (T.string_of_typ_expand env.cons (T.as_immut t))
+            (T.string_of_typ_expand (T.as_immut t))
       end;
       t
   in
   if not env.pre then begin
     if s = T.Actor && priv.it = Public && not (is_func_exp exp) then
       error env field.at "public actor field is not a function";
-    if s <> T.Object T.Local && priv.it = Public && not (T.sub env.cons t T.Shared) then
+    if s <> T.Object T.Local && priv.it = Public && not (T.sub t T.Shared) then
       error env field.at "public shared object or actor field %s has non-shared type\n  %s"
-        (string_of_name name.it) (T.string_of_typ_expand env.cons t)
+        (string_of_name name.it) (T.string_of_typ_expand t)
   end;
   let ve' = T.Env.add id.it t ve in
   let tfs' =
@@ -1009,9 +1004,9 @@ and check_block env t decs at : scope =
 and check_block_exps env t decs at =
   match decs with
   | [] ->
-    if not (T.sub env.cons T.unit t) then
+    if not (T.sub T.unit t) then
       local_error env at "empty block cannot produce expected type\n  %s"
-        (T.string_of_typ_expand env.cons t)
+        (T.string_of_typ_expand t)
   | [dec] ->
     check_dec env t dec
   | dec::decs' ->
@@ -1049,35 +1044,24 @@ and check_dec env t dec =
   | _ ->
     let t' = infer_dec env dec in
     (* TBR: special-case unit? *)
-    if not (T.eq env.cons t T.unit || T.sub env.cons t' t) then
+    if not (T.eq t T.unit || T.sub t' t) then
       local_error env dec.at "expression of type\n  %s\ncannot produce expected type\n  %s"
-        (T.string_of_typ_expand env.cons t')
-        (T.string_of_typ_expand env.cons t)
-(*
-and print_ce =
-  Con.Env.iter (fun c k ->
-    Printf.printf "  type %s %s\n" (Con.to_string c) (Type.string_of_kind k)
-  )
-and print_ve =
-  Type.Env.iter (fun x t ->
-    Printf.printf "  %s : %s\n" x (Type.string_of_typ t)
-  )
-*)
-
+        (T.string_of_typ_expand t')
+        (T.string_of_typ_expand t)
 
 and infer_block_decs env decs : scope =
+  (* assert (not env.pre);? *)
   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 ce = infer_block_typdecs true env' decs in
   let env'' = adjoin env {scope with con_env = ce} in
-  let _ce' = infer_block_typdecs env'' decs in
+  let _ce' = infer_block_typdecs false 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}
 
-
 (* 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
@@ -1088,35 +1072,42 @@ and gather_dec_typdecs env scope dec : scope =
   | TypD (con_id, binds, _) | ClassD (_, con_id, binds, _, _, _, _) ->
     if T.Env.mem con_id.it scope.typ_env then
       error env dec.at "duplicate definition for type %s in block" con_id.it;
-    let cs =
-      List.map (fun (bind : typ_bind) -> Con.fresh bind.it.var.it) binds in
-    let pre_tbs = List.map (fun c -> {T.var = Con.name c; bound = T.Pre}) cs in
-    let c = Con.fresh con_id.it in
+    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 = T.fresh_con con_id.it pre_k in
     let ve' =
       match dec.it with
       | ClassD (id, _, _ , _, _, _, _) ->
+        let cs = List.map (fun (bind : typ_bind) -> T.fresh_con bind.it.var.it (T.Abs ([], T.Pre))) binds in
         let t2 = T.Con (c, List.map (fun c' -> T.Con (c', [])) cs) in
         T.Env.add id.it (T.Func (T.Local, T.Returns, pre_tbs, [T.Pre], [t2])) scope.val_env
       | _ -> scope.val_env in
     let te' = T.Env.add con_id.it c scope.typ_env in
-    let ce' = Con.Env.add c pre_k scope.con_env in
+    let ce' = T.ConSet.disjoint_add c scope.con_env in
     {val_env = ve'; typ_env = te'; con_env = ce'}
 
 
 (* Pass 2 and 3: infer type definitions *)
-and infer_block_typdecs env decs : con_env =
-  let _env', ce =
-    List.fold_left (fun (env, ce) dec ->
-      let ce' = infer_dec_typdecs env dec in
-      adjoin_cons env ce', Con.Env.adjoin ce ce'
-    ) (env, Con.Env.empty) decs
-  in ce
-
-and infer_dec_typdecs env dec : con_env =
+and infer_block_typdecs firstPass env decs : con_env =
+  List.fold_left
+    (fun ce dec ->
+      let ce' = infer_dec_typdecs firstPass env dec in
+      T.ConSet.disjoint_union ce ce'
+    )  T.ConSet.empty decs
+
+
+and infer_dec_typdecs firstPass env dec : con_env =
+  let set con_id c k =
+    if firstPass then
+      begin
+        T.set_kind c k;
+        con_id.note <- Some c
+      end
+    else assert (T.eq_kind (T.kind c) k)
+  in
   match dec.it with
   | ExpD _ | LetD _ | VarD _ | FuncD _ ->
-    Con.Env.empty
+    T.ConSet.empty
   | 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
@@ -1124,8 +1115,8 @@ and infer_dec_typdecs env dec : con_env =
     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
-    con_id.note <- Some (c, k);
-    Con.Env.singleton c k
+    set con_id c k;
+    T.ConSet.singleton c
   | ClassD (id, con_id, binds, sort, pat, self_id, fields) ->
     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
@@ -1135,8 +1126,8 @@ and infer_dec_typdecs env dec : con_env =
     let t = infer_obj (adjoin_vals env' ve) sort.it self_id (Some self_typ) fields 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
-    con_id.note <- Some (c, k);
-    Con.Env.singleton c k
+    set con_id c k;
+    T.ConSet.singleton c
 
 (* Pass 4: collect value identifiers *)
 and gather_block_valdecs env decs : val_env =
@@ -1179,19 +1170,19 @@ and infer_dec_valdecs env dec : val_env =
     let t1, _ = infer_pat {env' with pre = true} pat in
     let t2 = check_typ env' typ in
     if not env.pre && sort.it = T.Sharable then begin
-      if not (T.sub env'.cons t1 T.Shared) then
+      if not (T.sub t1 T.Shared) then
         error env pat.at "shared function has non-shared parameter type\n  %s"
-          (T.string_of_typ_expand env'.cons t1);
+          (T.string_of_typ_expand t1);
       begin match t2 with
       | T.Tup [] -> ()
       | T.Async t2 ->
-        if not (T.sub env'.cons t2 T.Shared) then
+        if not (T.sub t2 T.Shared) then
           error env typ.at "shared function has non-shared result type\n  %s"
-            (T.string_of_typ_expand env'.cons t2);
+            (T.string_of_typ_expand t2);
         if not (isAsyncE exp) then
           error env dec.at "shared function with async type has non-async body"
       | _ -> error env typ.at "shared function has non-async result type\n  %s"
-          (T.string_of_typ_expand env'.cons t2)
+          (T.string_of_typ_expand t2)
       end;
     end;
     let ts1 = match pat.it with TupP ps -> T.as_seq t1 | _ -> [t1] in
diff --git a/src/typing.mli b/src/typing.mli
index 35a71b49292..9da30ffeb89 100644
--- a/src/typing.mli
+++ b/src/typing.mli
@@ -2,7 +2,7 @@ open Type
 
 type val_env = typ Env.t
 type typ_env = con Env.t
-type con_env = Type.con_env
+type con_env = Type.con_set
 
 type scope =
   { val_env : val_env;