diff --git a/language/sail.ott b/language/sail.ott
index 85b2751cc..f30dcc23d 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -252,10 +252,11 @@ n_constraint :: 'NC_' ::=
   | nexp '<=' nexp'                  :: :: bounded_le
   | nexp '<' nexp'                   :: :: bounded_lt
   | nexp != nexp'                    :: :: not_equal
-  | kid 'IN' { num1 , ... , numn }   :: :: set
+  | nexp 'IN' { num1 , ... , numn }  :: :: set
   | n_constraint & n_constraint'     :: :: or
   | n_constraint | n_constraint'     :: :: and
   | id ( typ_arg0 , ... , typ_argn ) :: :: app
+  | id                               :: :: id
   | kid                              :: :: var
   | true                             :: :: true
   | false                            :: :: false
@@ -304,6 +305,8 @@ type_def_aux  :: 'TD_' ::=
     {{ com tagged union type definition}} {{ texlong }}
   | typedef id = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
     {{ com enumeration type definition}} {{ texlong }}
+  | typedef id : kind :: :: abstract
+    {{ com abstract type }}
   | bitfield id : typ = { id1 : index_range1 , ... , idn : index_rangen } :: :: bitfield
     {{ com register mutable bitfield type definition }} {{ texlong }}
 
@@ -746,6 +749,8 @@ def :: 'DEF_' ::=
   {{ aux _ def_annot }} {{ auxparam 'a }}
   | type_def                                           :: :: type
     {{ com type definition }}
+  | constraint n_constraint                            :: :: constraint
+    {{ com top-level constraint }}
   | fundef                                             :: :: fundef
     {{ com function definition }}
   | mapdef                                             :: :: mapdef
diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml
index 8fb96afdb..25fb7b67c 100644
--- a/src/lib/ast_util.ml
+++ b/src/lib/ast_util.ml
@@ -381,6 +381,13 @@ and nexp_simp_aux = function
 let rec constraint_simp (NC_aux (nc_aux, l)) =
   let nc_aux =
     match nc_aux with
+    | NC_set (nexp, ints) ->
+        let nexp = nexp_simp nexp in
+        begin
+          match nexp with
+          | Nexp_aux (Nexp_constant c, _) -> if List.exists (fun i -> Big_int.equal c i) ints then NC_true else NC_false
+          | _ -> NC_set (nexp, ints)
+        end
     | NC_equal (nexp1, nexp2) ->
         let nexp1, nexp2 = (nexp_simp nexp1, nexp_simp nexp2) in
         if nexp_identical nexp1 nexp2 then NC_true else NC_equal (nexp1, nexp2)
@@ -510,6 +517,7 @@ let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
 let nc_lt n1 n2 = NC_aux (NC_bounded_lt (n1, n2), Parse_ast.Unknown)
 let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
 let nc_gt n1 n2 = NC_aux (NC_bounded_gt (n1, n2), Parse_ast.Unknown)
+let nc_id id = mk_nc (NC_id id)
 let nc_var kid = mk_nc (NC_var kid)
 let nc_true = mk_nc NC_true
 let nc_false = mk_nc NC_false
@@ -796,6 +804,7 @@ and map_def_annot f (DEF_aux (aux, annot)) =
   let aux =
     match aux with
     | DEF_type td -> DEF_type (map_typedef_annot f td)
+    | DEF_constraint nc -> DEF_constraint nc
     | DEF_fundef fd -> DEF_fundef (map_fundef_annot f fd)
     | DEF_mapdef md -> DEF_mapdef (map_mapdef_annot f md)
     | DEF_outcome (outcome_spec, defs) -> DEF_outcome (outcome_spec, List.map (map_def_annot f) defs)
@@ -892,7 +901,7 @@ and string_of_n_constraint = function
   | NC_aux (NC_bounded_lt (n1, n2), _) -> string_of_nexp n1 ^ " < " ^ string_of_nexp n2
   | NC_aux (NC_or (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")"
   | NC_aux (NC_and (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
-  | NC_aux (NC_set (kid, ns), _) -> string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
+  | NC_aux (NC_set (n, ns), _) -> string_of_nexp n ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
   | NC_aux (NC_app (Id_aux (Operator op, _), [arg1; arg2]), _) ->
       "(" ^ string_of_typ_arg arg1 ^ " " ^ op ^ " " ^ string_of_typ_arg arg2 ^ ")"
   | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")"
@@ -1109,8 +1118,10 @@ let id_of_type_def_aux = function
   | TD_record (id, _, _, _)
   | TD_variant (id, _, _, _)
   | TD_enum (id, _, _)
+  | TD_abstract (id, _)
   | TD_bitfield (id, _, _) ->
       id
+
 let id_of_type_def (TD_aux (td_aux, _)) = id_of_type_def_aux td_aux
 
 let id_of_val_spec (VS_aux (VS_val_spec (_, id, _), _)) = id
@@ -1186,7 +1197,7 @@ let rec nc_compare (NC_aux (nc1, _)) (NC_aux (nc2, _)) =
   | NC_bounded_lt (n1, n2), NC_bounded_lt (n3, n4)
   | NC_not_equal (n1, n2), NC_not_equal (n3, n4) ->
       lex_ord Nexp.compare Nexp.compare n1 n3 n2 n4
-  | NC_set (k1, s1), NC_set (k2, s2) -> lex_ord Kid.compare (Util.compare_list Nat_big_num.compare) k1 k2 s1 s2
+  | NC_set (n1, s1), NC_set (n2, s2) -> lex_ord Nexp.compare (Util.compare_list Nat_big_num.compare) n1 n2 s1 s2
   | NC_or (nc1, nc2), NC_or (nc3, nc4) | NC_and (nc1, nc2), NC_and (nc3, nc4) ->
       lex_ord nc_compare nc_compare nc1 nc3 nc2 nc4
   | NC_app (f1, args1), NC_app (f2, args2) -> lex_ord Id.compare (Util.compare_list typ_arg_compare) f1 f2 args1 args2
@@ -1383,7 +1394,7 @@ let rec kopts_of_constraint (NC_aux (nc, _)) =
   | NC_bounded_lt (nexp1, nexp2)
   | NC_not_equal (nexp1, nexp2) ->
       KOptSet.union (kopts_of_nexp nexp1) (kopts_of_nexp nexp2)
-  | NC_set (kid, _) -> KOptSet.singleton (mk_kopt K_int kid)
+  | NC_set (nexp, _) -> kopts_of_nexp nexp
   | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> KOptSet.union (kopts_of_constraint nc1) (kopts_of_constraint nc2)
   | NC_app (_, args) -> List.fold_left (fun s t -> KOptSet.union s (kopts_of_typ_arg t)) KOptSet.empty args
   | NC_var kid -> KOptSet.singleton (mk_kopt K_bool kid)
@@ -1428,7 +1439,7 @@ let rec tyvars_of_constraint (NC_aux (nc, _)) =
   | NC_bounded_lt (nexp1, nexp2)
   | NC_not_equal (nexp1, nexp2) ->
       KidSet.union (tyvars_of_nexp nexp1) (tyvars_of_nexp nexp2)
-  | NC_set (kid, _) -> KidSet.singleton kid
+  | NC_set (nexp, _) -> tyvars_of_nexp nexp
   | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> KidSet.union (tyvars_of_constraint nc1) (tyvars_of_constraint nc2)
   | NC_app (_, args) -> List.fold_left (fun s t -> KidSet.union s (tyvars_of_typ_arg t)) KidSet.empty args
   | NC_var kid -> KidSet.singleton kid
@@ -1706,7 +1717,7 @@ let rec locate_nc f (NC_aux (nc_aux, l)) =
     | NC_bounded_le (nexp1, nexp2) -> NC_bounded_le (locate_nexp f nexp1, locate_nexp f nexp2)
     | NC_bounded_lt (nexp1, nexp2) -> NC_bounded_lt (locate_nexp f nexp1, locate_nexp f nexp2)
     | NC_not_equal (nexp1, nexp2) -> NC_not_equal (locate_nexp f nexp1, locate_nexp f nexp2)
-    | NC_set (kid, nums) -> NC_set (locate_kid f kid, nums)
+    | NC_set (nexp, nums) -> NC_set (locate_nexp f nexp, nums)
     | NC_or (nc1, nc2) -> NC_or (locate_nc f nc1, locate_nc f nc2)
     | NC_and (nc1, nc2) -> NC_and (locate_nc f nc1, locate_nc f nc2)
     | NC_true -> NC_true
@@ -1906,12 +1917,7 @@ and constraint_subst_aux l sv subst = function
   | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2)
   | NC_bounded_lt (n1, n2) -> NC_bounded_lt (nexp_subst sv subst n1, nexp_subst sv subst n2)
   | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
-  | NC_set (kid, ints) as set_nc -> begin
-      match subst with
-      | A_aux (A_nexp (Nexp_aux (Nexp_var kid', _)), _) when Kid.compare kid sv = 0 -> NC_set (kid', ints)
-      | A_aux (A_nexp n, _) when Kid.compare kid sv = 0 -> nexp_set_to_or l n ints
-      | _ -> set_nc
-    end
+  | NC_set (n, ints) -> NC_set (nexp_subst sv subst n, ints)
   | NC_or (nc1, nc2) -> NC_or (constraint_subst sv subst nc1, constraint_subst sv subst nc2)
   | NC_and (nc1, nc2) -> NC_and (constraint_subst sv subst nc1, constraint_subst sv subst nc2)
   | NC_app (id, args) -> NC_app (id, List.map (typ_arg_subst sv subst) args)
@@ -1995,19 +2001,7 @@ let subst_kids_nc, subst_kids_typ, subst_kids_typ_arg =
     | NC_bounded_le (n1, n2) -> re (NC_bounded_le (snexp n1, snexp n2))
     | NC_bounded_lt (n1, n2) -> re (NC_bounded_lt (snexp n1, snexp n2))
     | NC_not_equal (n1, n2) -> re (NC_not_equal (snexp n1, snexp n2))
-    | NC_set (kid, is) -> begin
-        match KBindings.find kid substs with
-        | Nexp_aux (Nexp_constant i, _) ->
-            if List.exists (fun j -> Big_int.equal i j) is then re NC_true else re NC_false
-        | nexp -> begin
-            match List.rev is with
-            | i :: is ->
-                let equal_num i = re (NC_equal (nexp, nconstant i)) in
-                List.fold_left (fun nc i -> re (NC_or (equal_num i, nc))) (equal_num i) is
-            | [] -> re NC_false
-          end
-        | exception Not_found -> n_constraint
-      end
+    | NC_set (n, ints) -> re (NC_set (snexp n, ints))
     | NC_or (nc1, nc2) -> re (NC_or (snc nc1, snc nc2))
     | NC_and (nc1, nc2) -> re (NC_and (snc nc1, snc nc2))
     | NC_true | NC_false -> n_constraint
diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli
index 5748e8c85..606544450 100644
--- a/src/lib/ast_util.mli
+++ b/src/lib/ast_util.mli
@@ -289,8 +289,9 @@ val nc_or : n_constraint -> n_constraint -> n_constraint
 val nc_not : n_constraint -> n_constraint
 val nc_true : n_constraint
 val nc_false : n_constraint
-val nc_set : kid -> Big_int.num list -> n_constraint
-val nc_int_set : kid -> int list -> n_constraint
+val nc_set : nexp -> Big_int.num list -> n_constraint
+val nc_int_set : nexp -> int list -> n_constraint
+val nc_id : id -> n_constraint
 val nc_var : kid -> n_constraint
 
 (** {2 Functions for building type arguments}*)
@@ -454,6 +455,7 @@ val string_of_index_range : index_range -> string
 
 val id_of_fundef : 'a fundef -> id
 val id_of_mapdef : 'a mapdef -> id
+val id_of_type_def_aux : type_def_aux -> id
 val id_of_type_def : 'a type_def -> id
 val id_of_val_spec : 'a val_spec -> id
 val id_of_dec_spec : 'a dec_spec -> id
diff --git a/src/lib/callgraph.ml b/src/lib/callgraph.ml
index 5369bcd67..f78f8442f 100644
--- a/src/lib/callgraph.ml
+++ b/src/lib/callgraph.ml
@@ -278,6 +278,7 @@ let add_def_to_graph graph (DEF_aux (def, _)) =
         scan_typquant (Type id) typq
     | TD_enum (id, ctors, _) ->
         List.iter (fun ctor_id -> graph := G.add_edge (Constructor ctor_id) (Type id) !graph) ctors
+    | TD_abstract (id, _) -> graph := G.add_edges (Type id) [] !graph
     | TD_bitfield (id, typ, ranges) ->
         graph := G.add_edges (Type id) (List.map (fun id -> Type id) (IdSet.elements (typ_ids typ))) !graph
   in
@@ -378,14 +379,6 @@ let rec graph_of_defs defs =
 
 let graph_of_ast ast = graph_of_defs ast.defs
 
-let id_of_typedef (TD_aux (aux, _)) =
-  match aux with
-  | TD_abbrev (id, _, _) -> id
-  | TD_record (id, _, _, _) -> id
-  | TD_variant (id, _, _, _) -> id
-  | TD_enum (id, _, _) -> id
-  | TD_bitfield (id, _, _) -> id
-
 let id_of_reg_dec (DEC_aux (DEC_reg (_, id, _), _)) = id
 
 let id_of_funcl (FCL_aux (FCL_funcl (id, _), _)) = id
@@ -426,7 +419,7 @@ let filter_ast_extra cuts g ast keep_std =
         let ids = pat_ids pat |> IdSet.elements in
         if List.exists (fun id -> NM.mem (Letbind id) g) ids then DEF_aux (DEF_let lb, def_annot) :: filter_ast' g defs
         else filter_ast' g defs
-    | DEF_aux (DEF_type tdef, def_annot) :: defs when NM.mem (Type (id_of_typedef tdef)) g ->
+    | DEF_aux (DEF_type tdef, def_annot) :: defs when NM.mem (Type (id_of_type_def tdef)) g ->
         DEF_aux (DEF_type tdef, def_annot) :: filter_ast' g defs
     | DEF_aux (DEF_type _, _) :: defs -> filter_ast' g defs
     | DEF_aux (DEF_measure (id, _, _), _) :: defs when NS.mem (Function id) cuts -> filter_ast' g defs
diff --git a/src/lib/constant_propagation.ml b/src/lib/constant_propagation.ml
index e488a78cf..0bd283dab 100644
--- a/src/lib/constant_propagation.ml
+++ b/src/lib/constant_propagation.ml
@@ -144,7 +144,7 @@ let lit_match = function
 let fabricate_nexp_exist env l typ kids nc typ' =
   match (kids, nc, Env.expand_synonyms env typ') with
   | ( [kid],
-      NC_aux (NC_set (kid', i :: _), _),
+      NC_aux (NC_set (Nexp_aux (Nexp_var kid', _), i :: _), _),
       Typ_aux (Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var kid'', _)), _)]), _) )
     when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 ->
       Nexp_aux (Nexp_constant i, Unknown)
@@ -154,7 +154,7 @@ let fabricate_nexp_exist env l typ kids nc typ' =
     when Kid.compare kid kid'' = 0 ->
       nint 32
   | ( [kid],
-      NC_aux (NC_set (kid', i :: _), _),
+      NC_aux (NC_set (Nexp_aux (Nexp_var kid', _), i :: _), _),
       Typ_aux
         ( Typ_app
             ( Id_aux (Id "range", _),
diff --git a/src/lib/constraint.ml b/src/lib/constraint.ml
index fe3586f89..e21458324 100644
--- a/src/lib/constraint.ml
+++ b/src/lib/constraint.ml
@@ -168,9 +168,9 @@ let rec add_list buf sep add_elem = function
 let smt_type l = function
   | K_int -> Atom "Int"
   | K_bool -> Atom "Bool"
-  | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kinded variable to SMT solver")
+  | K_type -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type kinded variable to SMT solver")
 
-let to_smt l vars constr =
+let to_smt l abstract vars constr =
   (* Numbering all SMT variables v0, ... vn, rather than generating
      names based on their Sail names (e.g. using zencode) ensures that
      alpha-equivalent constraints generate the same SMT problem, which
@@ -189,10 +189,20 @@ let to_smt l vars constr =
 
   let exponentials = ref [] in
 
+  let abstract_decs =
+    abstract |> Bindings.bindings
+    |> List.filter_map (fun (id, kind) ->
+           match kind with
+           | K_aux (K_type, _) -> None
+           | _ ->
+               Some (sfun "declare-const" [Atom (Util.zencode_string (string_of_id id)); smt_type l (unaux_kind kind)])
+       )
+  in
+
   (* var_decs outputs the list of variables to be used by the SMT
      solver in SMTLIB v2.0 format. It takes a kind_aux KBindings, as
      returned by Type_check.get_typ_vars *)
-  let var_decs l (vars : kind_aux KBindings.t) : sexpr list =
+  let var_decs (vars : kind_aux KBindings.t) : sexpr list =
     vars |> KBindings.bindings |> List.map (fun (v, k) -> sfun "declare-const" [fst (smt_var v); smt_type l k])
   in
   let rec smt_nexp (Nexp_aux (aux, _) : nexp) : sexpr =
@@ -229,7 +239,7 @@ let to_smt l vars constr =
     | NC_bounded_ge (nexp1, nexp2) -> sfun ">=" [smt_nexp nexp1; smt_nexp nexp2]
     | NC_bounded_gt (nexp1, nexp2) -> sfun ">" [smt_nexp nexp1; smt_nexp nexp2]
     | NC_not_equal (nexp1, nexp2) -> sfun "not" [sfun "=" [smt_nexp nexp1; smt_nexp nexp2]]
-    | NC_set (v, ints) -> sfun "or" (List.map (fun i -> sfun "=" [fst (smt_var v); Atom (Big_int.to_string i)]) ints)
+    | NC_set (nexp, ints) -> sfun "or" (List.map (fun i -> sfun "=" [smt_nexp nexp; Atom (Big_int.to_string i)]) ints)
     | NC_or (nc1, nc2) -> sfun "or" [smt_constraint nc1; smt_constraint nc2]
     | NC_and (nc1, nc2) -> sfun "and" [smt_constraint nc1; smt_constraint nc2]
     | NC_app (id, args) -> sfun (string_of_id id) (List.map smt_typ_arg args)
@@ -243,18 +253,19 @@ let to_smt l vars constr =
     | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function")
   in
   let smt_constr = smt_constraint constr in
-  (var_decs l vars, smt_constr, smt_var, !exponentials)
+  (abstract_decs @ var_decs vars, smt_constr, smt_var, !exponentials)
 
 let sailexp_concrete n =
   List.init (n + 1) (fun i ->
       sfun "=" [sfun "sailexp" [Atom (string_of_int i)]; Atom (Big_int.to_string (Big_int.pow_int_positive 2 i))]
   )
 
-let smtlib_of_constraints ?(get_model = false) l vars extra constr : string * (kid -> sexpr * bool) * sexpr list =
+let smtlib_of_constraints ?(get_model = false) l abstract vars extra constr :
+    string * (kid -> sexpr * bool) * sexpr list =
   let open Buffer in
   let buf = create 512 in
   add_string buf !opt_solver.header;
-  let variables, problem, var_map, exponentials = to_smt l vars constr in
+  let variables, problem, var_map, exponentials = to_smt l abstract vars constr in
   add_list buf '\n' add_sexpr variables;
   add_char buf '\n';
   if !opt_solver.uninterpret_power then add_string buf "(declare-fun sailexp (Int) Int)\n";
@@ -326,7 +337,7 @@ let constraint_to_smt l constr =
     kopts_of_constraint constr |> KOptSet.elements |> List.map kopt_pair
     |> List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty
   in
-  let vars, sexpr, var_map, exponentials = to_smt l vars constr in
+  let vars, sexpr, var_map, exponentials = to_smt l Bindings.empty vars constr in
   let vars = string_of_list "\n" pp_sexpr vars in
   ( vars ^ "\n(assert " ^ pp_sexpr sexpr ^ ")",
     (fun v ->
@@ -336,13 +347,13 @@ let constraint_to_smt l constr =
     List.map pp_sexpr exponentials
   )
 
-let rec call_smt' l extra constraints =
+let rec call_smt' l abstract extra constraints =
   let vars =
     kopts_of_constraint constraints |> KOptSet.elements |> List.map kopt_pair
     |> List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty
   in
   let problems = [constraints] in
-  let smt_file, _, exponentials = smtlib_of_constraints l vars extra constraints in
+  let smt_file, _, exponentials = smtlib_of_constraints l abstract vars extra constraints in
 
   if !opt_smt_verbose then prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" smt_file);
 
@@ -418,7 +429,7 @@ let rec call_smt' l extra constraints =
            then try replacing `2^` with an uninterpreted function to see
            if the problem would be unsat in that case. *)
         opt_solver := { !opt_solver with uninterpret_power = true };
-        let result = call_smt_uninterpret_power ~bound:64 l constraints in
+        let result = call_smt_uninterpret_power ~bound:64 l abstract constraints in
         opt_solver := { !opt_solver with uninterpret_power = false };
         result
     | Unknown -> Unknown
@@ -426,31 +437,31 @@ let rec call_smt' l extra constraints =
     exponentials
   )
 
-and call_smt_uninterpret_power ~bound l constraints =
-  match call_smt' l (sailexp_concrete bound) constraints with
+and call_smt_uninterpret_power ~bound l abstract constraints =
+  match call_smt' l abstract (sailexp_concrete bound) constraints with
   | Unsat, _ -> Unsat
   | Sat, exponentials -> begin
-      match call_smt' l (sailexp_concrete bound @ List.map bound_exponential exponentials) constraints with
+      match call_smt' l abstract (sailexp_concrete bound @ List.map bound_exponential exponentials) constraints with
       | Sat, _ -> Sat
       | _ -> Unknown
     end
   | _ -> Unknown
 
-let call_smt l constraints =
+let call_smt l abstract constraints =
   let t = Profile.start_smt () in
   let result =
-    if !opt_solver.uninterpret_power then call_smt_uninterpret_power ~bound:64 l constraints
-    else fst (call_smt' l [] constraints)
+    if !opt_solver.uninterpret_power then call_smt_uninterpret_power ~bound:64 l abstract constraints
+    else fst (call_smt' l abstract [] constraints)
   in
   Profile.finish_smt t;
   result
 
-let solve_smt_file l extra constraints =
+let solve_smt_file l abstract extra constraints =
   let vars =
     kopts_of_constraint constraints |> KOptSet.elements |> List.map kopt_pair
     |> List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty
   in
-  smtlib_of_constraints ~get_model:true l vars extra constraints
+  smtlib_of_constraints ~get_model:true l abstract vars extra constraints
 
 let call_smt_solve l smt_file smt_vars var =
   let smt_var = pp_sexpr (fst (smt_vars var)) in
@@ -539,23 +550,23 @@ let call_smt_solve_bitvector l smt_file smt_vars =
     smt_vars
   |> Util.option_all
 
-let solve_smt l constraints var =
-  let smt_file, smt_vars, _ = solve_smt_file l [] constraints in
+let solve_smt l abstract constraints var =
+  let smt_file, smt_vars, _ = solve_smt_file l abstract [] constraints in
   call_smt_solve l smt_file smt_vars var
 
-let solve_all_smt l constraints var =
+let solve_all_smt l abstract constraints var =
   let rec aux results =
     let constraints = List.fold_left (fun ncs r -> nc_and ncs (nc_neq (nconstant r) (nvar var))) constraints results in
-    match solve_smt l constraints var with
+    match solve_smt l abstract constraints var with
     | Some result -> aux (result :: results)
     | None -> (
-        match call_smt l constraints with Unsat -> Some results | _ -> None
+        match call_smt l abstract constraints with Unsat -> Some results | _ -> None
       )
   in
   aux []
 
-let solve_unique_smt' l constraints exp_defn exp_bound var =
-  let smt_file, smt_vars, exponentials = solve_smt_file l (exp_defn @ exp_bound) constraints in
+let solve_unique_smt' l abstract constraints exp_defn exp_bound var =
+  let smt_file, smt_vars, exponentials = solve_smt_file l abstract (exp_defn @ exp_bound) constraints in
   let digest = Digest.string (smt_file ^ pp_sexpr (fst (smt_vars var))) in
   let result =
     match DigestMap.find_opt digest !known_uniques with
@@ -565,7 +576,9 @@ let solve_unique_smt' l constraints exp_defn exp_bound var =
         match call_smt_solve l smt_file smt_vars var with
         | Some result ->
             let t = Profile.start_smt () in
-            let smt_result' = fst (call_smt' l exp_defn (nc_and constraints (nc_neq (nconstant result) (nvar var)))) in
+            let smt_result' =
+              fst (call_smt' l abstract exp_defn (nc_and constraints (nc_neq (nconstant result) (nvar var))))
+            in
             Profile.finish_smt t;
             begin
               match smt_result' with
@@ -588,17 +601,17 @@ let solve_unique_smt' l constraints exp_defn exp_bound var =
 (* Follows the same approach as call_smt' for unknown results due to
    exponentials, retrying with a bounded spec. *)
 
-let solve_unique_smt l constraints var =
+let solve_unique_smt l abstract constraints var =
   let t = Profile.start_smt () in
   let result =
-    match solve_unique_smt' l constraints [] [] var with
+    match solve_unique_smt' l abstract constraints [] [] var with
     | Some result, _ -> Some result
     | None, [] -> None
     | None, exponentials ->
         opt_solver := { !opt_solver with uninterpret_power = true };
         let sailexp = sailexp_concrete 64 in
         let exp_bound = List.map bound_exponential exponentials in
-        let result, _ = solve_unique_smt' l constraints sailexp exp_bound var in
+        let result, _ = solve_unique_smt' l abstract constraints sailexp exp_bound var in
         opt_solver := { !opt_solver with uninterpret_power = false };
         result
   in
diff --git a/src/lib/constraint.mli b/src/lib/constraint.mli
index 333e1c0a9..de2cbc501 100644
--- a/src/lib/constraint.mli
+++ b/src/lib/constraint.mli
@@ -83,12 +83,12 @@ val save_digests : unit -> unit
 
 val constraint_to_smt : l -> n_constraint -> string * (kid -> string * bool) * string list
 
-val call_smt : l -> n_constraint -> smt_result
+val call_smt : l -> kind Bindings.t -> n_constraint -> smt_result
 
 val call_smt_solve_bitvector : l -> string -> (int * string) list -> (int * lit) list option
 
-val solve_smt : l -> n_constraint -> kid -> Big_int.num option
+val solve_smt : l -> kind Bindings.t -> n_constraint -> kid -> Big_int.num option
 
-val solve_all_smt : l -> n_constraint -> kid -> Big_int.num list option
+val solve_all_smt : l -> kind Bindings.t -> n_constraint -> kid -> Big_int.num list option
 
-val solve_unique_smt : l -> n_constraint -> kid -> Big_int.num option
+val solve_unique_smt : l -> kind Bindings.t -> n_constraint -> kid -> Big_int.num option
diff --git a/src/lib/effects.ml b/src/lib/effects.ml
index 9306cc0d5..f845c8610 100644
--- a/src/lib/effects.ml
+++ b/src/lib/effects.ml
@@ -263,6 +263,7 @@ let infer_mapdef_extra_direct_effects def =
 let can_have_direct_side_effect (DEF_aux (aux, _)) =
   match aux with
   | DEF_type _ -> false
+  | DEF_constraint _ -> false
   | DEF_fundef _ -> true
   | DEF_mapdef _ -> false
   | DEF_impl _ -> true
diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml
index 96860ac73..9cca80fbb 100644
--- a/src/lib/initial_check.ml
+++ b/src/lib/initial_check.ml
@@ -335,7 +335,7 @@ let rec to_ast_typ ctx atyp =
   | P.ATyp_bidir (typ1, typ2, _) -> Typ_aux (Typ_bidir (to_ast_typ ctx typ1, to_ast_typ ctx typ2), l)
   | P.ATyp_nset nums ->
       let n = Kid_aux (Var "'n", gen_loc l) in
-      Typ_aux (Typ_exist ([mk_kopt ~loc:l K_int n], nc_set n nums, atom_typ (nvar n)), l)
+      Typ_aux (Typ_exist ([mk_kopt ~loc:l K_int n], nc_set (nvar n) nums, atom_typ (nvar n)), l)
   | P.ATyp_tuple typs -> Typ_aux (Typ_tuple (List.map (to_ast_typ ctx) typs), l)
   | P.ATyp_app (P.Id_aux (P.Id "int", il), [n]) ->
       Typ_aux (Typ_app (Id_aux (Id "atom", il), [to_ast_typ_arg ctx n K_int]), l)
@@ -477,7 +477,7 @@ and to_ast_constraint ctx atyp =
         | P.ATyp_var v -> NC_var (to_ast_var v)
         | P.ATyp_lit (P.L_aux (P.L_true, _)) -> NC_true
         | P.ATyp_lit (P.L_aux (P.L_false, _)) -> NC_false
-        | P.ATyp_in (P.ATyp_aux (P.ATyp_var v, _), P.ATyp_aux (P.ATyp_nset bounds, _)) -> NC_set (to_ast_var v, bounds)
+        | P.ATyp_in (n, P.ATyp_aux (P.ATyp_nset bounds, _)) -> NC_set (to_ast_nexp ctx n, bounds)
         | _ -> raise (Reporting.err_typ l "Invalid constraint")
       in
       NC_aux (aux, l)
@@ -1048,6 +1048,16 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : uannot d
       ( fns @ [DEF_aux (DEF_type (TD_aux (TD_enum (id, enums, false), (l, empty_uannot))), def_annot)],
         { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
       )
+  | P.TD_abstract (id, kind) ->
+      let id = to_ast_reserved_type_id ctx id in
+      begin
+        match to_ast_kind kind with
+        | Some kind ->
+            ( [DEF_aux (DEF_type (TD_aux (TD_abstract (id, kind), (l, empty_uannot))), def_annot)],
+              { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
+            )
+        | None -> raise (Reporting.err_general l "Abstract type cannot have Order kind")
+      end
   | P.TD_bitfield (id, typ, ranges) ->
       let id = to_ast_reserved_type_id ctx id in
       let typ = to_ast_typ ctx typ in
@@ -1316,6 +1326,9 @@ let rec to_ast_def doc attrs ctx (P.DEF_aux (def, l)) : uannot def list ctx_out
   | P.DEF_register dec ->
       let d = to_ast_dec ctx dec in
       ([DEF_aux (DEF_register d, annot)], ctx)
+  | P.DEF_constraint nc ->
+      let nc = to_ast_constraint ctx nc in
+      ([DEF_aux (DEF_constraint nc, annot)], ctx)
   | P.DEF_pragma (pragma, arg, ltrim) ->
       let l = pragma_arg_loc pragma ltrim l in
       begin
diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml
index f05594ed8..f120976e2 100644
--- a/src/lib/monomorphise.ml
+++ b/src/lib/monomorphise.ml
@@ -203,7 +203,7 @@ let extract_set_nc env l var nc =
   let rec aux expanded (NC_aux (nc, l) as nc_full) =
     let re nc = NC_aux (nc, l) in
     match nc with
-    | NC_set (id, is) when KidSet.mem id vars -> Some (is, re NC_true)
+    | NC_set (Nexp_aux (Nexp_var id, _), is) when KidSet.mem id vars -> Some (is, re NC_true)
     | NC_equal (Nexp_aux (Nexp_var id, _), Nexp_aux (Nexp_constant n, _)) when KidSet.mem id vars ->
         Some ([n], re NC_true)
     (* Turn (i <= 'v & 'v <= j & ...) into set constraint ('v in {i..j}) *)
@@ -2000,11 +2000,7 @@ module Analysis = struct
     | NC_bounded_lt (nexp1, nexp2)
     | NC_not_equal (nexp1, nexp2) ->
         dmerge (deps_of_nexp l kid_deps [] nexp1) (deps_of_nexp l kid_deps [] nexp2)
-    | NC_set (kid, _) -> (
-        match KBindings.find kid kid_deps with
-        | deps -> deps
-        | exception Not_found -> Unknown (l, "Unknown type variable in constraint " ^ string_of_kid kid)
-      )
+    | NC_set (nexp, _) -> deps_of_nexp l kid_deps [] nexp
     | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> dmerge (deps_of_nc kid_deps nc1) (deps_of_nc kid_deps nc2)
     | NC_true | NC_false -> dempty
     | NC_app (Id_aux (Id "mod", _), [A_aux (A_nexp nexp1, _); A_aux (A_nexp nexp2, _)]) ->
@@ -2362,7 +2358,7 @@ module Analysis = struct
                 let l' = Generated l in
                 let split =
                   match typ_of e1 with
-                  | Typ_aux (Typ_exist ([kdid], NC_aux (NC_set (kid, sizes), _), typ), _)
+                  | Typ_aux (Typ_exist ([kdid], NC_aux (NC_set (Nexp_aux (Nexp_var kid, _), sizes), _), typ), _)
                     when Kid.compare (kopt_kid kdid) kid == 0 -> begin
                       match Type_check.destruct_atom_nexp (env_of e1) typ with
                       | Some nexp when Nexp.compare (nvar kid) nexp == 0 ->
@@ -2377,7 +2373,11 @@ module Analysis = struct
                       begin
                         match
                           Util.find_map
-                            (function NC_aux (NC_set (kid'', is), _) when KidSet.mem kid'' vars -> Some is | _ -> None)
+                            (function
+                              | NC_aux (NC_set (Nexp_aux (Nexp_var kid'', _), is), _) when KidSet.mem kid'' vars ->
+                                  Some is
+                              | _ -> None
+                              )
                             constraints
                         with
                         | Some sizes ->
@@ -2711,7 +2711,7 @@ module Analysis = struct
     let rec sets_from_nc (NC_aux (nc, l) as nc_full) =
       match nc with
       | NC_and (nc1, nc2) -> merge_set_asserts_by_kid (sets_from_nc nc1) (sets_from_nc nc2)
-      | NC_set (kid, is) -> KBindings.singleton kid (l, is)
+      | NC_set (Nexp_aux (Nexp_var kid, _), is) -> KBindings.singleton kid (l, is)
       | NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant n, _)) -> KBindings.singleton kid (l, [n])
       | NC_or _ -> (
           match set_from_nc_or nc_full with
diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml
index d53bb5037..d721b0024 100644
--- a/src/lib/parse_ast.ml
+++ b/src/lib/parse_ast.ml
@@ -383,6 +383,7 @@ type type_def_aux =
   | TD_record of id * typquant * (atyp * id) list (* struct type definition *)
   | TD_variant of id * typquant * type_union list (* union type definition *)
   | TD_enum of id * (id * atyp) list * (id * exp option) list (* enumeration type definition *)
+  | TD_abstract of id * kind
   | TD_bitfield of id * atyp * (id * index_range) list (* register mutable bitfield type definition *)
 
 type val_spec_aux = (* Value type specification *)
@@ -425,6 +426,7 @@ type fixity_token = prec * Big_int.num * string
 type def_aux =
   (* Top-level definition *)
   | DEF_type of type_def (* type definition *)
+  | DEF_constraint of atyp (* global constraint *)
   | DEF_fundef of fundef (* function definition *)
   | DEF_mapdef of mapdef (* mapping definition *)
   | DEF_impl of funcl (* impl definition *)
diff --git a/src/lib/parser.mly b/src/lib/parser.mly
index d95864af2..e85757c9f 100644
--- a/src/lib/parser.mly
+++ b/src/lib/parser.mly
@@ -991,6 +991,8 @@ type_def:
     { mk_td (TD_abbrev ($2, $3, $5, $7)) $startpos $endpos }
   | Typedef id Colon kind Eq typ
     { mk_td (TD_abbrev ($2, mk_typqn, $4, $6)) $startpos $endpos }
+  | Typedef id Colon kind
+    { mk_td (TD_abstract ($2, $4)) $startpos $endpos }
   | Struct id Eq Lcurly struct_fields Rcurly
     { mk_td (TD_record ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5)) $startpos $endpos }
   | Struct id typaram Eq Lcurly struct_fields Rcurly
@@ -1330,6 +1332,8 @@ def_aux:
     { DEF_scattered $1 }
   | default_def
     { DEF_default $1 }
+  | Constraint typ
+    { DEF_constraint $2 }
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
   | Pragma
diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml
index 056533ee5..a995103eb 100644
--- a/src/lib/pretty_print_sail.ml
+++ b/src/lib/pretty_print_sail.ml
@@ -151,8 +151,8 @@ let rec doc_nc nc =
     | NC_bounded_gt (n1, n2) -> nc_op ">" n1 n2
     | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
     | NC_bounded_lt (n1, n2) -> nc_op "<" n1 n2
-    | NC_set (kid, ints) ->
-        separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
+    | NC_set (nexp, ints) ->
+        separate space [doc_nexp nexp; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
     | NC_app (id, args) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_typ_arg args)
     | NC_var kid -> doc_kid kid
     | NC_or _ | NC_and _ -> nc0 ~parenthesize:true nc
@@ -196,7 +196,7 @@ and doc_typ ?(simple = false) (Typ_aux (typ_aux, l)) =
   (* Resugar set types like {|1, 2, 3|} *)
   | Typ_exist
       ( [kopt],
-        NC_aux (NC_set (kid1, ints), _),
+        NC_aux (NC_set (Nexp_aux (Nexp_var kid1, _), ints), _),
         Typ_aux (Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var kid2, _)), _)]), _)
       )
     when Kid.compare (kopt_kid kopt) kid1 == 0 && Kid.compare kid1 kid2 == 0 && Id.compare (mk_id "atom") id == 0 ->
diff --git a/src/lib/rewriter.ml b/src/lib/rewriter.ml
index 01f872bc1..8b6b5ab3d 100644
--- a/src/lib/rewriter.ml
+++ b/src/lib/rewriter.ml
@@ -295,8 +295,8 @@ let rec rewrite_def rewriters (DEF_aux (aux, def_annot)) =
     match aux with
     | DEF_register (DEC_aux (DEC_reg (typ, id, Some exp), annot)) ->
         DEF_register (DEC_aux (DEC_reg (typ, id, Some (rewriters.rewrite_exp rewriters exp)), annot))
-    | DEF_type _ | DEF_mapdef _ | DEF_val _ | DEF_default _ | DEF_register _ | DEF_overload _ | DEF_fixity _
-    | DEF_instantiation _ ->
+    | DEF_type _ | DEF_constraint _ | DEF_mapdef _ | DEF_val _ | DEF_default _ | DEF_register _ | DEF_overload _
+    | DEF_fixity _ | DEF_instantiation _ ->
         aux
     | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
     | DEF_impl funcl -> DEF_impl (rewrite_funcl rewriters funcl)
diff --git a/src/lib/spec_analysis.ml b/src/lib/spec_analysis.ml
index 6bd7d4acd..dc2ffcd8a 100644
--- a/src/lib/spec_analysis.ml
+++ b/src/lib/spec_analysis.ml
@@ -160,8 +160,9 @@ and fv_of_nconstraint consider_var bound used (Ast.NC_aux (nc, _)) =
   | NC_bounded_lt (n1, n2)
   | NC_not_equal (n1, n2) ->
       fv_of_nexp consider_var bound (fv_of_nexp consider_var bound used n1) n2
-  | NC_set (Ast.Kid_aux (Ast.Var i, _), _) | NC_var (Ast.Kid_aux (Ast.Var i, _)) ->
+  | NC_var (Ast.Kid_aux (Ast.Var i, _)) ->
       if consider_var then conditional_add_typ bound used (Ast.Id_aux (Ast.Id i, Parse_ast.Unknown)) else used
+  | NC_set (n, _) -> fv_of_nexp consider_var bound used n
   | NC_or (nc1, nc2) | NC_and (nc1, nc2) ->
       fv_of_nconstraint consider_var bound (fv_of_nconstraint consider_var bound used nc1) nc2
   | NC_app (id, targs) ->
diff --git a/src/lib/specialize.ml b/src/lib/specialize.ml
index 5be9f512b..b1c03db05 100644
--- a/src/lib/specialize.ml
+++ b/src/lib/specialize.ml
@@ -205,8 +205,7 @@ let string_of_instantiation instantiation =
     | NC_aux (NC_bounded_lt (n1, n2), _) -> string_of_nexp n1 ^ " < " ^ string_of_nexp n2
     | NC_aux (NC_or (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")"
     | NC_aux (NC_and (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
-    | NC_aux (NC_set (kid, ns), _) ->
-        kid_name (mk_kopt K_int kid) ^ " in {" ^ Util.string_of_list ", " Big_int.to_string ns ^ "}"
+    | NC_aux (NC_set (n, ns), _) -> string_of_nexp n ^ " in {" ^ Util.string_of_list ", " Big_int.to_string ns ^ "}"
     | NC_aux (NC_true, _) -> "true"
     | NC_aux (NC_false, _) -> "false"
     | NC_aux (NC_var kid, _) -> kid_name (mk_kopt K_bool kid)
diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml
index 06f02d5a9..57556ea41 100644
--- a/src/lib/type_check.ml
+++ b/src/lib/type_check.ml
@@ -406,8 +406,8 @@ and simp_typ_aux = function
    which is then a problem we can feed to the constraint solver expecting unsat.
 *)
 
-let prove_smt ~assumptions:ncs (NC_aux (_, l) as nc) =
-  match Constraint.call_smt l (List.fold_left nc_and (nc_not nc) ncs) with
+let prove_smt ~abstract ~assumptions:ncs (NC_aux (_, l) as nc) =
+  match Constraint.call_smt l abstract (List.fold_left nc_and (nc_not nc) ncs) with
   | Constraint.Unsat ->
       typ_debug (lazy "unsat");
       true
@@ -419,7 +419,7 @@ let prove_smt ~assumptions:ncs (NC_aux (_, l) as nc) =
          constraints, even when such constraints are irrelevant *)
       let ncs' = List.concat (List.map constraint_conj ncs) in
       let ncs' = List.filter (fun nc -> KidSet.is_empty (constraint_power_variables nc)) ncs' in
-      match Constraint.call_smt l (List.fold_left nc_and (nc_not nc) ncs') with
+      match Constraint.call_smt l abstract (List.fold_left nc_and (nc_not nc) ncs') with
       | Constraint.Unsat ->
           typ_debug (lazy "unsat");
           true
@@ -442,8 +442,9 @@ let solve_unique env (Nexp_aux (_, l) as nexp) =
       let env = Env.add_typ_var l (mk_kopt K_int (mk_kid "solve#")) env in
       let vars = Env.get_typ_vars env in
       let _vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
+      let abstract = Env.get_abstract_typs env in
       let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in
-      Constraint.solve_unique_smt l constr (mk_kid "solve#")
+      Constraint.solve_unique_smt l abstract constr (mk_kid "solve#")
 
 let debug_pos (file, line, _, _) = "(" ^ file ^ "/" ^ string_of_int line ^ ") "
 
@@ -464,7 +465,7 @@ let prove pos env nc =
       ^ string_of_list ", " string_of_n_constraint ncs
       ^ " |- " ^ string_of_n_constraint nc
       );
-  match nc_aux with NC_true -> true | _ -> prove_smt ~assumptions:ncs nc
+  match nc_aux with NC_true -> true | _ -> prove_smt ~abstract:(Env.get_abstract_typs env) ~assumptions:ncs nc
 
 (**************************************************************************)
 (* 3. Unification                                                         *)
@@ -508,8 +509,8 @@ let rec nc_identical (NC_aux (nc1, _)) (NC_aux (nc2, _)) =
   | NC_and (nc1a, nc1b), NC_and (nc2a, nc2b) -> nc_identical nc1a nc2a && nc_identical nc1b nc2b
   | NC_true, NC_true -> true
   | NC_false, NC_false -> true
-  | NC_set (kid1, ints1), NC_set (kid2, ints2) when List.length ints1 = List.length ints2 ->
-      Kid.compare kid1 kid2 = 0 && List.for_all2 (fun i1 i2 -> i1 = i2) ints1 ints2
+  | NC_set (nexp1, ints1), NC_set (nexp2, ints2) when List.length ints1 = List.length ints2 ->
+      nexp_identical nexp1 nexp2 && List.for_all2 (fun i1 i2 -> i1 = i2) ints1 ints2
   | NC_var kid1, NC_var kid2 -> Kid.compare kid1 kid2 = 0
   | NC_app (id1, args1), NC_app (id2, args2) when List.length args1 = List.length args2 ->
       Id.compare id1 id2 = 0 && List.for_all2 typ_arg_identical args1 args2
@@ -939,8 +940,9 @@ and kid_order_arg kind_map (A_aux (aux, _)) =
 
 and kid_order_constraint kind_map (NC_aux (aux, _)) =
   match aux with
-  | (NC_var kid | NC_set (kid, _)) when KBindings.mem kid kind_map ->
+  | NC_var kid when KBindings.mem kid kind_map ->
       ([mk_kopt (unaux_kind (KBindings.find kid kind_map)) kid], KBindings.remove kid kind_map)
+  | NC_set (n, _) -> kid_order_nexp kind_map n
   | NC_var _ | NC_set _ -> ([], kind_map)
   | NC_true | NC_false -> ([], kind_map)
   | NC_equal (n1, n2)
@@ -1078,7 +1080,7 @@ let rec subtyp l env typ1 typ2 =
         KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) (Env.get_typ_vars env)
       in
       begin
-        match Constraint.call_smt l (nc_eq nexp1 nexp2) with
+        match Constraint.call_smt l Bindings.empty (nc_eq nexp1 nexp2) with
         | Constraint.Sat ->
             let env = Env.add_constraint (nc_eq nexp1 nexp2) env in
             if prove __POS__ env nc2 then ()
@@ -1231,6 +1233,7 @@ let rec rewrite_sizeof' l env (Nexp_aux (aux, _) as nexp) =
       let exp1 = rewrite_sizeof' l env nexp1 in
       let exp2 = rewrite_sizeof' l env nexp2 in
       mk_exp (E_app (mk_id "emod_int", [exp1; exp2]))
+  | Nexp_id id when Env.is_abstract_typ id env -> mk_exp (E_sizeof nexp)
   | Nexp_app _ | Nexp_id _ -> typ_error l ("Cannot re-write sizeof(" ^ string_of_nexp nexp ^ ")")
 
 let rewrite_sizeof l env nexp =
@@ -1268,9 +1271,9 @@ and rewrite_nc_aux l env =
   | NC_false -> E_lit (mk_lit L_false)
   | NC_true -> E_lit (mk_lit L_true)
   | NC_set (_, []) -> E_lit (mk_lit L_false)
-  | NC_set (kid, int :: ints) ->
-      let kid_eq kid int = nc_eq (nvar kid) (nconstant int) in
-      unaux_exp (rewrite_nc env (List.fold_left (fun nc int -> nc_or nc (kid_eq kid int)) (kid_eq kid int) ints))
+  | NC_set (nexp, int :: ints) ->
+      let nexp_eq int = nc_eq nexp (nconstant int) in
+      unaux_exp (rewrite_nc env (List.fold_left (fun nc int -> nc_or nc (nexp_eq int)) (nexp_eq int) ints))
   | NC_app (f, [A_aux (A_bool nc, _)]) when string_of_id f = "not" -> E_app (mk_id "not_bool", [rewrite_nc env nc])
   | NC_app (f, args) -> unaux_exp (rewrite_nc env (Env.expand_constraint_synonyms env (mk_nc (NC_app (f, args)))))
   | NC_var v ->
@@ -3053,7 +3056,11 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) =
         )
     end
   | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
-  | E_sizeof nexp -> irule infer_exp env (rewrite_sizeof l env (Env.expand_nexp_synonyms env nexp))
+  | E_sizeof nexp -> begin
+      match nexp with
+      | Nexp_aux (Nexp_id id, _) when Env.is_abstract_typ id env -> annot_exp (E_sizeof nexp) (atom_typ nexp)
+      | _ -> irule infer_exp env (rewrite_sizeof l env (Env.expand_nexp_synonyms env nexp))
+    end
   | E_constraint nc ->
       Env.wf_constraint env nc;
       crule check_exp env (rewrite_nc env (Env.expand_constraint_synonyms env nc)) (atom_bool_typ nc)
@@ -4243,6 +4250,7 @@ let check_record l env def_annot id typq fields =
 
 let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list * Env.t =
  fun env def_annot (TD_aux (tdef, (l, _))) ->
+  typ_print (lazy ("\n" ^ Util.("Check type " |> cyan |> clear) ^ string_of_id (id_of_type_def_aux tdef)));
   match tdef with
   | TD_abbrev (id, typq, typ_arg) ->
       begin
@@ -4251,6 +4259,8 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list
         | _ -> ()
       end;
       ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.add_typ_synonym id typq typ_arg env)
+  | TD_abstract (id, kind) ->
+      ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.add_abstract_typ id kind env)
   | TD_record (id, typq, fields, _) ->
       let env = check_record l env def_annot id typq fields in
       ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env)
@@ -4494,6 +4504,7 @@ and check_def : Env.t -> uannot def -> tannot def list * Env.t =
   match aux with
   | DEF_fixity (prec, n, op) -> ([DEF_aux (DEF_fixity (prec, n, op), def_annot)], env)
   | DEF_type tdef -> check_typedef env def_annot tdef
+  | DEF_constraint nc -> ([DEF_aux (DEF_constraint nc, def_annot)], Env.add_constraint ~global:true nc env)
   | DEF_fundef fdef -> check_fundef env def_annot fdef
   | DEF_mapdef mdef -> check_mapdef env def_annot mdef
   | DEF_impl funcl -> check_impldef env def_annot funcl
diff --git a/src/lib/type_check.mli b/src/lib/type_check.mli
index bc82dd303..710ff8c40 100644
--- a/src/lib/type_check.mli
+++ b/src/lib/type_check.mli
@@ -147,7 +147,7 @@ module Env : sig
   (** Get the current set of constraints. *)
   val get_constraints : t -> n_constraint list
 
-  val add_constraint : ?reason:Ast.l * string -> n_constraint -> t -> t
+  val add_constraint : ?global:bool -> ?reason:Ast.l * string -> n_constraint -> t -> t
 
   (** Push all the type variables and constraints from a typquant into
       an environment *)
@@ -510,4 +510,4 @@ val initial_env : Env.t
 (** The initial type checking environment, with a specific set of available modules. *)
 val initial_env_with_modules : Project.project_structure -> Env.t
 
-val prove_smt : assumptions:n_constraint list -> n_constraint -> bool
+val prove_smt : abstract:kind Bindings.t -> assumptions:n_constraint list -> n_constraint -> bool
diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml
index 42d51403d..719b3ae1d 100644
--- a/src/lib/type_env.ml
+++ b/src/lib/type_env.ml
@@ -108,6 +108,8 @@ type global_env = {
   unions : (typquant * type_union list) env_item Bindings.t;
   union_ids : (typquant * typ) env_item Bindings.t;
   scattered_union_envs : global_env Bindings.t;
+  abstract_typs : kind env_item Bindings.t;
+  constraints : (constraint_reason * n_constraint) list;
   enums : (bool * IdSet.t) env_item Bindings.t;
   records : (typquant * (typ * id) list) env_item Bindings.t;
   synonyms : (typquant * typ_arg) env_item Bindings.t;
@@ -131,6 +133,8 @@ let empty_global_env =
     unions = Bindings.empty;
     union_ids = Bindings.empty;
     scattered_union_envs = Bindings.empty;
+    abstract_typs = Bindings.empty;
+    constraints = [];
     enums = Bindings.empty;
     records = Bindings.empty;
     accessors = IdPairMap.empty;
@@ -363,6 +367,7 @@ let builtin_typs =
 let bound_typ_id env id =
   Bindings.mem id env.global.synonyms || Bindings.mem id env.global.unions || Bindings.mem id env.global.records
   || Bindings.mem id env.global.enums || Bindings.mem id builtin_typs
+  || Bindings.mem id env.global.abstract_typs
 
 let get_binding_loc env id =
   let find map = Some (item_loc (Bindings.find id map)) in
@@ -371,6 +376,7 @@ let get_binding_loc env id =
   else if Bindings.mem id env.global.records then find env.global.records
   else if Bindings.mem id env.global.enums then find env.global.enums
   else if Bindings.mem id env.global.synonyms then find env.global.synonyms
+  else if Bindings.mem id env.global.abstract_typs then find env.global.abstract_typs
   else None
 
 let already_bound str id env =
@@ -508,6 +514,10 @@ let check_args_typquant id env args typq =
     typ_error (id_loc id)
       ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
 
+let get_constraints env = List.map snd env.global.constraints @ List.map snd env.constraints
+
+let get_constraint_reasons env = env.global.constraints @ env.constraints
+
 let mk_synonym typq typ_arg =
   let kopts, ncs = quant_split typq in
   let kopts = List.map (fun kopt -> (kopt, fresh_existential (kopt_loc kopt) (unaux_kind (kopt_kind kopt)))) kopts in
@@ -544,7 +554,7 @@ let mk_synonym typq typ_arg =
         ("Could not prove constraints "
         ^ string_of_list ", " string_of_n_constraint ncs
         ^ " in type synonym " ^ string_of_typ_arg typ_arg ^ " with "
-        ^ Util.string_of_list ", " string_of_n_constraint (List.map snd env.constraints)
+        ^ Util.string_of_list ", " string_of_n_constraint (get_constraints env)
         )
 
 let get_typ_synonym id env =
@@ -554,10 +564,6 @@ let get_typ_synonym id env =
 
 let get_typ_synonyms env = filter_items env env.global.synonyms
 
-let get_constraints env = List.map snd env.constraints
-
-let get_constraint_reasons env = env.constraints
-
 let wf_debug str f x exs =
   typ_debug ~level:2
     (lazy ("wf_" ^ str ^ ": " ^ f x ^ " exs: " ^ Util.string_of_list ", " string_of_kid (KidSet.elements exs)))
@@ -569,7 +575,7 @@ let rec wf_typ' ?(exs = KidSet.empty) env (Typ_aux (typ_aux, l) as typ) =
   match typ_aux with
   | Typ_id id when bound_typ_id env id ->
       let typq = infer_kind env id in
-      if quant_kopts typq != [] then
+      if not (Util.list_empty (quant_kopts typq)) then
         typ_error l ("Type constructor " ^ string_of_id id ^ " expected " ^ string_of_typquant typq)
       else ()
   | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id)
@@ -614,6 +620,7 @@ and wf_typ_arg ?(exs = KidSet.empty) env (A_aux (typ_arg_aux, _)) =
 and wf_nexp ?(exs = KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) =
   wf_debug "nexp" string_of_nexp nexp exs;
   match nexp_aux with
+  | Nexp_id id when Bindings.mem id env.global.abstract_typs -> ()
   | Nexp_id id -> typ_error l ("Undefined type synonym " ^ string_of_id id)
   | Nexp_var kid when KidSet.mem kid exs -> ()
   | Nexp_var kid -> begin
@@ -642,6 +649,8 @@ and wf_nexp ?(exs = KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) =
 and wf_constraint ?(exs = KidSet.empty) env (NC_aux (nc_aux, l) as nc) =
   wf_debug "constraint" string_of_n_constraint nc exs;
   match nc_aux with
+  | NC_id id when Bindings.mem id env.global.abstract_typs -> ()
+  | NC_id id -> typ_error l ("Undefined type synonym " ^ string_of_id id)
   | NC_equal (n1, n2) ->
       wf_nexp ~exs env n1;
       wf_nexp ~exs env n2
@@ -660,16 +669,7 @@ and wf_constraint ?(exs = KidSet.empty) env (NC_aux (nc_aux, l) as nc) =
   | NC_bounded_lt (n1, n2) ->
       wf_nexp ~exs env n1;
       wf_nexp ~exs env n2
-  | NC_set (kid, _) when KidSet.mem kid exs -> ()
-  | NC_set (kid, _) -> begin
-      match get_typ_var kid env with
-      | K_int -> ()
-      | kind ->
-          typ_error l
-            ("Set constraint is badly formed, " ^ string_of_kid kid ^ " has kind " ^ string_of_kind_aux kind
-           ^ " but should have kind Int"
-            )
-    end
+  | NC_set (nexp, _) -> wf_nexp ~exs env nexp
   | NC_or (nc1, nc2) ->
       wf_constraint ~exs env nc1;
       wf_constraint ~exs env nc2
@@ -685,6 +685,23 @@ and wf_constraint ?(exs = KidSet.empty) env (NC_aux (nc_aux, l) as nc) =
     end
   | NC_true | NC_false -> ()
 
+let add_abstract_typ id kind env =
+  if bound_typ_id env id then
+    typ_error (id_loc id)
+      ("Cannot introduce abstract type " ^ string_of_id id ^ " as a type or synonym with that name already exists")
+  else (
+    typ_print (lazy (adding ^ "abstract type " ^ string_of_id id ^ " : " ^ string_of_kind kind)) [@coverage off];
+    update_global
+      (fun global ->
+        { global with abstract_typs = Bindings.add id (mk_item env ~loc:(id_loc id) kind) global.abstract_typs }
+      )
+      env
+  )
+
+let get_abstract_typs env = filter_items env env.global.abstract_typs
+
+let is_abstract_typ id env = Bindings.mem id env.global.abstract_typs
+
 let rec expand_constraint_synonyms env (NC_aux (aux, l) as nc) =
   match aux with
   | NC_or (nc1, nc2) -> NC_aux (NC_or (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l)
@@ -802,7 +819,7 @@ and expand_arg_synonyms env (A_aux (typ_arg, l)) =
   | A_bool nc -> A_aux (A_bool (expand_constraint_synonyms env nc), l)
   | A_nexp nexp -> A_aux (A_nexp (expand_nexp_synonyms env nexp), l)
 
-and add_constraint ?reason constr env =
+and add_constraint ?(global = false) ?reason constr env =
   let (NC_aux (nc_aux, l) as constr) = constraint_simp (expand_constraint_synonyms env constr) in
   wf_constraint env constr;
   let power_vars = constraint_power_variables constr in
@@ -815,7 +832,7 @@ and add_constraint ?reason constr env =
     let v = KidSet.choose power_vars in
     let constrs = List.fold_left nc_and nc_true (get_constraints env) in
     begin
-      match Constraint.solve_all_smt l constrs v with
+      match Constraint.solve_all_smt l (get_abstract_typs env) constrs v with
       | Some solutions ->
           typ_print
             ( lazy
@@ -845,7 +862,11 @@ and add_constraint ?reason constr env =
     | NC_true -> env
     | _ ->
         typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr)) [@coverage off];
-        { env with constraints = (reason, constr) :: env.constraints }
+        if global then
+          update_global
+            (fun global_env -> { global_env with constraints = (reason, constr) :: global_env.constraints })
+            env
+        else { env with constraints = (reason, constr) :: env.constraints }
   )
 
 let add_typquant l quant env =
diff --git a/src/lib/type_env.mli b/src/lib/type_env.mli
index b598ae491..44db1d123 100644
--- a/src/lib/type_env.mli
+++ b/src/lib/type_env.mli
@@ -132,6 +132,10 @@ val add_outcome_variable : l -> kid -> typ -> t -> t
 val set_outcome_typschm : outcome_loc:l -> typquant * typ -> t -> t
 val get_outcome_typschm_opt : t -> (typquant * typ) option
 
+val add_abstract_typ : id -> kind -> t -> t
+val is_abstract_typ : id -> t -> bool
+val get_abstract_typs : t -> kind Bindings.t
+
 val is_variant : id -> t -> bool
 val add_variant : id -> typquant * type_union list -> t -> t
 val add_scattered_variant : id -> typquant -> t -> t
@@ -169,7 +173,7 @@ val add_register : id -> typ -> t -> t
 
 val get_constraints : t -> n_constraint list
 val get_constraint_reasons : t -> ((Ast.l * string) option * n_constraint) list
-val add_constraint : ?reason:Ast.l * string -> n_constraint -> t -> t
+val add_constraint : ?global:bool -> ?reason:Ast.l * string -> n_constraint -> t -> t
 
 val add_typquant : l -> typquant -> t -> t
 
diff --git a/src/lib/type_internal.ml b/src/lib/type_internal.ml
index 9cd7ebd65..ae35131b3 100644
--- a/src/lib/type_internal.ml
+++ b/src/lib/type_internal.ml
@@ -150,7 +150,7 @@ and unloc_n_constraint_aux = function
   | NC_bounded_le (nexp1, nexp2) -> NC_bounded_le (unloc_nexp nexp1, unloc_nexp nexp2)
   | NC_bounded_lt (nexp1, nexp2) -> NC_bounded_lt (unloc_nexp nexp1, unloc_nexp nexp2)
   | NC_not_equal (nexp1, nexp2) -> NC_not_equal (unloc_nexp nexp1, unloc_nexp nexp2)
-  | NC_set (kid, nums) -> NC_set (unloc_kid kid, nums)
+  | NC_set (nexp, nums) -> NC_set (unloc_nexp nexp, nums)
   | NC_or (nc1, nc2) -> NC_or (unloc_n_constraint nc1, unloc_n_constraint nc2)
   | NC_and (nc1, nc2) -> NC_and (unloc_n_constraint nc1, unloc_n_constraint nc2)
   | NC_var kid -> NC_var (unloc_kid kid)
diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml
index 8f90c2986..9eafd707d 100644
--- a/src/sail_coq_backend/pretty_print_coq.ml
+++ b/src/sail_coq_backend/pretty_print_coq.ml
@@ -320,7 +320,7 @@ let rec orig_nc (NC_aux (nc, l) as full_nc) =
   | NC_bounded_le (nexp1, nexp2) -> rewrap (NC_bounded_le (orig_nexp nexp1, orig_nexp nexp2))
   | NC_bounded_lt (nexp1, nexp2) -> rewrap (NC_bounded_lt (orig_nexp nexp1, orig_nexp nexp2))
   | NC_not_equal (nexp1, nexp2) -> rewrap (NC_not_equal (orig_nexp nexp1, orig_nexp nexp2))
-  | NC_set (kid, s) -> rewrap (NC_set (orig_kid kid, s))
+  | NC_set (nexp, s) -> rewrap (NC_set (orig_nexp nexp, s))
   | NC_or (nc1, nc2) -> rewrap (NC_or (orig_nc nc1, orig_nc nc2))
   | NC_and (nc1, nc2) -> rewrap (NC_and (orig_nc nc1, orig_nc nc2))
   | NC_app (f, args) -> rewrap (NC_app (f, List.map orig_typ_arg args))
@@ -419,7 +419,8 @@ let rec count_nc_vars (NC_aux (nc, _)) =
   in
   match nc with
   | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> merge_kid_count (count_nc_vars nc1) (count_nc_vars nc2)
-  | NC_var kid | NC_set (kid, _) -> KBindings.singleton kid 1
+  | NC_var kid -> KBindings.singleton kid 1
+  | NC_set (n, _) -> count_nexp_vars n
   | NC_equal (n1, n2)
   | NC_bounded_ge (n1, n2)
   | NC_bounded_gt (n1, n2)
@@ -459,7 +460,7 @@ let simplify_atom_bool l kopts nc atom_nc =
       | NC_bounded_lt (_, Nexp_aux (Nexp_var kid, _)) when KBindings.mem kid lin_ty_vars -> Some kid
       | NC_not_equal (Nexp_aux (Nexp_var kid, _), _) when KBindings.mem kid lin_ty_vars -> Some kid
       | NC_not_equal (_, Nexp_aux (Nexp_var kid, _)) when KBindings.mem kid lin_ty_vars -> Some kid
-      | NC_set (kid, _ :: _) when KBindings.mem kid lin_ty_vars -> Some kid
+      | NC_set (Nexp_aux (Nexp_var kid, _), _ :: _) when KBindings.mem kid lin_ty_vars -> Some kid
       | _ -> None
     in
     let replace kills vars =
@@ -816,11 +817,11 @@ and doc_nc_exp ctx env nc =
     match nc with
     | NC_not_equal (ne1, ne2) ->
         string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2))
-    | NC_set (kid, is) ->
+    | NC_set (nexp, is) ->
         separate space
           [
             string "member_Z_list";
-            doc_var ctx kid;
+            doc_nexp ctx nexp;
             brackets (separate (string "; ") (List.map (fun i -> string (Nat_big_num.to_string i)) is));
           ]
     | NC_app (f, args) -> separate space (doc_nc_fn ctx f :: List.map doc_typ_arg_exp args)
diff --git a/test/typecheck/pass/complex_exist_sat/v2.expect b/test/typecheck/pass/complex_exist_sat/v2.expect
index 1a98f3339..e7d253d79 100644
--- a/test/typecheck/pass/complex_exist_sat/v2.expect
+++ b/test/typecheck/pass/complex_exist_sat/v2.expect
@@ -3,7 +3,7 @@
 3 |function foo(x) = 4
   |                  ^
   | int(4) is not a subtype of {('q : Int), 'q in {0, 1}. int((2 * 'q))}
-  | as ('ex2 == 0 | 'ex2 == 1) could not be proven
+  | as 'ex2 in {0, 1} could not be proven
   | 
   | type variable 'ex2:
   | pass/complex_exist_sat/v2.sail:1.18-50:
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
index c9ed441f7..c832f69b6 100644
--- a/test/typecheck/pass/constrained_struct/v1.expect
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -12,4 +12,4 @@
    |    | Caused by pass/constrained_struct/v1.sail:10.18-26:
    |    | 10 |type MyStruct64 = MyStruct(65)
    |    |    |                  ^------^
-   |    | Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct
+   |    | Could not prove 65 in {32, 64} for type constructor MyStruct
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index 78dce04af..d2bb18654 100644
--- a/test/typecheck/pass/existential_ast3/v1.expect
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -3,7 +3,7 @@
 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |                                                ^---------------^
    | (int(33), int('ex291)) is not a subtype of (int('ex286), int('ex287))
-   | as ((33 == 32 | 33 == 64) & (0 <= 'ex291 & 'ex291 < 33)) could not be proven
+   | as false could not be proven
    | 
    | type variable 'ex286:
    | pass/existential_ast3/v1.sail:16.23-25:
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index 858b6cf3f..3a1d2d19d 100644
--- a/test/typecheck/pass/existential_ast3/v2.expect
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -3,7 +3,7 @@
 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |                                                ^---------------^
    | (int(31), int('ex291)) is not a subtype of (int('ex286), int('ex287))
-   | as ((31 == 32 | 31 == 64) & (0 <= 'ex291 & 'ex291 < 31)) could not be proven
+   | as false could not be proven
    | 
    | type variable 'ex286:
    | pass/existential_ast3/v2.sail:16.23-25:
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index 342792364..a69623584 100644
--- a/test/typecheck/pass/existential_ast3/v3.expect
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -3,4 +3,4 @@
 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
    |         ^-----------------------------^
    | Could not resolve quantifiers for Ctor
-   | * ((64 == 32 | 64 == 64) & (0 <= 'ex330# & 'ex330# < 64))
+   | * (64 in {32, 64} & (0 <= 'ex330# & 'ex330# < 64))
diff --git a/test/typecheck/pass/reg_32_64/v1.expect b/test/typecheck/pass/reg_32_64/v1.expect
index 5a9d57f87..bd5c98f54 100644
--- a/test/typecheck/pass/reg_32_64/v1.expect
+++ b/test/typecheck/pass/reg_32_64/v1.expect
@@ -11,6 +11,6 @@ Explicit effect annotations are deprecated. They are no longer used and can be r
    | No overloading for R, tried:
    | * set_R
    |    Could not resolve quantifiers for set_R
-   |    * (regno(0) & (56 == 32 | 56 == 64))
+   |    * (regno(0) & 56 in {32, 64})
    | * get_R
    |    Could not unify int('r) and bitvector(56)