diff --git a/CHANGELOG.md b/CHANGELOG.md
index dd62087a9..285c8bbc9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,27 @@
 Changelog
 =========
 
+Sail 0.19
+---------
+
+##### Stricter bitvector type indexing
+
+Stricter indexing for bitvector types. Previous versions of Sail
+treated `bitvector('n)` as uninhabited if `'n < 0`, but otherwise
+permitted such bitvector types in signatures. Now the type
+`bitvector('n)` is only well-formed if `'n >= 0`. This is a breaking
+change, as some previously permitted definitions are now rejected
+without additional constraints. However Sail has a new kind `Nat`
+which allows it to infer these `>= 0` constraints when explicit type
+variables are ommited, so in a function signature
+```
+val foo : forall 'n. bits('n) -> bool
+```
+the `'n` type variable will be inferred as:
+```
+val foo : forall ('n : Nat). bits('n) -> bool
+```
+
 Sail 0.18
 ---------
 
diff --git a/lib/concurrency_interface/read_write.sail b/lib/concurrency_interface/read_write.sail
index ec038c4bb..f5109d8e2 100644
--- a/lib/concurrency_interface/read_write.sail
+++ b/lib/concurrency_interface/read_write.sail
@@ -107,7 +107,7 @@ union Access_kind('arch_ak : Type) = {
 $option -lem_extern_type Mem_read_request
 $option -coq_extern_type Mem_read_request
 struct Mem_read_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
-                        'arch_ak: Type), 'n > 0 = {
+                        'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   access_kind : Access_kind('arch_ak),
   // There may not always be a virtual address, e.g. when translation is off.
   // Additionally, translate reads don't have a (VA, PA) pair in the
@@ -203,7 +203,7 @@ with
 $option -lem_extern_type Mem_write_request
 $option -coq_extern_type Mem_write_request
 struct Mem_write_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
-                         'arch_ak : Type), 'n > 0 = {
+                         'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   access_kind : Access_kind('arch_ak),
   va : option(bits('vasize)),
   pa : 'pa,
diff --git a/lib/vector.sail b/lib/vector.sail
index a77c79cb8..d2901224b 100644
--- a/lib/vector.sail
+++ b/lib/vector.sail
@@ -74,7 +74,7 @@ $endif
 
 $include <flow.sail>
 
-type bits('n : Int) = bitvector('n)
+type bits('n) = bitvector('n)
 
 val eq_bits = pure {
   ocaml: "eq_list",
@@ -150,7 +150,7 @@ function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail
 
 overload operator ^ = {sail_mask}
 
-val bitvector_concat = pure {ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec", _: "append"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = pure {ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec", _: "append"} : forall 'n 'm.
   (bits('n), bits('m)) -> bits('n + 'm)
 
 overload append = {bitvector_concat}
@@ -337,7 +337,7 @@ val slice = pure "slice_inc" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm.
   (bits('m), int('o), int('n)) -> bits('n)
 $endif
 
-val replicate_bits = pure "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bits('n * 'm)
+val replicate_bits = pure "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), int('m)) -> bits('n * 'm)
 
 val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n)
 function slice_mask(n,i,l) =
diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml
index 4acba9728..285458e1a 100644
--- a/src/lib/ast_util.ml
+++ b/src/lib/ast_util.ml
@@ -809,6 +809,12 @@ let quant_map_items f = function
   | TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_no_forall, l)
   | TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (List.map f qis), l)
 
+let quant_fold_map_items f acc = function
+  | TypQ_aux (TypQ_no_forall, l) -> (acc, TypQ_aux (TypQ_no_forall, l))
+  | TypQ_aux (TypQ_tq qis, l) ->
+      let acc, qis = Util.fold_left_map f acc qis in
+      (acc, TypQ_aux (TypQ_tq qis, l))
+
 let is_quant_kopt = function QI_aux (QI_id _, _) -> true | _ -> false
 
 let is_quant_constraint = function QI_aux (QI_constraint _, _) -> true | _ -> false
diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli
index 62ae86ee6..d33791e58 100644
--- a/src/lib/ast_util.mli
+++ b/src/lib/ast_util.mli
@@ -435,6 +435,7 @@ val quant_items : typquant -> quant_item list
 val quant_kopts : typquant -> kinded_id list
 val quant_split : typquant -> kinded_id list * n_constraint list
 val quant_map_items : (quant_item -> quant_item) -> typquant -> typquant
+val quant_fold_map_items : ('acc -> quant_item -> 'acc * quant_item) -> 'acc -> typquant -> 'acc * typquant
 
 val is_quant_kopt : quant_item -> bool
 val is_quant_constraint : quant_item -> bool
diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml
index 6b73b3bb9..2bf5ab7f1 100644
--- a/src/lib/chunk_ast.ml
+++ b/src/lib/chunk_ast.ml
@@ -481,7 +481,7 @@ let pop_trailing_comment ?space:(n = 0) comments chunks line_num =
     end
 
 let string_of_kind (K_aux (k, _)) =
-  match k with K_type -> "Type" | K_int -> "Int" | K_order -> "Order" | K_bool -> "Bool"
+  match k with K_type -> "Type" | K_int -> "Int" | K_nat -> "Nat" | K_order -> "Order" | K_bool -> "Bool"
 
 (* Right now, let's just assume we never break up kinded-identifiers *)
 let chunk_of_kopt (KOpt_aux (KOpt_kind (special, vars, kind, _), l)) =
diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml
index 88a723f34..4256c552e 100644
--- a/src/lib/initial_check.ml
+++ b/src/lib/initial_check.ml
@@ -89,7 +89,7 @@ module StringMap = Map.Make (String)
    $sail_internal marked files in the prelude. *)
 let reserved_type_ids = IdSet.of_list [mk_id "result"; mk_id "option"]
 
-type type_constructor = kind_aux option list * kind_aux
+type type_constructor = P.kind_aux list * P.kind_aux
 
 type ctx = {
   kinds : (kind_aux * P.l) KBindings.t;
@@ -168,19 +168,47 @@ let string_contains str char =
     true
   with Not_found -> false
 
+let to_ast_kind_aux = function
+  | P.K_type -> Some K_type
+  | P.K_int -> Some K_int
+  | P.K_nat -> Some K_int
+  | P.K_order -> None
+  | P.K_bool -> Some K_bool
+
 let to_ast_kind (P.K_aux (k, l)) =
   match k with
   | P.K_type -> Some (K_aux (K_type, l))
   | P.K_int -> Some (K_aux (K_int, l))
+  | P.K_nat -> Some (K_aux (K_int, l))
   | P.K_order -> None
   | P.K_bool -> Some (K_aux (K_bool, l))
 
+let parse_kind_constraint l v = function
+  | P.K_nat ->
+      let v = Nexp_aux (Nexp_var v, kid_loc v) in
+      Some (NC_aux (NC_ge (v, Nexp_aux (Nexp_constant Big_int.zero, l)), l))
+  | _ -> None
+
+let not_order_kind = function P.K_order -> false | _ -> true
+
+let filter_order_kinds kinds = List.filter not_order_kind kinds
+
 let string_of_parse_kind_aux = function
   | P.K_order -> "Order"
   | P.K_int -> "Int"
+  | P.K_nat -> "Nat"
   | P.K_bool -> "Bool"
   | P.K_type -> "Type"
 
+(* Used for error messages involving lists of kinds *)
+let format_parse_kind_aux_list = function
+  | [kind] -> string_of_parse_kind_aux kind
+  | kinds -> "(" ^ Util.string_of_list ", " string_of_parse_kind_aux kinds ^ ")"
+
+let format_kind_aux_list = function
+  | [kind] -> string_of_kind_aux kind
+  | kinds -> "(" ^ Util.string_of_list ", " string_of_kind_aux kinds ^ ")"
+
 let to_parse_kind = function
   | Some K_int -> P.K_int
   | Some K_bool -> P.K_bool
@@ -316,11 +344,6 @@ let parse_infix_atyp ctx = function
 
 let to_ast_var (P.Kid_aux (P.Var v, l)) = Kid_aux (Var v, l)
 
-(* Used for error messages involving lists of kinds *)
-let format_kind_aux_list = function
-  | [kind] -> string_of_kind_aux kind
-  | kinds -> "(" ^ Util.string_of_list ", " string_of_kind_aux kinds ^ ")"
-
 (** The [KindInference] module implements a type-inference module for
     kind (types of types).
 
@@ -373,9 +396,10 @@ module KindInference = struct
     in
     ((), { env with sets = go env.sets })
 
-  let check_same_kind kind l kind' l' =
+  let unify_kind kind l kind' l' =
     match (kind, kind') with
-    | P.K_int, P.K_int | P.K_bool, P.K_bool | P.K_type, P.K_type | P.K_order, P.K_order -> ()
+    | P.K_nat, P.K_int | P.K_int, P.K_nat -> P.K_nat
+    | P.K_int, P.K_int | P.K_nat, P.K_nat | P.K_bool, P.K_bool | P.K_type, P.K_type | P.K_order, P.K_order -> kind
     | _ ->
         raise
           (Reporting.err_typ
@@ -390,8 +414,8 @@ module KindInference = struct
     | Unknown, Unknown -> Unknown
     | Unknown, known | known, Unknown -> known
     | Known (kind, l), Known (kind', l') ->
-        check_same_kind kind l kind' l';
-        Known (kind, l)
+        let kind'' = unify_kind kind l kind' l' in
+        Known (kind'', l)
 
   let unify n m env =
     let n_sets, other_sets = List.partition (fun (set, _) -> IntSet.mem n set) env.sets in
@@ -442,7 +466,7 @@ module KindInference = struct
         let n_set, nk = List.hd n_sets in
         ((), { env with sets = (n_set, merge_unification_kind nk (Known (kind, l))) :: env.sets })
     | Kind (kind', l') ->
-        check_same_kind kind l kind' l';
+        let _ = unify_kind kind l kind' l' in
         ((), env)
 
   let atyp_loc (P.ATyp_aux (_, l)) = l
@@ -455,7 +479,7 @@ module KindInference = struct
         let* () =
           match Bindings.find_opt id' ctx.type_constructors with
           | None -> return ()
-          | Some ([], ret_kind) -> resolve ~at:l (to_parse_kind (Some ret_kind)) ik
+          | Some ([], ret_kind) -> resolve ~at:l ret_kind ik
           | Some (kind_opts, _) -> raise (ksprintf (Reporting.err_typ l) "%s is not a constant" (string_of_id id'))
         in
         return atyp
@@ -509,19 +533,35 @@ module KindInference = struct
         let* arg = check ctx arg (Kind (P.K_bool, atyp_loc arg)) in
         wrap (P.ATyp_app (id, [arg]))
     | P.ATyp_sum (t1, t2) ->
-        let* t1 = check ctx t1 ik in
-        let* t2 = check ctx t2 ik in
+        let* () = resolve ~at:l K_int ik in
+        let* t1 = check ctx t1 (Kind (P.K_int, atyp_loc t1)) in
+        let* t2 = check ctx t2 (Kind (P.K_int, atyp_loc t2)) in
         wrap (P.ATyp_sum (t1, t2))
-    | P.ATyp_times (t1, t2) ->
-        let* t1 = check ctx t1 ik in
-        let* t2 = check ctx t2 ik in
-        wrap (P.ATyp_times (t1, t2))
+    | P.ATyp_times (t1, t2) -> begin
+        (* Special case N * M when either N or M is a constant > 0, in
+           which case we can infer that if N * M is a Nat then the
+           non-constant case is also a Nat *)
+        match (t1, t2) with
+        | P.ATyp_aux (P.ATyp_lit (P.L_aux (P.L_num n, _)), _), _ when Big_int.greater n Big_int.zero ->
+            let* t2 = check ctx t2 ik in
+            wrap (P.ATyp_times (t1, t2))
+        | _, P.ATyp_aux (P.ATyp_lit (P.L_aux (P.L_num n, _)), _) when Big_int.greater n Big_int.zero ->
+            let* t1 = check ctx t1 ik in
+            wrap (P.ATyp_times (t1, t2))
+        | _ ->
+            let* () = resolve ~at:l K_int ik in
+            let* t1 = check ctx t1 (Kind (P.K_int, atyp_loc t1)) in
+            let* t2 = check ctx t2 (Kind (P.K_int, atyp_loc t2)) in
+            wrap (P.ATyp_times (t1, t2))
+      end
     | P.ATyp_minus (t1, t2) ->
-        let* t1 = check ctx t1 ik in
-        let* t2 = check ctx t2 ik in
+        let* () = resolve ~at:l K_int ik in
+        let* t1 = check ctx t1 (Kind (P.K_int, atyp_loc t1)) in
+        let* t2 = check ctx t2 (Kind (P.K_int, atyp_loc t2)) in
         wrap (P.ATyp_minus (t1, t2))
     | P.ATyp_exp t ->
-        let* t = check ctx t ik in
+        let* () = resolve ~at:l K_int ik in
+        let* t = check ctx t (Kind (P.K_int, atyp_loc t)) in
         wrap (P.ATyp_exp t)
     | P.ATyp_neg t ->
         let* t = check ctx t ik in
@@ -532,23 +572,19 @@ module KindInference = struct
           match Bindings.find_opt id' ctx.type_constructors with
           | None ->
               raise (ksprintf (Reporting.err_typ l) "Unknown type level operator or function %s" (string_of_id id'))
-          | Some (kind_opts, ret_kind) ->
-              let* () = resolve ~at:l (to_parse_kind (Some ret_kind)) ik in
+          | Some (kinds, ret_kind) ->
+              let* () = resolve ~at:l ret_kind ik in
               let args_len = List.length args in
-              let kind_opts =
-                if args_len = List.length kind_opts then kind_opts else List.filter Option.is_some kind_opts
-              in
-              if List.compare_lengths args kind_opts <> 0 then
+              let kinds = if args_len = List.length kinds then kinds else filter_order_kinds kinds in
+              if List.compare_lengths args kinds <> 0 then
                 raise
                   (Reporting.err_typ l
                      (sprintf "%s : %s -> Type expected %d arguments, given %d" (string_of_id id')
-                        (format_kind_aux_list (Util.option_these kind_opts))
-                        (List.length kind_opts) (List.length args)
+                        (format_parse_kind_aux_list (filter_order_kinds kinds))
+                        (List.length kinds) (List.length args)
                      )
                   );
-              mapM
-                (function arg, kind -> check ctx arg (Kind (to_parse_kind kind, id_loc id')))
-                (List.combine args kind_opts)
+              mapM (function arg, kind -> check ctx arg (Kind (kind, id_loc id'))) (List.combine args kinds)
         in
         wrap (P.ATyp_app (id, args))
     | P.ATyp_lit (P.L_aux (aux, _)) ->
@@ -782,11 +818,25 @@ end
 
 module ConvertType = struct
   let to_ast_kopts kenv ctx (P.KOpt_aux (aux, l)) =
-    let mk_kopt v k =
+    let open Util.Option_monad in
+    let mk_kopt v (P.K_aux (aux, _) as k) =
       let v = to_ast_var v in
-      Option.map
-        (fun k -> (KOpt_aux (KOpt_kind (k, v), l), { ctx with kinds = KBindings.add v (unaux_kind k, l) ctx.kinds }))
-        (to_ast_kind k)
+      let* k = to_ast_kind k in
+      Some
+        ( KOpt_aux (KOpt_kind (k, v), l),
+          parse_kind_constraint l v aux,
+          { ctx with kinds = KBindings.add v (unaux_kind k, l) ctx.kinds }
+        )
+    in
+    let fold_vars vs k =
+      List.fold_left
+        (fun (kopts, constrs, ctx) v ->
+          match mk_kopt v k with
+          | Some (kopt, None, ctx) -> (kopt :: kopts, constrs, ctx)
+          | Some (kopt, Some constr, ctx) -> (kopt :: kopts, constr :: constrs, ctx)
+          | None -> (kopts, constrs, ctx)
+        )
+        ([], [], ctx) vs
     in
     match aux with
     | P.KOpt_kind (attr, vs, None, Some u) ->
@@ -795,30 +845,26 @@ module ConvertType = struct
           | Some k -> P.K_aux (k, gen_loc l)
           | None -> raise (Reporting.err_typ l "Could not infer Kind for this type variable")
         in
-        ( List.fold_left
-            (fun (kopts, ctx) v ->
-              match mk_kopt v k with Some (kopt, ctx) -> (kopt :: kopts, ctx) | None -> (kopts, ctx)
-            )
-            ([], ctx) vs,
-          attr
-        )
+        (fold_vars vs k, attr)
     | P.KOpt_kind (attr, vs, None, None) ->
         let k = P.K_aux (P.K_int, gen_loc l) in
-        ( List.fold_left
-            (fun (kopts, ctx) v ->
-              match mk_kopt v k with Some (kopt, ctx) -> (kopt :: kopts, ctx) | None -> (kopts, ctx)
-            )
-            ([], ctx) vs,
-          attr
-        )
-    | P.KOpt_kind (attr, vs, Some k, _) ->
-        ( List.fold_left
-            (fun (kopts, ctx) v ->
-              match mk_kopt v k with Some (kopt, ctx) -> (kopt :: kopts, ctx) | None -> (kopts, ctx)
-            )
-            ([], ctx) vs,
-          attr
-        )
+        (fold_vars vs k, attr)
+    | P.KOpt_kind (attr, vs, Some k, _) -> (fold_vars vs k, attr)
+
+  let get_inference_kinds kenv = function
+    | P.TypQ_aux (P.TypQ_no_forall, _) -> []
+    | P.TypQ_aux (P.TypQ_tq qis, _) ->
+        let qi_kinds = function
+          | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_kind (_, vs, None, Some u), l)), _) -> begin
+              match KindInference.get_kind ~at:l u kenv with
+              | Some k -> List.init (List.length vs) (fun _ -> k)
+              | None -> raise (Reporting.err_typ l "Could not infer Kind for this type variable")
+            end
+          | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_kind (_, vs, Some (P.K_aux (k, _)), _), _)), _) ->
+              List.init (List.length vs) (fun _ -> k)
+          | _ -> []
+        in
+        List.concat (List.map qi_kinds qis)
 
   let rec to_ast_typ kenv ctx atyp =
     let (P.ATyp_aux (aux, l)) = parse_infix_atyp ctx atyp in
@@ -847,7 +893,8 @@ module ConvertType = struct
           match Bindings.find_opt id ctx.type_constructors with
           | None -> raise (Reporting.err_typ l (sprintf "Could not find type constructor %s" (string_of_id id)))
           | Some (kinds, _) ->
-              let non_order_kinds = Util.option_these kinds in
+              let non_order_kinds = List.filter_map to_ast_kind_aux kinds in
+              let kinds = List.map to_ast_kind_aux kinds in
               let args_len = List.length args in
               if args_len = List.length non_order_kinds then
                 Typ_aux (Typ_app (id, List.map2 (to_ast_typ_arg kenv ctx) args non_order_kinds), l)
@@ -872,7 +919,7 @@ module ConvertType = struct
         let kopts, ctx =
           List.fold_right
             (fun kopt (kopts, ctx) ->
-              let (kopts', ctx), attr = to_ast_kopts kenv ctx kopt in
+              let (kopts', _, ctx), attr = to_ast_kopts kenv ctx kopt in
               match attr with
               | None -> (kopts' @ kopts, ctx)
               | Some attr ->
@@ -952,7 +999,7 @@ module ConvertType = struct
                   match Bindings.find_opt id ctx.type_constructors with
                   | None -> raise (Reporting.err_typ l (sprintf "Could not find type constructor %s" (string_of_id id)))
                   | Some (kinds, _) ->
-                      let non_order_kinds = Util.option_these kinds in
+                      let non_order_kinds = List.filter_map to_ast_kind_aux kinds in
                       if List.length non_order_kinds = 2 then
                         NC_app (id, List.map2 (to_ast_typ_arg kenv ctx) [t1; t2] non_order_kinds)
                       else
@@ -970,7 +1017,7 @@ module ConvertType = struct
                 match Bindings.find_opt id ctx.type_constructors with
                 | None -> raise (Reporting.err_typ l (sprintf "Could not find type constructor %s" (string_of_id id)))
                 | Some (kinds, _) ->
-                    let non_order_kinds = Util.option_these kinds in
+                    let non_order_kinds = List.filter_map to_ast_kind_aux kinds in
                     if List.length args = List.length non_order_kinds then
                       NC_app (id, List.map2 (to_ast_typ_arg kenv ctx) args non_order_kinds)
                     else
@@ -993,15 +1040,17 @@ module ConvertType = struct
   let to_ast_quant_items kenv ctx (P.QI_aux (aux, l)) =
     match aux with
     | P.QI_constraint nc -> ([QI_aux (QI_constraint (to_ast_constraint kenv ctx nc), l)], ctx)
-    | P.QI_id kopt -> (
-        let (kopts, ctx), attr = to_ast_kopts kenv ctx kopt in
-        match attr with
-        | Some "constant" ->
-            Reporting.warn "Deprecated" l "constant type variable attribute no longer used";
-            (List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, ctx)
-        | Some attr -> raise (Reporting.err_typ l (sprintf "Unknown attribute %s" attr))
-        | None -> (List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, ctx)
-      )
+    | P.QI_id kopt ->
+        let (kopts, constrs, ctx), attr = to_ast_kopts kenv ctx kopt in
+        begin
+          match attr with
+          | Some "constant" -> Reporting.warn "Deprecated" l "constant type variable attribute no longer used"
+          | Some attr -> raise (Reporting.err_typ l (sprintf "Unknown attribute %s" attr))
+          | None -> ()
+        end;
+        ( List.map (fun c -> QI_aux (QI_constraint c, l)) constrs @ List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts,
+          ctx
+        )
 
   let to_ast_typquant kenv ctx (P.TypQ_aux (aux, l)) =
     match aux with
@@ -1070,12 +1119,13 @@ let to_ast_type_union = ConvertType.to_ast_type_union KindInference.initial_env
 let to_ast_bind ctx typq atyp kind_opt =
   let open KindInference in
   let (typq, atyp, kind), kenv = check_bind ctx typq atyp kind_opt initial_env in
+  let inference_kinds = ConvertType.get_inference_kinds kenv typq in
   let typq, ctx = ConvertType.to_ast_typquant kenv ctx typq in
   match to_ast_kind kind with
   | None -> None
   | Some kind ->
       let typ_arg = ConvertType.to_ast_typ_arg kenv ctx atyp (unaux_kind kind) in
-      Some (typq, typ_arg, kind)
+      Some (typq, typ_arg, kind, inference_kinds)
 
 let to_ast_typschm ctx (P.TypSchm_aux (P.TypSchm_ts (typq, typ), l)) =
   let open KindInference in
@@ -1414,7 +1464,7 @@ let to_ast_outcome ctx (ev : P.outcome_spec) : outcome_spec ctx_out =
       let outcome_args, inner_ctx =
         List.fold_left
           (fun (args, ctx) arg ->
-            let (arg, ctx), _ = to_ast_kopts ctx arg in
+            let (arg, _, ctx), _ = to_ast_kopts ctx arg in
             (arg @ args, ctx)
           )
           ([], ctx) outcome_args
@@ -1434,8 +1484,8 @@ let rec to_ast_range ctx (P.BF_aux (r, l)) =
     )
 
 let add_constructor id typq kind ctx =
-  let kinds = List.map (fun kopt -> Some (unaux_kind (kopt_kind kopt))) (quant_kopts typq) in
-  { ctx with type_constructors = Bindings.add id (kinds, kind) ctx.type_constructors }
+  let kinds = List.map (fun kopt -> to_parse_kind (Some (unaux_kind (kopt_kind kopt)))) (quant_kopts typq) in
+  { ctx with type_constructors = Bindings.add id (kinds, to_parse_kind (Some kind)) ctx.type_constructors }
 
 let anon_rec_constructor_typ record_id = function
   | P.TypQ_aux (P.TypQ_no_forall, l) -> P.ATyp_aux (P.ATyp_id record_id, Generated l)
@@ -1585,9 +1635,13 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : untyped_
       let id = to_ast_reserved_type_id ctx id in
       begin
         match to_ast_bind ctx typq atyp kind_opt with
-        | Some (typq, typ_arg, kind) ->
+        | Some (typq, typ_arg, kind, inference_kinds) ->
             ( [DEF_aux (DEF_type (TD_aux (TD_abbrev (id, typq, typ_arg), (l, empty_uannot))), def_annot)],
-              add_constructor id typq (unaux_kind kind) ctx
+              {
+                ctx with
+                type_constructors =
+                  Bindings.add id (inference_kinds, to_parse_kind (Some (unaux_kind kind))) ctx.type_constructors;
+              }
             )
         | None ->
             raise
@@ -1629,11 +1683,11 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : untyped_
       )
   | P.TD_enum (id, fns, enums) ->
       let id = to_ast_reserved_type_id ctx id in
-      let ctx = { ctx with type_constructors = Bindings.add id ([], K_type) ctx.type_constructors } in
+      let ctx = { ctx with type_constructors = Bindings.add id ([], P.K_type) ctx.type_constructors } in
       let fns = generate_enum_functions l ctx id fns enums in
       let enums = List.map (fun e -> to_ast_id ctx (fst e)) enums in
       ( fns @ [DEF_aux (DEF_type (TD_aux (TD_enum (id, enums, false), (l, empty_uannot))), def_annot)],
-        { ctx with type_constructors = Bindings.add id ([], K_type) ctx.type_constructors }
+        { ctx with type_constructors = Bindings.add id ([], P.K_type) ctx.type_constructors }
       )
   | P.TD_abstract (id, kind) ->
       if not !opt_abstract_types then raise (Reporting.err_general l abstract_type_error);
@@ -1642,7 +1696,10 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : untyped_
         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 ([], unaux_kind kind) ctx.type_constructors }
+              {
+                ctx with
+                type_constructors = Bindings.add id ([], to_parse_kind (Some (unaux_kind kind))) ctx.type_constructors;
+              }
             )
         | None -> raise (Reporting.err_general l "Abstract type cannot have Order kind")
       end
@@ -1651,7 +1708,7 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : untyped_
       let typ = to_ast_typ ctx typ in
       let ranges = List.map (fun (id, range) -> (to_ast_id ctx id, to_ast_range ctx range)) ranges in
       ( [DEF_aux (DEF_type (TD_aux (TD_bitfield (id, typ, ranges), (l, empty_uannot))), def_annot)],
-        { ctx with type_constructors = Bindings.add id ([], K_type) ctx.type_constructors }
+        { ctx with type_constructors = Bindings.add id ([], P.K_type) ctx.type_constructors }
       )
 
 let to_ast_rec ctx (P.Rec_aux (r, l) : P.rec_opt) : uannot rec_opt =
@@ -2030,33 +2087,33 @@ let initial_ctx =
         (fun m (k, v) -> Bindings.add (mk_id k) v m)
         Bindings.empty
         [
-          ("bool", ([], K_type));
-          ("nat", ([], K_type));
-          ("int", ([], K_type));
-          ("unit", ([], K_type));
-          ("bit", ([], K_type));
-          ("string", ([], K_type));
-          ("string_literal", ([], K_type));
-          ("real", ([], K_type));
-          ("list", ([Some K_type], K_type));
-          ("register", ([Some K_type], K_type));
-          ("range", ([Some K_int; Some K_int], K_type));
-          ("bitvector", ([Some K_int; None], K_type));
-          ("vector", ([Some K_int; None; Some K_type], K_type));
-          ("atom", ([Some K_int], K_type));
-          ("atom_bool", ([Some K_bool], K_type));
-          ("implicit", ([Some K_int], K_type));
-          ("itself", ([Some K_int], K_type));
-          ("not", ([Some K_bool], K_bool));
-          ("ite", ([Some K_bool; Some K_int; Some K_int], K_int));
-          ("abs", ([Some K_int], K_int));
-          ("mod", ([Some K_int; Some K_int], K_int));
-          ("div", ([Some K_int; Some K_int], K_int));
-          ("float16", ([], K_type));
-          ("float32", ([], K_type));
-          ("float64", ([], K_type));
-          ("float128", ([], K_type));
-          ("float_rounding_mode", ([], K_type));
+          ("bool", ([], P.K_type));
+          ("nat", ([], P.K_type));
+          ("int", ([], P.K_type));
+          ("unit", ([], P.K_type));
+          ("bit", ([], P.K_type));
+          ("string", ([], P.K_type));
+          ("string_literal", ([], P.K_type));
+          ("real", ([], P.K_type));
+          ("list", ([P.K_type], P.K_type));
+          ("register", ([P.K_type], P.K_type));
+          ("range", ([P.K_int; P.K_int], P.K_type));
+          ("bitvector", ([P.K_nat; P.K_order], P.K_type));
+          ("vector", ([P.K_nat; P.K_order; P.K_type], P.K_type));
+          ("atom", ([P.K_int], P.K_type));
+          ("atom_bool", ([P.K_bool], P.K_type));
+          ("implicit", ([P.K_int], P.K_type));
+          ("itself", ([P.K_int], P.K_type));
+          ("not", ([P.K_bool], P.K_bool));
+          ("ite", ([P.K_bool; P.K_int; P.K_int], P.K_int));
+          ("abs", ([P.K_int], P.K_int));
+          ("mod", ([P.K_int; P.K_int], P.K_int));
+          ("div", ([P.K_int; P.K_int], P.K_int));
+          ("float16", ([], P.K_type));
+          ("float32", ([], P.K_type));
+          ("float64", ([], P.K_type));
+          ("float128", ([], P.K_type));
+          ("float_rounding_mode", ([], P.K_type));
         ];
     function_type_variables = Bindings.empty;
     kinds = KBindings.empty;
diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll
index a0710f654..8cf6941ed 100644
--- a/src/lib/lexer.mll
+++ b/src/lib/lexer.mll
@@ -108,9 +108,10 @@ let kw_table =
      ("let",                     (fun _ -> Let_));
      ("var",                     (fun _ -> Var));
      ("ref",                     (fun _ -> Ref));
-     ("Int",                     (fun _ -> Int));
-     ("Order",                   (fun _ -> Order));
-     ("Bool",                    (fun _ -> Bool));
+     ("Int",                     (fun _ -> INT));
+     ("Nat",                     (fun _ -> NAT));
+     ("Order",                   (fun _ -> ORDER));
+     ("Bool",                    (fun _ -> BOOL));
      ("pure",                    (fun _ -> Pure));
      ("impure",                  (fun _ -> Impure));
      ("monadic",                 (fun _ -> Monadic));
diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml
index 3ddf3f310..0fd9098b7 100644
--- a/src/lib/parse_ast.ml
+++ b/src/lib/parse_ast.ml
@@ -106,7 +106,8 @@ type ix = text (* infix identifier *)
 type kind_aux =
   | (* base kind *)
     K_type (* kind of types *)
-  | K_int (* kind of natural number size expressions *)
+  | K_int (* kind of integer type expressions *)
+  | K_nat (* kind of natural type expressions *)
   | K_order (* kind of vector order specifications *)
   | K_bool (* kind of constraints *)
 
diff --git a/src/lib/parser.mly b/src/lib/parser.mly
index a848928fc..13a03ba92 100644
--- a/src/lib/parser.mly
+++ b/src/lib/parser.mly
@@ -236,7 +236,7 @@ let set_syntax_deprecated l =
 /*Terminals with no content*/
 
 %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
-%token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast
+%token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ INT NAT ORDER BOOL Cast
 %token Pure Impure Monadic Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
 %token Undefined Union Newtype With Val Outcome Constraint Throw Try Catch Exit Bitfield Constant
 %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure Instantiation Impl Private
@@ -444,13 +444,15 @@ typ_list:
     { $1 :: $3 }
 
 kind:
-  | Int
+  | INT
     { K_aux (K_int, loc $startpos $endpos) }
+  | NAT
+    { K_aux (K_nat, loc $startpos $endpos) }
   | TYPE
     { K_aux (K_type, loc $startpos $endpos) }
-  | Order
+  | ORDER
     { K_aux (K_order, loc $startpos $endpos) }
-  | Bool
+  | BOOL
     { K_aux (K_bool, loc $startpos $endpos) }
 
 kid_list:
diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml
index c63b5ed06..07b56bed5 100644
--- a/src/lib/pretty_print_sail.ml
+++ b/src/lib/pretty_print_sail.ml
@@ -96,13 +96,11 @@ module Printer (Config : PRINT_CONFIG) = struct
     ^^ match def_annot.visibility with Private _ -> string "private" ^^ space | Public -> empty
 
   let doc_kopt_no_parens = function
-    | kopt when is_int_kopt kopt -> doc_kid (kopt_kid kopt)
+    | kopt when is_int_kopt kopt -> separate space [doc_kid (kopt_kid kopt); colon; string "Int"]
     | kopt when is_typ_kopt kopt -> separate space [doc_kid (kopt_kid kopt); colon; string "Type"]
     | kopt -> separate space [doc_kid (kopt_kid kopt); colon; string "Bool"]
 
-  let doc_kopt = function
-    | kopt when is_int_kopt kopt -> doc_kopt_no_parens kopt
-    | kopt -> parens (doc_kopt_no_parens kopt)
+  let doc_kopt kopt = parens (doc_kopt_no_parens kopt)
 
   let doc_int n = string (Big_int.to_string n)
 
diff --git a/src/lib/type_check.mli b/src/lib/type_check.mli
index 999fa322c..d6d45cf8f 100644
--- a/src/lib/type_check.mli
+++ b/src/lib/type_check.mli
@@ -239,7 +239,7 @@ module Env : sig
      environment is lacking even basic builtins. *)
   val empty : t
 
-  val builtin_typs : typquant Bindings.t
+  val builtin_typs : (typquant * kind_aux) Bindings.t
 
   val get_union_id : id -> t -> typquant * typ
 
diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml
index 654ca1b49..d85189b94 100644
--- a/src/lib/type_env.ml
+++ b/src/lib/type_env.ml
@@ -359,32 +359,42 @@ let k_name () =
 let kinds_typq kinds = mk_typquant (List.map (fun k -> mk_qi_id k (k_name ())) kinds)
 
 let builtin_typs =
+  let k_counter = ref 0 in
+  let k_name () =
+    let kid = mk_kid ("k#" ^ string_of_int !k_counter) in
+    incr k_counter;
+    kid
+  in
+  let kinds_typq kinds = mk_typquant (List.map (fun k -> mk_qi_id k (k_name ())) kinds) in
   List.fold_left
-    (fun m (name, kinds) -> Bindings.add (mk_id name) (kinds_typq kinds) m)
+    (fun m (name, parameter_kinds, kind) -> Bindings.add (mk_id name) (kinds_typq parameter_kinds, kind) m)
     Bindings.empty
     [
-      ("range", [K_int; K_int]);
-      ("atom", [K_int]);
-      ("implicit", [K_int]);
-      ("vector", [K_int; K_type]);
-      ("bitvector", [K_int]);
-      ("register", [K_type]);
-      ("bit", []);
-      ("unit", []);
-      ("int", []);
-      ("nat", []);
-      ("bool", []);
-      ("real", []);
-      ("list", [K_type]);
-      ("string", []);
-      ("string_literal", []);
-      ("itself", [K_int]);
-      ("atom_bool", [K_bool]);
-      ("float16", []);
-      ("float32", []);
-      ("float64", []);
-      ("float128", []);
-      ("float_rounding_mode", []);
+      ("range", [K_int; K_int], K_type);
+      ("atom", [K_int], K_type);
+      ("implicit", [K_int], K_type);
+      ("vector", [K_int; K_type], K_type);
+      ("bitvector", [K_int], K_type);
+      ("register", [K_type], K_type);
+      ("bit", [], K_type);
+      ("unit", [], K_type);
+      ("int", [], K_type);
+      ("nat", [], K_type);
+      ("bool", [], K_type);
+      ("real", [], K_type);
+      ("list", [K_type], K_type);
+      ("string", [], K_type);
+      ("string_literal", [], K_type);
+      ("itself", [K_int], K_type);
+      ("atom_bool", [K_bool], K_type);
+      ("float16", [], K_type);
+      ("float32", [], K_type);
+      ("float64", [], K_type);
+      ("float128", [], K_type);
+      ("float_rounding_mode", [], K_type);
+      ("abs", [K_int], K_int);
+      ("mod", [K_int; K_int], K_int);
+      ("div", [K_int; K_int], K_int);
     ]
 
 let bound_typ_id env id =
@@ -530,91 +540,61 @@ let add_filtered_overload original_id ids env =
 let infer_kind env id =
   let l = id_loc id in
   if Bindings.mem id builtin_typs then Bindings.find id builtin_typs
-  else if Bindings.mem id env.global.unions then fst (get_item l env (Bindings.find id env.global.unions))
-  else if Bindings.mem id env.global.records then fst (get_item l env (Bindings.find id env.global.records))
-  else if Bindings.mem id env.global.enums then mk_typquant []
-  else if Bindings.mem id env.global.synonyms then
-    typ_error (id_loc id) ("Cannot infer kind of type synonym " ^ string_of_id id)
-  else if Bindings.mem id env.global.abstract_typs then mk_typquant []
+  else if Bindings.mem id env.global.unions then (fst (get_item l env (Bindings.find id env.global.unions)), K_type)
+  else if Bindings.mem id env.global.records then (fst (get_item l env (Bindings.find id env.global.records)), K_type)
+  else if Bindings.mem id env.global.enums then (mk_typquant [], K_type)
+  else if Bindings.mem id env.global.synonyms then (
+    let typq, arg = get_item l env (Bindings.find id env.global.synonyms) in
+    (typq, unaux_kind (typ_arg_kind arg))
+  )
+  else if Bindings.mem id env.global.abstract_typs then (
+    let kind = get_item l env (Bindings.find id env.global.abstract_typs) in
+    (mk_typquant [], unaux_kind kind)
+  )
   else typ_error (id_loc id) ("Cannot infer kind of " ^ string_of_id id)
 
-let check_args_typquant id env args typq =
-  let kopts, ncs = quant_split typq in
-  let rec subst_args kopts args =
-    match (kopts, args) with
-    | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_int_kopt kopt ->
-        List.map (constraint_subst (kopt_kid kopt) arg) (subst_args kopts args)
-    | kopt :: kopts, A_aux (A_typ _, _) :: args when is_typ_kopt kopt -> subst_args kopts args
-    | kopt :: kopts, A_aux (A_bool _, _) :: args when is_bool_kopt kopt -> subst_args kopts args
-    | [], [] -> ncs
-    | _, A_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
-    | _, _ -> typ_error Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
-  in
-  let ncs = subst_args kopts args in
-  if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then ()
-  else
-    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.constraints @ List.map snd env.global.constraints
 let get_global_constraints env = List.map snd env.global.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
-  let ncs =
-    List.map
-      (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts)
-      ncs
-  in
-  let typ_arg =
-    List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts
-  in
-  let kopts = List.map snd kopts in
-  let rec subst_args env l kopts args =
-    match (kopts, args) with
-    | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt ->
-        let typ_arg, ncs = subst_args env l kopts args in
-        ( typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg,
-          List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs
-        )
-    | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt ->
-        let typ_arg, ncs = subst_args env l kopts args in
-        (typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs)
-    | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt ->
-        let typ_arg, ncs = subst_args env l kopts args in
-        (typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs)
-    | [], [] -> (typ_arg, ncs)
-    | kopts, args ->
-        typ_error l
-          ("Synonym applied to bad arguments "
-          ^ Util.string_of_list ", " string_of_kinded_id kopts
-          ^ Util.string_of_list ", " string_of_typ_arg args
+module Well_formedness = struct
+  type existential = { vars : KidSet.t; constr : n_constraint option }
+
+  let no_existential = { vars = KidSet.empty; constr = None }
+
+  let with_existential exs =
+    match exs.constr with Some ex_constraint -> fun c -> nc_or (nc_not ex_constraint) c | None -> fun c -> c
+
+  let check_args_typquant id exs env args typq =
+    let kopts, ncs = quant_split typq in
+    let rec subst_args kopts args =
+      match (kopts, args) with
+      | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_int_kopt kopt ->
+          List.map (constraint_subst (kopt_kid kopt) arg) (subst_args kopts args)
+      | kopt :: kopts, A_aux (A_typ _, _) :: args when is_typ_kopt kopt -> subst_args kopts args
+      | kopt :: kopts, A_aux (A_bool _, _) :: args when is_bool_kopt kopt -> subst_args kopts args
+      | [], [] -> ncs
+      | _, A_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
+      | _, _ -> typ_error Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
+    in
+    let ncs = subst_args kopts args in
+    let unproven =
+      match env.prove with
+      | Some prove -> List.filter (fun nc -> not (prove env (with_existential exs nc))) ncs
+      | None -> ncs
+    in
+    match unproven with
+    | [] -> ()
+    | ncs ->
+        typ_error (id_loc id)
+          ("Could not prove "
+          ^ string_of_list ", " string_of_n_constraint ncs
+          ^ " for type constructor " ^ string_of_id id
           )
-  in
-  fun l env args ->
-    let typ_arg, ncs = subst_args env l kopts args in
-    if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then typ_arg
-    else
-      typ_error l
-        ("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 (get_constraints env)
-        )
-
-let get_typ_synonym id env =
-  match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.synonyms) with
-  | Some (typq, arg) -> mk_synonym typq arg
-  | None -> raise Not_found
-
-let get_typ_synonyms env = filter_items env env.global.synonyms
 
-module Well_formedness = struct
   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)))
+      (lazy ("wf_" ^ str ^ ": " ^ f x ^ " exs: " ^ Util.string_of_list ", " string_of_kid (KidSet.elements exs.vars)))
   [@@coverage off]
 
   (* Check if a type, order, n-expression or constraint is
@@ -622,9 +602,21 @@ module Well_formedness = struct
   let rec wf_typ exs 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
+        let typq, k = infer_kind env id in
+        begin
+          match k with
+          | K_type -> ()
+          | _ ->
+              typ_error l
+                (string_of_id id ^ " has kind " ^ string_of_kind_aux k
+               ^ " but was used in a place where a type was expected"
+                )
+        end;
         if not (Util.list_empty (quant_kopts typq)) then
-          typ_error l ("Type constructor " ^ string_of_id id ^ " expected " ^ string_of_typquant typq)
+          typ_error l
+            ("Type constructor " ^ string_of_id id ^ " expected arguments " ^ string_of_typquant typq
+           ^ ", but was used here with none"
+            )
         else ()
     | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id)
     | Typ_var kid -> begin
@@ -647,15 +639,41 @@ module Well_formedness = struct
         wf_typ exs env typ1;
         wf_typ exs env typ2
     | Typ_tuple typs -> List.iter (wf_typ exs env) typs
+    | Typ_app (id, [A_aux (A_nexp nexp, _)]) when string_of_id id = "bitvector" ->
+        wf_nexp exs env nexp;
+        begin
+          match env.prove with
+          | Some prove ->
+              let with_existential =
+                match exs.constr with
+                | Some ex_constraint -> fun c -> nc_or (nc_not ex_constraint) c
+                | None -> fun c -> c
+              in
+              if not (prove env (with_existential (nc_gteq nexp (nint 0)))) then
+                typ_error l "Bitvector index must be greater than or equal to zero"
+          | None -> Reporting.unreachable l __POS__ "No prover in environment when checking well-formedness"
+        end
     | Typ_app (id, [(A_aux (A_nexp _, _) as arg)]) when string_of_id id = "implicit" -> wf_typ_arg exs env arg
     | Typ_app (id, args) when bound_typ_id env id ->
         List.iter (wf_typ_arg exs env) args;
-        check_args_typquant id env args (infer_kind env id)
+        let typq, k = infer_kind env id in
+        begin
+          match k with
+          | K_type -> ()
+          | _ ->
+              typ_error l
+                (string_of_id id ^ " has kind " ^ string_of_kind_aux k
+               ^ " but was used in a place where a type was expected"
+                )
+        end;
+        check_args_typquant id exs env args typq
     | Typ_app (id, _) -> typ_error l ("Undefined type " ^ string_of_id id)
     | Typ_exist ([], _, _) -> typ_error l "Existential must have some type variables"
-    | Typ_exist (kopts, nc, typ) when KidSet.is_empty exs ->
-        wf_constraint (KidSet.of_list (List.map kopt_kid kopts)) env nc;
-        wf_typ (KidSet.of_list (List.map kopt_kid kopts)) env typ
+    | Typ_exist (kopts, nc, typ) when KidSet.is_empty exs.vars ->
+        let vars = KidSet.of_list (List.map kopt_kid kopts) in
+        wf_constraint { vars; constr = None } env nc;
+        let env = List.fold_right (add_typ_var l) kopts env in
+        wf_typ { vars; constr = Some nc } env typ
     | Typ_exist (_, _, _) -> typ_error l "Nested existentials are not allowed"
     | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" [@coverage off]
 
@@ -669,8 +687,24 @@ module Well_formedness = struct
     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_id id when bound_typ_id env id ->
+        let typq, k = infer_kind env id in
+        begin
+          match k with
+          | K_int -> ()
+          | _ ->
+              typ_error l
+                (string_of_id id ^ " has kind " ^ string_of_kind_aux k
+               ^ " but was used in a place where a type-level number was expected"
+                )
+        end;
+        if not (Util.list_empty (quant_kopts typq)) then
+          typ_error l
+            ("Numeric type constructor " ^ string_of_id id ^ " expected arguments " ^ string_of_typquant typq
+           ^ ", but was used here with none"
+            )
+    | Nexp_id id -> typ_error l ("Undefined numeric type " ^ string_of_id id)
+    | Nexp_var kid when KidSet.mem kid exs.vars -> ()
     | Nexp_var kid -> begin
         match get_typ_var kid env with
         | K_int -> ()
@@ -681,12 +715,19 @@ module Well_formedness = struct
               )
       end
     | Nexp_constant _ -> ()
-    | Nexp_app (id, nexps) ->
-        let name = string_of_id id in
-        (* We allow the abs, mod, and div functions that are included in the SMTLIB2 integer theory *)
-        if name = "abs" || name = "mod" || name = "div" || Bindings.mem id env.global.synonyms then
-          List.iter (fun n -> wf_nexp exs env n) nexps
-        else typ_error l ("Unknown type level operator or function " ^ name)
+    | Nexp_app (id, nexps) when bound_typ_id env id ->
+        let typq, k = infer_kind env id in
+        begin
+          match k with
+          | K_int -> ()
+          | _ ->
+              typ_error l
+                (string_of_id id ^ " has kind " ^ string_of_kind_aux k
+               ^ " but was used in a place where a type-level number was expected"
+                )
+        end;
+        List.iter (fun n -> wf_nexp exs env n) nexps
+    | Nexp_app (id, _) -> typ_error l ("Unknown type level numeric operator or function " ^ string_of_id id)
     | Nexp_times (nexp1, nexp2) | Nexp_sum (nexp1, nexp2) | Nexp_minus (nexp1, nexp2) ->
         wf_nexp exs env nexp1;
         wf_nexp exs env nexp2
@@ -697,11 +738,27 @@ module Well_formedness = struct
         wf_nexp exs env t;
         wf_nexp exs env e
 
-  and wf_constraint exs env (NC_aux (nc_aux, l) as nc) =
+  and wf_constraint (exs : existential) 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_id id when bound_typ_id env id ->
+        let typq, k = infer_kind env id in
+        begin
+          match k with
+          | K_bool -> ()
+          | _ ->
+              typ_error l
+                (string_of_id id ^ " has kind " ^ string_of_kind_aux k
+               ^ " but was used in a place where a constraint was expected"
+                )
+        end;
+        if not (Util.list_empty (quant_kopts typq)) then
+          typ_error l
+            ("Constraint " ^ string_of_id id ^ " expected arguments " ^ string_of_typquant typq
+           ^ ", but was used here with none"
+            )
+    | NC_id id -> typ_error l ("Undefined type constraint " ^ string_of_id id)
     | NC_equal (arg1, arg2) | NC_not_equal (arg1, arg2) ->
         wf_typ_arg exs env arg1;
         wf_typ_arg exs env arg2
@@ -713,7 +770,7 @@ module Well_formedness = struct
         wf_constraint exs env nc1;
         wf_constraint exs env nc2
     | NC_app (_, args) -> List.iter (wf_typ_arg exs env) args
-    | NC_var kid when KidSet.mem kid exs -> ()
+    | NC_var kid when KidSet.mem kid exs.vars -> ()
     | NC_var kid -> begin
         match get_typ_var kid env with
         | K_bool -> ()
@@ -722,6 +779,57 @@ module Well_formedness = struct
     | NC_true | NC_false -> ()
 end
 
+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
+  let ncs =
+    List.map
+      (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts)
+      ncs
+  in
+  let typ_arg =
+    List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts
+  in
+  let kopts = List.map snd kopts in
+  let rec subst_args env l kopts args =
+    match (kopts, args) with
+    | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt ->
+        let typ_arg, ncs = subst_args env l kopts args in
+        ( typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg,
+          List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs
+        )
+    | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt ->
+        let typ_arg, ncs = subst_args env l kopts args in
+        (typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs)
+    | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt ->
+        let typ_arg, ncs = subst_args env l kopts args in
+        (typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs)
+    | [], [] -> (typ_arg, ncs)
+    | kopts, args ->
+        typ_error l
+          ("Synonym applied to bad arguments "
+          ^ Util.string_of_list ", " string_of_kinded_id kopts
+          ^ Util.string_of_list ", " string_of_typ_arg args
+          )
+  in
+  fun l env args ->
+    let typ_arg, ncs = subst_args env l kopts args in
+    if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then typ_arg
+    else
+      typ_error l
+        ("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 (get_constraints env)
+        )
+
+let get_typ_synonym id env =
+  match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.synonyms) with
+  | Some (typq, arg) -> mk_synonym typq arg
+  | None -> raise Not_found
+
+let get_typ_synonyms env = filter_items env env.global.synonyms
+
 let add_abstract_typ id kind env =
   if bound_typ_id env id then
     typ_error (id_loc id)
@@ -870,8 +978,8 @@ and expand_arg_synonyms env (A_aux (typ_arg, l)) =
   | A_nexp nexp -> A_aux (A_nexp (expand_nexp_synonyms env nexp |> nexp_simp), l)
 
 and add_constraint ?(global = false) ?reason constr env =
+  Well_formedness.wf_constraint Well_formedness.no_existential env constr;
   let (NC_aux (nc_aux, l) as constr) = constraint_simp (expand_constraint_synonyms env constr) in
-  Well_formedness.wf_constraint KidSet.empty env constr;
   let power_vars = constraint_power_variables constr in
   if KidSet.cardinal power_vars > 1 && !opt_smt_linearize then
     typ_error l
@@ -920,11 +1028,10 @@ and add_constraint ?(global = false) ?reason constr env =
   )
 
 let wf_typ ~at:at_l env (Typ_aux (_, l) as typ) =
-  let typ = expand_synonyms env typ in
-  Well_formedness.wf_debug "typ" string_of_typ typ KidSet.empty;
+  Well_formedness.wf_debug "typ" string_of_typ typ Well_formedness.no_existential;
   incr depth;
   try
-    Well_formedness.wf_typ KidSet.empty env typ;
+    Well_formedness.wf_typ Well_formedness.no_existential env typ;
     decr depth
   with Type_error (err_l, err) ->
     decr depth;
@@ -932,11 +1039,10 @@ let wf_typ ~at:at_l env (Typ_aux (_, l) as typ) =
     typ_raise l (err_because (Err_other ("Well-formedness check failed for type" ^ extra), err_l, err))
 
 let wf_constraint ~at:at_l env (NC_aux (_, l) as nc) =
-  let nc = expand_constraint_synonyms env nc in
-  Well_formedness.wf_debug "constraint" string_of_n_constraint nc KidSet.empty;
+  Well_formedness.wf_debug "constraint" string_of_n_constraint nc Well_formedness.no_existential;
   incr depth;
   try
-    Well_formedness.wf_constraint KidSet.empty env nc;
+    Well_formedness.wf_constraint Well_formedness.no_existential env nc;
     decr depth
   with Type_error (err_l, err) ->
     decr depth;
@@ -958,13 +1064,16 @@ let add_typ_synonym id typq arg env =
     typ_error (id_loc id)
       ("Cannot define type synonym " ^ string_of_id id ^ ", as a type or synonym with that name already exists")
   else (
-    let typq =
-      quant_map_items
-        (function
-          | QI_aux (QI_constraint nexp, aux) -> QI_aux (QI_constraint (expand_constraint_synonyms env nexp), aux)
-          | quant_item -> quant_item
-          )
-        typq
+    let _, typq =
+      quant_fold_map_items
+        (fun env quant_item ->
+          match quant_item with
+          | QI_aux (QI_constraint constr, l) ->
+              let constr = expand_constraint_synonyms env constr in
+              (add_constraint constr env, QI_aux (QI_constraint constr, l))
+          | QI_aux (QI_id kopt, l) -> (add_typ_var l kopt env, quant_item)
+        )
+        env typq
     in
     typ_print
       ( lazy
diff --git a/src/lib/type_env.mli b/src/lib/type_env.mli
index 3648030eb..dbd11ce2b 100644
--- a/src/lib/type_env.mli
+++ b/src/lib/type_env.mli
@@ -270,4 +270,4 @@ val set_prover : (t -> n_constraint -> bool) option -> t -> t
    sets up a correct initial environment. *)
 val empty : t
 
-val builtin_typs : typquant Bindings.t
+val builtin_typs : (typquant * kind_aux) Bindings.t
diff --git a/src/lib/type_error.ml b/src/lib/type_error.ml
index 9e7bd060f..bc72b112d 100644
--- a/src/lib/type_error.ml
+++ b/src/lib/type_error.ml
@@ -371,6 +371,16 @@ let message_of_type_error type_error =
         end
     | Err_instantiation_info (_, err) -> to_message err
     | Err_unresolved_quants (id, quants, locals, tyvars, ncs) ->
+        let quants =
+          List.filter_map
+            (function
+              | QI_aux (QI_id _, _) as quant -> Some quant
+              | QI_aux (QI_constraint nc, _) as quant -> (
+                  match constraint_simp nc with NC_aux (NC_true, _) -> None | _ -> Some quant
+                )
+              )
+            quants
+        in
         ( Seq
             [
               Line ("Could not resolve quantifiers for " ^ string_of_id id);
diff --git a/src/sail_doc_backend/html_source.ml b/src/sail_doc_backend/html_source.ml
index a3b7eafdd..d7a28e62b 100644
--- a/src/sail_doc_backend/html_source.ml
+++ b/src/sail_doc_backend/html_source.ml
@@ -98,7 +98,7 @@ let highlights ~filename ~contents =
     | Id _ ->
         mark Highlight.Id;
         go ()
-    | Int | Bool | TYPE | Order ->
+    | INT | NAT | BOOL | TYPE | ORDER ->
         mark Highlight.Kind;
         go ()
     | String _ ->
diff --git a/src/sail_ocaml_backend/ocaml_backend.ml b/src/sail_ocaml_backend/ocaml_backend.ml
index 500b73ccf..0480abd9a 100644
--- a/src/sail_ocaml_backend/ocaml_backend.ml
+++ b/src/sail_ocaml_backend/ocaml_backend.ml
@@ -917,7 +917,7 @@ let ocaml_pp_generators ctx defs orig_types required =
           | TD_abbrev (_, _, _) -> assert false
           | TD_bitfield _ -> assert false
         )
-      | exception Not_found -> Bindings.find id Type_check.Env.builtin_typs
+      | exception Not_found -> fst (Bindings.find id Type_check.Env.builtin_typs)
     in
     let tquants = quant_kopts allquants in
     let gen_tyvars = List.map (fun k -> kopt_kid k |> zencode_kid) (List.filter is_typ_kopt tquants) in
diff --git a/test/c/get_slice_int.sail b/test/c/get_slice_int.sail
index ac19cf9d2..0abd940af 100644
--- a/test/c/get_slice_int.sail
+++ b/test/c/get_slice_int.sail
@@ -3,7 +3,7 @@ $include <prelude.sail>
 
 /* Use functions to hide the fact that these are really small constants, so they are forced to be represented as big ints */
 
-val big_five : unit -> int
+val big_five : unit -> nat
 
 function big_five() = 5
 
diff --git a/test/c/int_struct.sail b/test/c/int_struct.sail
index 9e9099029..86249cf12 100644
--- a/test/c/int_struct.sail
+++ b/test/c/int_struct.sail
@@ -5,7 +5,7 @@ $include <prelude.sail>
 $[sv_module { stdout = true }]
 val print = "print_endline" : string -> unit
 
-struct Foo('n: Int) = {
+struct Foo('n) = {
   field: bits('n)
 }
 
diff --git a/test/c/int_struct_constrained.sail b/test/c/int_struct_constrained.sail
index c5b8beabb..c9a81c741 100644
--- a/test/c/int_struct_constrained.sail
+++ b/test/c/int_struct_constrained.sail
@@ -5,7 +5,7 @@ $include <prelude.sail>
 $[sv_module { stdout = true }]
 val print = "print_endline" : string -> unit
 
-struct Foo('n: Int), 'n <= 64 = {
+struct Foo('n: Int), 0 <= 'n <= 64 = {
   field: bits('n)
 }
 
diff --git a/test/c/issue429.sail b/test/c/issue429.sail
index f6c2b2235..61f8deeb7 100644
--- a/test/c/issue429.sail
+++ b/test/c/issue429.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-union two_bitvectors('n : Int) = {
+union two_bitvectors('n) = {
     BV1 : bits('n),
     BV2 : bits('n),
 }
diff --git a/test/c/stack_struct.sail b/test/c/stack_struct.sail
index 08c3f9639..2b8b40928 100644
--- a/test/c/stack_struct.sail
+++ b/test/c/stack_struct.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $sail_internal
 
-type bits ('n : Int) = bitvector('n, dec)
+type bits('n) = bitvector('n, dec)
 
 union option ('a : Type) = {
   Some : 'a,
diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail
index 8f8fef496..c5cf400b0 100644
--- a/test/ocaml/reg_ref/rr.sail
+++ b/test/ocaml/reg_ref/rr.sail
@@ -33,7 +33,7 @@ overload _mod_GPR = { rGPR, wGPR }
 /* Create a new type which is a pair of a bitvector and a start index
 
    slice('n, 'm) is equivalent to old-sail vector('n, 'm, dec, bit) */
-newtype slice ('n : Int, 'm : Int) = MkSlice : (atom('n), bits('m))
+newtype slice ('n : Int, 'm : Nat) = MkSlice : (atom('n), bits('m))
 
 /* Extract the bitvector from a slice */
 val slice_bits : forall 'n 'm. slice('n, 'm) -> bits('m)
diff --git a/test/typecheck/fail/add_vec_lit_old.expect b/test/typecheck/fail/add_vec_lit_old.expect
index 98da899d1..b0a1aacb7 100644
--- a/test/typecheck/fail/add_vec_lit_old.expect
+++ b/test/typecheck/fail/add_vec_lit_old.expect
@@ -1,5 +1,5 @@
 Warning: Deprecated fail/add_vec_lit_old.sail:9.4-8:
-9 |val cast unsigned : forall ('n : Int).
+9 |val cast unsigned : forall 'n.
   |    ^--^
   | 
 Cast annotations are deprecated. They will be removed in a future version of the language.
diff --git a/test/typecheck/fail/add_vec_lit_old.sail b/test/typecheck/fail/add_vec_lit_old.sail
index cb0054765..af18c2e7e 100644
--- a/test/typecheck/fail/add_vec_lit_old.sail
+++ b/test/typecheck/fail/add_vec_lit_old.sail
@@ -1,12 +1,12 @@
 default Order inc
 
-val add_vec = impure {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
+val add_vec = impure {ocaml: "add_vec", lem: "add_vec"}: forall 'n.
   (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
-val add_range = impure {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = impure {ocaml: "add_range", lem: "add_range"}: forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val cast unsigned : forall ('n : Int).
+val cast unsigned : forall 'n.
   bitvector('n, inc) -> range(0, 2 ^ 'n - 1)
 
 overload operator + = {add_vec, add_range}
diff --git a/test/typecheck/fail/bitfield_error.expect b/test/typecheck/fail/bitfield_error.expect
index b053b7bd0..ce0080cde 100644
--- a/test/typecheck/fail/bitfield_error.expect
+++ b/test/typecheck/fail/bitfield_error.expect
@@ -10,5 +10,6 @@
   | Bitfield error fail/bitfield_error.sail:6.6-13:
   | 6 |  b : 0 .. 15,
   |   |      ^-----^
-  |   | Could not resolve quantifiers for subrange_bits
-  |   | * (0 <= 15 & (15 <= 0 & 0 < 15))
+  |   | Well-formedness check failed for type here
+  |   | 
+  |   | Bitvector index must be greater than or equal to zero
diff --git a/test/typecheck/fail/missing_tick.expect b/test/typecheck/fail/missing_tick.expect
index 5218dff5d..80c023408 100644
--- a/test/typecheck/fail/missing_tick.expect
+++ b/test/typecheck/fail/missing_tick.expect
@@ -12,4 +12,4 @@
   |   | Caused by fail/missing_tick.sail:5.16-17:
   |   | 5 |type foo = bits(x)
   |   |   |                ^
-  |   |   | Undefined type synonym x
+  |   |   | Undefined numeric type x
diff --git a/test/typecheck/fail/negative_bits_existential.expect b/test/typecheck/fail/negative_bits_existential.expect
index 5e9bbd84e..8f91dd007 100644
--- a/test/typecheck/fail/negative_bits_existential.expect
+++ b/test/typecheck/fail/negative_bits_existential.expect
@@ -1,5 +1,17 @@
 Type error:
-fail/negative_bits_existential.sail:12.17-26:
-12 |    let x: Foo = undefined;
-   |                 ^-------^
-   | Type Foo cannot be undefined
+fail/negative_bits_existential.sail:5.0-7.1:
+5 |struct Foo = {
+  |^-------------
+7 |}
+  |^
+  | Types are not well-formed within this type definition. Note that recursive types are forbidden.
+  | 
+  | Caused by fail/negative_bits_existential.sail:6.8-32:
+  | 6 |    xs: {'n, 'n == -1. bits('n)}
+  |   |        ^----------------------^
+  |   | Well-formedness check failed for type
+  |   | 
+  |   | Caused by fail/negative_bits_existential.sail:6.23-27:
+  |   | 6 |    xs: {'n, 'n == -1. bits('n)}
+  |   |   |                       ^--^
+  |   |   | Could not prove 'n >= 0 for type constructor bits
diff --git a/test/typecheck/fail/negative_bits_list.expect b/test/typecheck/fail/negative_bits_list.expect
new file mode 100644
index 000000000..44392d38a
--- /dev/null
+++ b/test/typecheck/fail/negative_bits_list.expect
@@ -0,0 +1,10 @@
+Type error:
+fail/negative_bits_list.sail:8.11-25:
+8 |    let x: list(bits(-1)) = [||];
+  |           ^------------^
+  | Well-formedness check failed for type
+  | 
+  | Caused by fail/negative_bits_list.sail:8.16-20:
+  | 8 |    let x: list(bits(-1)) = [||];
+  |   |                ^--^
+  |   | Could not prove -1 >= 0 for type constructor bits
diff --git a/test/typecheck/pass/negative_bits_list.sail b/test/typecheck/fail/negative_bits_list.sail
similarity index 100%
rename from test/typecheck/pass/negative_bits_list.sail
rename to test/typecheck/fail/negative_bits_list.sail
diff --git a/test/typecheck/fail/negative_bits_struct.expect b/test/typecheck/fail/negative_bits_struct.expect
index f6c309fda..a7b09249f 100644
--- a/test/typecheck/fail/negative_bits_struct.expect
+++ b/test/typecheck/fail/negative_bits_struct.expect
@@ -1,5 +1,10 @@
 Type error:
-fail/negative_bits_struct.sail:14.24-33:
+fail/negative_bits_struct.sail:14.11-21:
 14 |    let x: synonym(1) = undefined;
-   |                        ^-------^
-   | Type synonym(1) cannot be undefined
+   |           ^--------^
+   | Well-formedness check failed for type
+   | 
+   | Caused by fail/negative_bits_struct.sail:14.11-18:
+   | 14 |    let x: synonym(1) = undefined;
+   |    |           ^-----^
+   |    | Could not prove 1 >= 2 for type constructor synonym
diff --git a/test/typecheck/fail/negative_bits_struct.sail b/test/typecheck/fail/negative_bits_struct.sail
index 9507cf1cb..54cc51fb2 100644
--- a/test/typecheck/fail/negative_bits_struct.sail
+++ b/test/typecheck/fail/negative_bits_struct.sail
@@ -2,11 +2,11 @@ default Order dec
 
 $include <prelude.sail>
 
-struct Foo('n: Int) = {
+struct Foo('n), 'n >= 2 = {
     xs: bits('n - 2)
 }
 
-type synonym('n: Int) = Foo('n)
+type synonym('n: Int), 'n >= 2 = Foo('n)
 
 val foo : unit -> unit
 
diff --git a/test/typecheck/fail/negative_bits_struct2.expect b/test/typecheck/fail/negative_bits_struct2.expect
index 49010a5a8..d16c472dd 100644
--- a/test/typecheck/fail/negative_bits_struct2.expect
+++ b/test/typecheck/fail/negative_bits_struct2.expect
@@ -1,5 +1,17 @@
 Type error:
-fail/negative_bits_struct2.sail:12.17-26:
-12 |    let x: Foo = undefined;
-   |                 ^-------^
-   | Type Foo cannot be undefined
+fail/negative_bits_struct2.sail:5.0-7.1:
+5 |struct Foo = {
+  |^-------------
+7 |}
+  |^
+  | Types are not well-formed within this type definition. Note that recursive types are forbidden.
+  | 
+  | Caused by fail/negative_bits_struct2.sail:6.8-16:
+  | 6 |    xs: bits(-3)
+  |   |        ^------^
+  |   | Well-formedness check failed for type
+  |   | 
+  |   | Caused by fail/negative_bits_struct2.sail:6.8-12:
+  |   | 6 |    xs: bits(-3)
+  |   |   |        ^--^
+  |   |   | Could not prove -3 >= 0 for type constructor bits
diff --git a/test/typecheck/fail/negative_bits_tuple.expect b/test/typecheck/fail/negative_bits_tuple.expect
index 553f35f1e..ed5f89ab8 100644
--- a/test/typecheck/fail/negative_bits_tuple.expect
+++ b/test/typecheck/fail/negative_bits_tuple.expect
@@ -1,5 +1,10 @@
 Type error:
-fail/negative_bits_tuple.sail:8.29-38:
+fail/negative_bits_tuple.sail:8.11-26:
 8 |    let x: (bits(-1), int) = undefined;
-  |                             ^-------^
-  | Type (bits(-1), int) could be empty
+  |           ^-------------^
+  | Well-formedness check failed for type
+  | 
+  | Caused by fail/negative_bits_tuple.sail:8.12-16:
+  | 8 |    let x: (bits(-1), int) = undefined;
+  |   |            ^--^
+  |   | Could not prove -1 >= 0 for type constructor bits
diff --git a/test/typecheck/fail/negative_bits_union.expect b/test/typecheck/fail/negative_bits_union.expect
index e78b32efb..82d597497 100644
--- a/test/typecheck/fail/negative_bits_union.expect
+++ b/test/typecheck/fail/negative_bits_union.expect
@@ -1,5 +1,5 @@
 Type error:
-fail/negative_bits_union.sail:12.20-29:
-12 |    let x: Foo(1) = undefined;
-   |                    ^-------^
-   | Type Foo(1) cannot be undefined
+fail/negative_bits_union.sail:6.10-22:
+6 |    Bar : bits('n - 2),
+  |          ^----------^
+  | Could not prove constraints ('n - 2) >= 0 in type synonym bitvector(('n - 2)) with 
diff --git a/test/typecheck/fail/negative_bits_union2.expect b/test/typecheck/fail/negative_bits_union2.expect
index b0bac9e6c..36f8e6cd3 100644
--- a/test/typecheck/fail/negative_bits_union2.expect
+++ b/test/typecheck/fail/negative_bits_union2.expect
@@ -1,5 +1,5 @@
 Type error:
-fail/negative_bits_union2.sail:15.20-29:
-15 |    let x: Foo(1) = undefined;
-   |                    ^-------^
-   | Type Foo(1) cannot be undefined
+fail/negative_bits_union2.sail:8.10-22:
+8 |    Bar : bits('n - 2),
+  |          ^----------^
+  | Could not prove constraints ('n - 2) >= 0 in type synonym bitvector(('n - 2)) with 
diff --git a/test/typecheck/fail/non_synonym.expect b/test/typecheck/fail/non_synonym.expect
index 32b27ea71..53e654f4c 100644
--- a/test/typecheck/fail/non_synonym.expect
+++ b/test/typecheck/fail/non_synonym.expect
@@ -7,4 +7,4 @@
   | Caused by fail/non_synonym.sail:6.23-26:
   | 6 |let my_vector : vector(max, dec, int) = [1, 2, 3, 4, 5, 6]
   |   |                       ^-^
-  |   | Undefined type synonym max
+  |   | Undefined numeric type max
diff --git a/test/typecheck/fail/procstate1.expect b/test/typecheck/fail/procstate1.expect
index f3c402190..e9e365b67 100644
--- a/test/typecheck/fail/procstate1.expect
+++ b/test/typecheck/fail/procstate1.expect
@@ -1,5 +1,17 @@
 Type error:
-fail/procstate1.sail:14.0-30:
-14 |register PSTATE : ProcState(1)
-   |^----------------------------^
-   | Must provide a default register value for a register of type ProcState(1)
+fail/procstate1.sail:7.0-12.1:
+7  |struct ProcState('n : Int) = {
+   |^-----------------------------
+12 |}
+   |^
+   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
+   | 
+   | Caused by fail/procstate1.sail:8.6-24:
+   | 8 |  N : bitvector('n, dec),
+   |   |      ^----------------^
+   |   | Well-formedness check failed for type
+   |   | 
+   |   | Caused by fail/procstate1.sail:8.6-24:
+   |   | 8 |  N : bitvector('n, dec),
+   |   |   |      ^----------------^
+   |   |   | Bitvector index must be greater than or equal to zero
diff --git a/test/typecheck/fail/procstate1.sail b/test/typecheck/fail/procstate1.sail
index 250b9aaff..0a1736ed9 100644
--- a/test/typecheck/fail/procstate1.sail
+++ b/test/typecheck/fail/procstate1.sail
@@ -4,7 +4,7 @@ infix 4 ==
 
 val operator == = pure {lem: "eq_vec"} : forall 'n. (bitvector('n, dec), bitvector('n, dec)) -> bool
 
-struct ProcState ('n : Int) = {
+struct ProcState('n : Int) = {
   N : bitvector('n, dec),
   Z : bitvector(1, dec),
   C : bitvector(1, dec),
diff --git a/test/typecheck/fail/tuple_lexp1.expect b/test/typecheck/fail/tuple_lexp1.expect
index f5532423b..046070d21 100644
--- a/test/typecheck/fail/tuple_lexp1.expect
+++ b/test/typecheck/fail/tuple_lexp1.expect
@@ -2,7 +2,7 @@
 fail/tuple_lexp1.sail:10.11-20:
 10 |  (x, y) = (2, 3, 4)
    |           ^-------^
-   | Type mismatch between (int('ex248#), int('ex249#)) and (int(2), int(3), int(4))
+   | Type mismatch between (int('ex180#), int('ex181#)) and (int(2), int(3), int(4))
    | 
    | Caused by fail/tuple_lexp1.sail:10.2-8:
    | 10 |  (x, y) = (2, 3, 4)
diff --git a/test/typecheck/fail/tuple_lexp2.expect b/test/typecheck/fail/tuple_lexp2.expect
index d219bc97b..99d73fc46 100644
--- a/test/typecheck/fail/tuple_lexp2.expect
+++ b/test/typecheck/fail/tuple_lexp2.expect
@@ -2,7 +2,7 @@
 fail/tuple_lexp2.sail:10.11-12:
 10 |  (x, y) = 2
    |           ^
-   | Type mismatch between (int('ex248#), int('ex249#)) and int(2)
+   | Type mismatch between (int('ex180#), int('ex181#)) and int(2)
    | 
    | Caused by fail/tuple_lexp2.sail:10.2-8:
    | 10 |  (x, y) = 2
diff --git a/test/typecheck/fail/unbound_tyvar.expect b/test/typecheck/fail/unbound_tyvar.expect
index aee5a2e32..799bae203 100644
--- a/test/typecheck/fail/unbound_tyvar.expect
+++ b/test/typecheck/fail/unbound_tyvar.expect
@@ -9,4 +9,4 @@
   | Caused by fail/unbound_tyvar.sail:5.23-44:
   | 5 |function foo() -> bits(definitelydoesntexist) = {
   |   |                       ^-------------------^
-  |   | Undefined type synonym definitelydoesntexist
+  |   | Undefined numeric type definitelydoesntexist
diff --git a/test/typecheck/fail/unbound_tyvar2.expect b/test/typecheck/fail/unbound_tyvar2.expect
index f5b98be1f..31a5c8006 100644
--- a/test/typecheck/fail/unbound_tyvar2.expect
+++ b/test/typecheck/fail/unbound_tyvar2.expect
@@ -7,4 +7,4 @@
   | Caused by fail/unbound_tyvar2.sail:5.23-44:
   | 5 |val foo : unit -> bits(definitelydoesntexist)
   |   |                       ^-------------------^
-  |   | Undefined type synonym definitelydoesntexist
+  |   | Undefined numeric type definitelydoesntexist
diff --git a/test/typecheck/fail/unscope_type.expect b/test/typecheck/fail/unscope_type.expect
index 573a29123..c93dccad8 100644
--- a/test/typecheck/fail/unscope_type.expect
+++ b/test/typecheck/fail/unscope_type.expect
@@ -2,9 +2,14 @@
 fail/unscope_type.sail:18.10-13:
 18 |  let _ : foo = 0xFFFF_FFFF;
    |          ^-^
-   | Not in scope
+   | Well-formedness check failed for type
    | 
-   | Try requiring module A to bring the following into scope:
-   | fail/unscope_type.sail:11.5-8:
-   | 11 |type foo = bits(32)
-   |    |     ^-^ definition here in A
+   | Caused by fail/unscope_type.sail:18.10-13:
+   | 18 |  let _ : foo = 0xFFFF_FFFF;
+   |    |          ^-^
+   |    | Not in scope
+   |    | 
+   |    | Try requiring module A to bring the following into scope:
+   |    | fail/unscope_type.sail:11.5-8:
+   |    | 11 |type foo = bits(32)
+   |    |    |     ^-^ definition here in A
diff --git a/test/typecheck/fail/wf_assign_type.expect b/test/typecheck/fail/wf_assign_type.expect
index ca00c56ee..015037774 100644
--- a/test/typecheck/fail/wf_assign_type.expect
+++ b/test/typecheck/fail/wf_assign_type.expect
@@ -7,4 +7,4 @@
   | Caused by fail/wf_assign_type.sail:9.15-16:
   | 9 |  var Y : bits(X) = 0b00;
   |   |               ^
-  |   | Undefined type synonym X
+  |   | Undefined numeric type X
diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail
index 291b7e168..32d178667 100644
--- a/test/typecheck/pass/Replicate.sail
+++ b/test/typecheck/pass/Replicate.sail
@@ -6,10 +6,10 @@ $include <prelude.sail>
 overload operator / = {ediv_int}
 overload operator % = {emod_int}
 
-val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
+val Replicate : forall 'M 'N, 'M >= 1.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
 function Replicate (N, x) = {
     assert('N % 'M == 0);
     replicate_bits(x, 'N / 'M)
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect
index 0499decdd..dd092e23f 100644
--- a/test/typecheck/pass/Replicate/v1.expect
+++ b/test/typecheck/pass/Replicate/v1.expect
@@ -8,4 +8,6 @@ Explicit effect annotations are deprecated. They are no longer used and can be r
 pass/Replicate/v1.sail:14.4-30:
 14 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Failed to prove constraint: ('M * div('N, 'M)) == 'N
+   | Could not resolve quantifiers for replicate_bits
+   | * 'M >= 0
+   | * div('N, 'M) >= 0
diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail
index 55627db54..0b9feb9ca 100644
--- a/test/typecheck/pass/Replicate/v1.sail
+++ b/test/typecheck/pass/Replicate/v1.sail
@@ -6,10 +6,10 @@ $include <prelude.sail>
 overload operator / = {ediv_int}
 overload operator % = {emod_int}
 
-val Replicate : forall ('M : Int) ('N : Int), 'M >= 0.
+val Replicate : forall 'M 'N.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
 function Replicate (N, x) = {
     assert('N % 'M == 0);
     replicate_bits(x, 'N / 'M)
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index fc0f5e158..cb1fedf96 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -8,4 +8,6 @@ Explicit effect annotations are deprecated. They are no longer used and can be r
 pass/Replicate/v2.sail:13.4-30:
 13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Failed to prove constraint: ('M * 'ex248#) == 'N
+   | Could not resolve quantifiers for replicate_bits
+   | * 'M >= 0
+   | * 'ex176# >= 0
diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail
index 436ef24b0..1cb949f72 100644
--- a/test/typecheck/pass/Replicate/v2.sail
+++ b/test/typecheck/pass/Replicate/v2.sail
@@ -5,7 +5,7 @@ $include <prelude.sail>
 overload operator / = {tdiv_int}
 overload operator % = {tmod_int}
 
-val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
+val Replicate : forall 'M 'N, 'M >= 1.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
 function Replicate (N, x) = {
diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail
index efe625558..be2261618 100644
--- a/test/typecheck/pass/add_vec_lit.sail
+++ b/test/typecheck/pass/add_vec_lit.sail
@@ -1,14 +1,13 @@
 default Order inc
 $include <arith.sail>
 
-val add_vec = pure {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
+val add_vec = pure {ocaml: "add_vec", lem: "add_vec"}: forall 'n.
   (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
-val unsigned : forall ('n : Int).
+val unsigned : forall 'n.
   bitvector('n, inc) -> range(0, 2 ^ 'n - 1)
 
 overload operator + = {add_vec}
 
 let x : range(0, 30) = unsigned(0xF + 0x2)
 let y : range(0, 30) = unsigned(0xF) + unsigned(0x2)
-
diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail
index 8c08bf95d..3b85f0de4 100644
--- a/test/typecheck/pass/arm_FPEXC1.sail
+++ b/test/typecheck/pass/arm_FPEXC1.sail
@@ -1,12 +1,12 @@
 default Order dec
 
-val vector_access = pure {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall ('n : Int).
+val vector_access = pure {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall 'n.
   (bitvector('n, dec), int) -> bit
 
-val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
+val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall 'n 'm 'o, 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
   (bitvector('n, dec), atom('m), atom('o)) -> bitvector('m - ('o - 1), dec)
 
-val vector_update_subrange = pure {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+val vector_update_subrange = pure {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o, 'm - ('o - 1) >= 0.
   (bitvector('n, dec), atom('m), atom('o), bitvector('m - ('o - 1), dec)) -> bitvector('n, dec)
 
 register _FPEXC32_EL2 : bitvector(32, dec)
diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect
index d9a6e0cc6..5692869b5 100644
--- a/test/typecheck/pass/bool_constraint/v1.expect
+++ b/test/typecheck/pass/bool_constraint/v1.expect
@@ -9,13 +9,13 @@ All external bindings should be marked as either pure or impure
 12 |  if b then n else 4
    |                   ^
    | int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)}
-   | as (('b & 'ex239 == 'n) | (not('b) & 'ex239 == 3)) could not be proven
+   | as (('b & 'ex171 == 'n) | (not('b) & 'ex171 == 3)) could not be proven
    | 
-   | type variable 'ex239:
+   | type variable 'ex171:
    | pass/bool_constraint/v1.sail:9.25-73:
    | 9 |  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
    |   |                         ^----------------------------------------------^ derived from here
    | pass/bool_constraint/v1.sail:12.19-20:
    | 12 |  if b then n else 4
    |    |                   ^ bound here
-   |    | has constraint: 4 == 'ex239
+   |    | has constraint: 4 == 'ex171
diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail
index cc7225694..3d6ab6630 100644
--- a/test/typecheck/pass/deinfix_plus.sail
+++ b/test/typecheck/pass/deinfix_plus.sail
@@ -1,6 +1,6 @@
 default Order inc
 
-val bv_add = pure {ocaml: "add_vec", lem: "add_vec", coq: "add_vec"}: forall ('n : Int).
+val bv_add = pure {ocaml: "add_vec", lem: "add_vec", coq: "add_vec"}: forall 'n.
   (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
 overload operator + = {bv_add}
diff --git a/test/typecheck/pass/ex_cast.sail b/test/typecheck/pass/ex_cast.sail
index 6565e9d18..83d4156f8 100644
--- a/test/typecheck/pass/ex_cast.sail
+++ b/test/typecheck/pass/ex_cast.sail
@@ -4,6 +4,6 @@ val cast ex_int : int -> {'n, true. atom('n)}
 
 val zeros : forall 'n. atom('n) -> vector('n, dec, bit)
 
-val test : int -> unit
+val test : nat -> unit
 
 function test n = { x = zeros(n); () }
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index b4870d796..65f17520d 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -1,5 +1,10 @@
 Type error:
-pass/exist_synonym/v1.sail:6.28-37:
+pass/exist_synonym/v1.sail:6.8-38:
 6 |let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
-  |                            ^-------^
-  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)
+  |        ^----------------------------^
+  | Well-formedness check failed for type
+  | 
+  | Caused by pass/exist_synonym/v1.sail:6.28-33:
+  | 6 |let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
+  |   |                            ^---^
+  |   | Could not prove (0 <= 'n & 'n < 32) for type constructor regno
diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect
index d88e1aafa..63096bbbf 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -1,5 +1,10 @@
 Type error:
-pass/exist_synonym/v2.sail:6.27-36:
+pass/exist_synonym/v2.sail:6.8-37:
 6 |let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
-  |                           ^-------^
-  | Could not prove constraints (0 <= 'n & 'n < 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)
+  |        ^---------------------------^
+  | Well-formedness check failed for type
+  | 
+  | Caused by pass/exist_synonym/v2.sail:6.27-32:
+  | 6 |let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
+  |   |                           ^---^
+  |   | Could not prove (0 <= 'n & 'n < 2) for type constructor regno
diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
index 4aecd8c57..a4d2e7547 100644
--- a/test/typecheck/pass/exist_synonym/v3.expect
+++ b/test/typecheck/pass/exist_synonym/v3.expect
@@ -1,5 +1,10 @@
 Type error:
-pass/exist_synonym/v3.sail:9.38-47:
+pass/exist_synonym/v3.sail:9.11-55:
 9 |val test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit
-  |                                      ^-------^
-  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_#x & '_#x <= 8), (0 <= '_#x#0 & '_#x#0 <= 8)
+  |           ^------------------------------------------^
+  | Well-formedness check failed for type
+  | 
+  | Caused by pass/exist_synonym/v3.sail:9.38-43:
+  | 9 |val test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit
+  |   |                                      ^---^
+  |   | Could not prove (0 <= 'n & 'n < 32) for type constructor regno
diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect
index f9711cd3c..169c87429 100644
--- a/test/typecheck/pass/exist_synonym/v4.expect
+++ b/test/typecheck/pass/exist_synonym/v4.expect
@@ -1,5 +1,10 @@
 Type error:
-pass/exist_synonym/v4.sail:9.35-44:
+pass/exist_synonym/v4.sail:9.11-52:
 9 |val test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit
-  |                                   ^-------^
-  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= '_#x & '_#x <= 8), (0 <= '_#x#0 & '_#x#0 <= 8)
+  |           ^---------------------------------------^
+  | Well-formedness check failed for type
+  | 
+  | Caused by pass/exist_synonym/v4.sail:9.35-40:
+  | 9 |val test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit
+  |   |                                   ^---^
+  |   | Could not prove (0 <= 'n & 'n < 32) for type constructor regno
diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail
index 1d0e1d207..40db23a07 100644
--- a/test/typecheck/pass/exist_tlb.sail
+++ b/test/typecheck/pass/exist_tlb.sail
@@ -1,16 +1,16 @@
 $include <flow.sail>
 
-val extz : forall ('n : Int) ('m : Int) ('ord : Order).
+val extz : forall 'n 'm ('ord : Order).
   bitvector('n, 'ord) -> bitvector('m, 'ord)
 
-val exts : forall ('n : Int) ('m : Int) ('ord : Order).
+val exts : forall 'n 'm ('ord : Order).
   bitvector('n, 'ord) -> bitvector('m, 'ord)
 
 overload EXTZ = {extz}
 
 overload EXTS = {exts}
 
-val add_vec : forall ('n : Int) ('ord : Order).
+val add_vec : forall 'n ('ord : Order).
   (bitvector('n, 'ord), bitvector('n, 'ord)) -> bitvector('n, 'ord)
 
 overload operator + = {add_vec}
@@ -71,10 +71,10 @@ function wordWidthBytes w = match w {
   D => 8
 }
 
-val MEMr_reserve_wrapper : forall ('n : Int).
+val MEMr_reserve_wrapper : forall 'n.
   (bitvector(64, dec), atom('n)) -> bitvector(8 * 'n, dec) effect {rmem}
 
-val MEMr_wrapper : forall ('n : Int).
+val MEMr_wrapper : forall 'n.
   (bitvector(64, dec), atom('n)) -> bitvector(8 * 'n, dec) effect {rmem}
 
 val wGPR : (bitvector(5, dec), bitvector(64, dec)) -> unit effect {wreg}
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index 59c047420..eb2b51394 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -9,4 +9,4 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^ checking function argument has type ast
    | Could not resolve quantifiers for Ctor1
-   | * 'ex334# in {32, 64}
+   | * 'ex247# in {32, 64}
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index 609d3a744..8ba820a54 100644
--- a/test/typecheck/pass/existential_ast3/v1.expect
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -2,10 +2,10 @@
 pass/existential_ast3/v1.sail:17.48-65:
 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |                                                ^---------------^
-   | (int(33), int('ex288)) is not a subtype of (int('ex283), int('ex284))
+   | (int(33), int('ex212)) is not a subtype of (int('ex207), int('ex208))
    | as false could not be proven
    | 
-   | type variable 'ex283:
+   | type variable 'ex207:
    | pass/existential_ast3/v1.sail:16.23-25:
    | 16 |  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
    |    |                       ^^ derived from here
@@ -13,7 +13,7 @@
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^ bound here
    | 
-   | type variable 'ex284:
+   | type variable 'ex208:
    | pass/existential_ast3/v1.sail:16.26-28:
    | 16 |  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
    |    |                          ^^ derived from here
@@ -21,7 +21,7 @@
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^ bound here
    | 
-   | type variable 'ex288:
+   | type variable 'ex212:
    | pass/existential_ast3/v1.sail:17.48-65:
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^ bound here
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index 353d38332..f63196c07 100644
--- a/test/typecheck/pass/existential_ast3/v2.expect
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -2,10 +2,10 @@
 pass/existential_ast3/v2.sail:17.48-65:
 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |                                                ^---------------^
-   | (int(31), int('ex288)) is not a subtype of (int('ex283), int('ex284))
+   | (int(31), int('ex212)) is not a subtype of (int('ex207), int('ex208))
    | as false could not be proven
    | 
-   | type variable 'ex283:
+   | type variable 'ex207:
    | pass/existential_ast3/v2.sail:16.23-25:
    | 16 |  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
    |    |                       ^^ derived from here
@@ -13,7 +13,7 @@
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^ bound here
    | 
-   | type variable 'ex284:
+   | type variable 'ex208:
    | pass/existential_ast3/v2.sail:16.26-28:
    | 16 |  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
    |    |                          ^^ derived from here
@@ -21,7 +21,7 @@
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^ bound here
    | 
-   | type variable 'ex288:
+   | type variable 'ex212:
    | pass/existential_ast3/v2.sail:17.48-65:
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^ bound here
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index 6779d6df8..0e2882dd6 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)))
    |         ^-----------------------------^ checking function argument has type ast
    | Could not resolve quantifiers for Ctor
-   | * (64 in {32, 64} & (0 <= 'ex325# & 'ex325# < 64))
+   | * (64 in {32, 64} & (0 <= 'ex244# & 'ex244# < 64))
diff --git a/test/typecheck/pass/existential_ast3/v4.expect b/test/typecheck/pass/existential_ast3/v4.expect
index dc172e036..1636d061b 100644
--- a/test/typecheck/pass/existential_ast3/v4.expect
+++ b/test/typecheck/pass/existential_ast3/v4.expect
@@ -3,13 +3,13 @@
 36 |    if is_64 then 64 else 32;
    |                  ^^
    | int(64) is not a subtype of {('d : Int), (('is_64 & 'd == 63) | (not('is_64) & 'd == 32)). int('d)}
-   | as (('is_64 & 'ex341 == 63) | (not('is_64) & 'ex341 == 32)) could not be proven
+   | as (('is_64 & 'ex256 == 63) | (not('is_64) & 'ex256 == 32)) could not be proven
    | 
-   | type variable 'ex341:
+   | type variable 'ex256:
    | pass/existential_ast3/v4.sail:35.18-79:
    | 35 |  let 'datasize : {'d, ('is_64 & 'd == 63) | (not('is_64) & 'd == 32). int('d)} =
    |    |                  ^-----------------------------------------------------------^ derived from here
    | pass/existential_ast3/v4.sail:36.18-20:
    | 36 |    if is_64 then 64 else 32;
    |    |                  ^^ bound here
-   |    | has constraint: 64 == 'ex341
+   |    | has constraint: 64 == 'ex256
diff --git a/test/typecheck/pass/existential_ast3/v5.expect b/test/typecheck/pass/existential_ast3/v5.expect
index 91b3e4539..57b7e4b62 100644
--- a/test/typecheck/pass/existential_ast3/v5.expect
+++ b/test/typecheck/pass/existential_ast3/v5.expect
@@ -3,13 +3,13 @@
 37 |  let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);
    |                                                  ^-------------^
    | range(0, 63) is not a subtype of range(0, ('datasize - 2))
-   | as (0 <= 'ex349 & 'ex349 <= ('datasize - 2)) could not be proven
+   | as (0 <= 'ex264 & 'ex264 <= ('datasize - 2)) could not be proven
    | 
-   | type variable 'ex349:
+   | type variable 'ex264:
    | pass/existential_ast3/v5.sail:37.10-33:
    | 37 |  let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);
    |    |          ^---------------------^ derived from here
    | pass/existential_ast3/v5.sail:37.50-65:
    | 37 |  let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);
    |    |                                                  ^-------------^ bound here
-   |    | has constraint: (0 <= 'ex349 & 'ex349 <= 63)
+   |    | has constraint: (0 <= 'ex264 & 'ex264 <= 63)
diff --git a/test/typecheck/pass/existential_ast3/v6.expect b/test/typecheck/pass/existential_ast3/v6.expect
index bab7bcb89..f56f52ecd 100644
--- a/test/typecheck/pass/existential_ast3/v6.expect
+++ b/test/typecheck/pass/existential_ast3/v6.expect
@@ -3,13 +3,13 @@
 37 |  let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);
    |                                                                       ^-------------^
    | range(0, 63) is not a subtype of range(0, ('datasize - 1))
-   | as (0 <= 'ex355 & 'ex355 <= ('datasize - 1)) could not be proven
+   | as (0 <= 'ex270 & 'ex270 <= ('datasize - 1)) could not be proven
    | 
-   | type variable 'ex355:
+   | type variable 'ex270:
    | pass/existential_ast3/v6.sail:37.10-33:
    | 37 |  let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);
    |    |          ^---------------------^ derived from here
    | pass/existential_ast3/v6.sail:37.71-86:
    | 37 |  let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);
    |    |                                                                       ^-------------^ bound here
-   |    | has constraint: (0 <= 'ex355 & 'ex355 <= 63)
+   |    | has constraint: (0 <= 'ex270 & 'ex270 <= 63)
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index ff6f26082..7f5153d48 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -3,7 +3,7 @@
 10 |  let _ = 0b100[if R then 0 else f()];
    |          ^-------------------------^
    | Could not resolve quantifiers for bitvector_access
-   | * (0 <= 'ex240# & 'ex240# < 3)
+   | * (0 <= 'ex172# & 'ex172# < 3)
    | 
    | Caused by pass/if_infer/v1.sail:10.10-37:
    | 10 |  let _ = 0b100[if R then 0 else f()];
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index dacec8d6a..53ddc5a53 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -3,7 +3,7 @@
 10 |  let _ = 0b1001[if R then 0 else f()];
    |          ^--------------------------^
    | Could not resolve quantifiers for bitvector_access
-   | * (0 <= 'ex240# & 'ex240# < 4)
+   | * (0 <= 'ex172# & 'ex172# < 4)
    | 
    | Caused by pass/if_infer/v2.sail:10.10-38:
    | 10 |  let _ = 0b1001[if R then 0 else f()];
diff --git a/test/typecheck/pass/int_synonym.sail b/test/typecheck/pass/int_synonym.sail
index 1de6087e7..ff59f2c1c 100644
--- a/test/typecheck/pass/int_synonym.sail
+++ b/test/typecheck/pass/int_synonym.sail
@@ -3,7 +3,7 @@ default Order dec
 
 $include <flow.sail>
 
-type bits ('n : Int) = bitvector('n, dec)
+type bits('n) = bitvector('n, dec)
 
 type xlen : Int       = 64
 type xlen_bytes : Int = 8
diff --git a/test/typecheck/pass/negative_bits_list/v1.expect b/test/typecheck/pass/negative_bits_list/v1.expect
deleted file mode 100644
index f74668439..000000000
--- a/test/typecheck/pass/negative_bits_list/v1.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Type error:
-pass/negative_bits_list/v1.sail:9.30-39:
-9 |    let z: list(bits(-1)) = [|undefined|];
-  |                              ^-------^
-  | Type bitvector(-1) could be empty
diff --git a/test/typecheck/pass/negative_bits_list/v1.sail b/test/typecheck/pass/negative_bits_list/v1.sail
deleted file mode 100644
index 7a1080162..000000000
--- a/test/typecheck/pass/negative_bits_list/v1.sail
+++ /dev/null
@@ -1,11 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-val foo : unit -> unit
-
-function foo() = {
-    let x: list(bits(-1)) = [||];
-    let z: list(bits(-1)) = [|undefined|];
-    ()
-}
diff --git a/test/typecheck/pass/negative_bits_list/v2.expect b/test/typecheck/pass/negative_bits_list/v2.expect
deleted file mode 100644
index e080a8588..000000000
--- a/test/typecheck/pass/negative_bits_list/v2.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Type error:
-pass/negative_bits_list/v2.sail:9.28-37:
-9 |    let y: list(bits(-1)) = undefined;
-  |                            ^-------^
-  | Type list(bits(-1)) cannot be undefined
diff --git a/test/typecheck/pass/negative_bits_list/v2.sail b/test/typecheck/pass/negative_bits_list/v2.sail
deleted file mode 100644
index c5238a289..000000000
--- a/test/typecheck/pass/negative_bits_list/v2.sail
+++ /dev/null
@@ -1,11 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-val foo : unit -> unit
-
-function foo() = {
-    let x: list(bits(-1)) = [||];
-    let y: list(bits(-1)) = undefined;
-    ()
-}
diff --git a/test/typecheck/pass/nexp_synonym2.sail b/test/typecheck/pass/nexp_synonym2.sail
index 9e9bd7b8d..df1e3c507 100644
--- a/test/typecheck/pass/nexp_synonym2.sail
+++ b/test/typecheck/pass/nexp_synonym2.sail
@@ -6,7 +6,7 @@ type LEN : Int = 30 + 2
 
 type V : Type = bits(LEN)
 
-type V2('n: Int) -> Type = bits('n)
+type V2('n : Int), 'n >= 0 -> Type = bits('n)
 
 let v : V = 0xFFFF_FFFF
 
diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail
index 5c376ba2e..cd5aa5fd6 100644
--- a/test/typecheck/pass/nzcv.sail
+++ b/test/typecheck/pass/nzcv.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_dec"} : forall 'n 'm 'o, 'o <= 'm <= 'n.
   (bitvector('n, dec), atom('m), atom('o)) -> bitvector('m - ('o - 1), dec)
 
 val test : bitvector(4, dec) -> unit
diff --git a/test/typecheck/pass/phantom_bitlist_struct.sail b/test/typecheck/pass/phantom_bitlist_struct.sail
index 09d0f952a..125db07c3 100644
--- a/test/typecheck/pass/phantom_bitlist_struct.sail
+++ b/test/typecheck/pass/phantom_bitlist_struct.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-struct phantom('n: Int) = {
+struct phantom('n) = {
   bits: bits('n),
 }
 
diff --git a/test/typecheck/pass/phantom_bitlist_union.sail b/test/typecheck/pass/phantom_bitlist_union.sail
index 111424a15..6876b86f2 100644
--- a/test/typecheck/pass/phantom_bitlist_union.sail
+++ b/test/typecheck/pass/phantom_bitlist_union.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-union phantom('n: Int) = {
+union phantom('n) = {
   Bits: bits('n),
 }
 
diff --git a/test/typecheck/pass/poly_vector/v2.expect b/test/typecheck/pass/poly_vector/v2.expect
index 3dae703f4..8dd069a2a 100644
--- a/test/typecheck/pass/poly_vector/v2.expect
+++ b/test/typecheck/pass/poly_vector/v2.expect
@@ -1,5 +1,5 @@
 Type error:
-pass/poly_vector/v2.sail:7.30-48:
-7 |val "to_generic" : forall 'n. bitvector('n, dec) -> vector('n, dec, bit)
-  |                              ^----------------^
-  | bitvector : Int -> Type expected 1 arguments, given 2
+pass/poly_vector/v2.sail:5.5-14:
+5 |type bitvector('n, 'ord: Order) = vector('n, 'ord, bit)
+  |     ^-------^
+  | Cannot define type synonym bitvector, as a type or synonym with that name already exists
diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail
index b837ac27d..580a1d27a 100644
--- a/test/typecheck/pass/procstate1.sail
+++ b/test/typecheck/pass/procstate1.sail
@@ -4,7 +4,7 @@ infix 4 ==
 
 val operator == = pure {lem: "eq_vec"} : forall 'n. (bitvector('n, dec), bitvector('n, dec)) -> bool
 
-struct ProcState ('n : Int) = {
+struct ProcState('n) = {
   N : bitvector('n, dec),
   Z : bitvector(1, dec),
   C : bitvector(1, dec),
diff --git a/test/typecheck/pass/reg_32_64/v3.expect b/test/typecheck/pass/reg_32_64/v3.expect
index 49775438f..9e5186a94 100644
--- a/test/typecheck/pass/reg_32_64/v3.expect
+++ b/test/typecheck/pass/reg_32_64/v3.expect
@@ -17,5 +17,5 @@ Explicit effect annotations are deprecated. They are no longer used and can be r
    | * sub_int
    |   pass/reg_32_64/v3.sail:29.15-17:
    |   29 |  reg_deref(R)['d - 1 .. 0]
-   |      |               ^^ checking function argument has type int('ex173#)
+   |      |               ^^ checking function argument has type int('ex105#)
    |      | Cannot re-write sizeof('d)
diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail
index 2bfbf22ff..c6cee7b26 100644
--- a/test/typecheck/pass/vec_pat1.sail
+++ b/test/typecheck/pass/vec_pat1.sail
@@ -1,12 +1,12 @@
 default Order inc
 
-val bv_add = pure {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
+val bv_add = pure {ocaml: "add_vec", lem: "add_vec"}: forall 'n.
   (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
-val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_inc"}: forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
+val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_inc"}: forall 'l 'm 'o, 'l >= 0 & 'm <= 'o & 'o <= 'l.
   (bitvector('l, inc), atom('m), atom('o)) -> bitvector('o + 1 - 'm, inc)
 
-val bitvector_concat = pure {ocaml: "append", lem: "concat_vec"} : forall ('m : Int) ('p : Int).
+val bitvector_concat = pure {ocaml: "append", lem: "concat_vec"} : forall 'm 'p.
   (bitvector('m, inc), bitvector('p, inc)) -> bitvector('m + 'p, inc)
 
 val eq_vec = pure {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bitvector('n, inc), bitvector('n, inc)) -> bool
diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail
index 88d4bea83..24cde45b4 100644
--- a/test/typecheck/pass/vector_subrange_gen.sail
+++ b/test/typecheck/pass/vector_subrange_gen.sail
@@ -1,10 +1,10 @@
 
-val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
+val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('l : Int) 'm ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
   (bitvector('l, inc), atom('m), atom('o)) -> bitvector('o - 'm + 1, inc)
 
 val sub : forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> atom('n - 'm)
 
-val bitvector_length = pure "length" : forall ('n : Int). bitvector('n, inc) -> atom('n)
+val bitvector_length = pure "length" : forall ('n : Int), 'n >= 0. bitvector('n, inc) -> atom('n)
 
 overload __size = {bitvector_length}
 
diff --git a/test/typecheck/pass/wf_specs/wf_specs.expect b/test/typecheck/pass/wf_specs/wf_specs.expect
index ba6a8df22..700f37819 100644
--- a/test/typecheck/pass/wf_specs/wf_specs.expect
+++ b/test/typecheck/pass/wf_specs/wf_specs.expect
@@ -7,4 +7,4 @@
    | Caused by pass/wf_specs/wf_specs.sail:10.25-35:
    | 10 |val f : bits(32) -> bits(THIRTY_TWO)
    |    |                         ^--------^
-   |    | Undefined type synonym THIRTY_TWO
+   |    | Undefined numeric type THIRTY_TWO
diff --git a/test/typecheck/pass/while_MM.sail b/test/typecheck/pass/while_MM.sail
index d0cbc8e50..69a012e0e 100644
--- a/test/typecheck/pass/while_MM.sail
+++ b/test/typecheck/pass/while_MM.sail
@@ -2,7 +2,7 @@ default Order dec
 
 val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int
 
-val add_vec_int : forall ('n : Int) ('ord : Order).
+val add_vec_int : forall 'n ('ord : Order).
   (bitvector('n, 'ord), int) -> bitvector('n, 'ord)
 
 overload operator + = {add_vec_int, add_int}