Simplify kinds in the AST

Rather than having K_aux (K_kind [BK_aux (BK_int, _)], _) represent
the Int kind, we now just have K_aux (K_int, _). Since the language is
first order we have no need for fancy kinds in the AST.

13 files changed, 106 insertions, 150 deletions

diff --git a/language/sail.ott b/language/sail.ott
index 2875c951..4ce08415 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -1,4 +1,4 @@
-%%
+%
 %% Grammar for user language. Generates ./src/ast.ml
 %%
 
@@ -169,19 +169,13 @@ kid :: '' ::=
 
 grammar
 
-base_kind :: 'BK_' ::=
+kind :: 'K_' ::=
   {{ com base kind}}
   {{ aux _ l }}
   | Type  :: :: type  {{ com kind of types  }}
   | Int   :: :: int   {{ com kind of natural number size expressions  }}
   | Order :: :: order {{ com kind of vector order specifications  }}
 
-kind :: 'K_' ::=
-  {{ com kinds}}
-  {{ aux _ l }}
-  | base_kind1 -> ... -> base_kindn            :: :: kind
-% we'll never use  ...-> Nat , .. Order , .. or Effects
-
 nexp :: 'Nexp_' ::=
   {{ com numeric expression, of kind Int }}
   {{ aux _ l }}
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 14638b88..ffe4c90e 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -106,13 +106,13 @@ let mk_funcl id pat body = FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, body),
 
 let mk_qi_nc nc = QI_aux (QI_const nc, Parse_ast.Unknown)
 
-let mk_qi_id bk kid =
+let mk_qi_id k kid =
   let kopt =
-    KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (bk, Parse_ast.Unknown)], Parse_ast.Unknown), kid), Parse_ast.Unknown)
+    KOpt_aux (KOpt_kind (K_aux (k, Parse_ast.Unknown), kid), Parse_ast.Unknown)
   in
   QI_aux (QI_id kopt, Parse_ast.Unknown)
 
-let mk_qi_kopt kopt =QI_aux (QI_id kopt, Parse_ast.Unknown)
+let mk_qi_kopt kopt = QI_aux (QI_id kopt, Parse_ast.Unknown)
 
 let mk_fundef funcls =
   let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in
@@ -131,16 +131,16 @@ let kopt_kid (KOpt_aux (kopt_aux, _)) =
   | KOpt_none kid | KOpt_kind (_, kid) -> kid
 
 let is_nat_kopt = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_int, _)], _), _), _) -> true
+  | KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true
   | KOpt_aux (KOpt_none _, _) -> true
   | _ -> false
 
 let is_order_kopt = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), _), _) -> true
+  | KOpt_aux (KOpt_kind (K_aux (K_order, _), _), _) -> true
   | _ -> false
 
 let is_typ_kopt = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), _), _) -> true
+  | KOpt_aux (KOpt_kind (K_aux (K_type, _), _), _) -> true
   | _ -> false
 
 let string_of_kid = function
@@ -625,14 +625,12 @@ let string_of_base_effect_aux = function
   (*| BE_lset -> "lset"
   | BE_lret -> "lret"*)
 
-let string_of_base_kind_aux = function
-  | BK_type -> "Type"
-  | BK_int -> "Int"
-  | BK_order -> "Order"
+let string_of_kind_aux = function
+  | K_type -> "Type"
+  | K_int -> "Int"
+  | K_order -> "Order"
 
-let string_of_base_kind (BK_aux (bk, _)) = string_of_base_kind_aux bk
-
-let string_of_kind (K_aux (K_kind bks, _)) = string_of_list " -> " string_of_base_kind bks
+let string_of_kind (K_aux (k, _)) = string_of_kind_aux k
 
 let string_of_base_effect = function
   | BE_aux (beff, _) -> string_of_base_effect_aux beff
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 8f555744..b7979e88 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -85,7 +85,7 @@ val mk_fundef : (unit funcl) list -> unit def
 val mk_val_spec : val_spec_aux -> unit def
 val mk_typschm : typquant -> typ -> typschm
 val mk_typquant : quant_item list -> typquant
-val mk_qi_id : base_kind_aux -> kid -> quant_item
+val mk_qi_id : kind_aux -> kid -> quant_item
 val mk_qi_nc : n_constraint -> quant_item
 val mk_qi_kopt : kinded_id -> quant_item
 val mk_fexp : id -> unit exp -> unit fexp
@@ -207,8 +207,7 @@ val def_loc : 'a def -> Parse_ast.l
 val string_of_id : id -> string
 val string_of_kid : kid -> string
 val string_of_base_effect_aux : base_effect_aux -> string
-val string_of_base_kind_aux : base_kind_aux -> string
-val string_of_base_kind : base_kind -> string
+val string_of_kind_aux : kind_aux -> string
 val string_of_kind : kind -> string
 val string_of_base_effect : base_effect -> string
 val string_of_effect : effect -> string
diff --git a/src/initial_check.ml b/src/initial_check.ml
index b442ae97..d1efb374 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -149,23 +149,11 @@ let to_ast_id (Parse_ast.Id_aux(id, l)) =
 
 let to_ast_var (Parse_ast.Kid_aux(Parse_ast.Var v,l)) = Kid_aux(Var v,l)
 
-let to_ast_base_kind (Parse_ast.BK_aux(k,l')) =
+let to_ast_kind (Parse_ast.K_aux(k,l')) =
   match k with
-  | Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ}
-  | Parse_ast.BK_int -> BK_aux(BK_int,l'), { k = K_Nat }
-  | Parse_ast.BK_order -> BK_aux(BK_order,l'), { k = K_Ord }
-
-let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) =
-  match klst with
-  | [] -> raise (Reporting.err_unreachable l __POS__ "Kind with empty kindlist encountered")
-  | [k] -> let k_ast,k_typ = to_ast_base_kind k in
-           K_aux(K_kind([k_ast]),l), k_typ
-  | ks -> let k_pairs = List.map to_ast_base_kind ks in
-          let reverse_typs = List.rev (List.map snd k_pairs) in
-          let ret,args = List.hd reverse_typs, List.rev (List.tl reverse_typs) in
-          match ret.k with
-          | K_Typ -> K_aux(K_kind(List.map fst k_pairs), l), { k = K_Lam(args,ret) }
-          | _ -> typ_error l "Type constructor must have an -> kind ending in Type" None None None
+  | Parse_ast.K_type -> K_aux(K_type,l'), { k = K_Typ}
+  | Parse_ast.K_int -> K_aux(K_int,l'), { k = K_Nat }
+  | Parse_ast.K_order -> K_aux(K_order,l'), { k = K_Ord }
 
 let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) : Ast.typ =
   (*  let _ = Printf.eprintf "to_ast_typ\n" in*)
@@ -392,7 +380,7 @@ let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant
       | Parse_ast.KOpt_kind(k,v) ->
 	let v = to_ast_var v in
 	let key = var_to_string v in
-	let kind,ktyp = to_ast_kind k_env k in
+        let kind,ktyp = to_ast_kind k in
 	v,key,Some(kind),Some(ktyp)
     in
     if (Nameset.mem key local_names)
@@ -639,13 +627,13 @@ and to_ast_record_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp
 
 let to_ast_default (names, k_env, default_order) (default : Parse_ast.default_typing_spec) : default_spec envs_out =
   match default with
-  | Parse_ast.DT_aux(Parse_ast.DT_order(bk,o),l) ->
-     let k,k_typ = to_ast_base_kind bk in
+  | Parse_ast.DT_aux(Parse_ast.DT_order(k,o),l) ->
+     let k,k_typ = to_ast_kind k in
      (match (k,o) with
-      | (BK_aux(BK_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_inc,lo)) ->
+      | (K_aux(K_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_inc,lo)) ->
          let default_order = Ord_aux(Ord_inc,lo) in
          DT_aux(DT_order default_order,l),(names,k_env,default_order)
-      | (BK_aux(BK_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_dec,lo)) ->
+      | (K_aux(K_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_dec,lo)) ->
          let default_order = Ord_aux(Ord_dec,lo) in
          DT_aux(DT_order default_order,l),(names,k_env,default_order)
       | _ -> typ_error l "Inc and Dec must have kind Order" None None None)
@@ -732,7 +720,7 @@ let to_ast_kdef (names, k_env, def_ord) (td:Parse_ast.kind_def) : unit kind_def
   match td with
   | Parse_ast.KD_aux (Parse_ast.KD_nabbrev (kind, id, name_scm_opt, atyp), l) ->
      let id = to_ast_id id in
-     let (kind, k) = to_ast_kind k_env kind in
+     let (kind, k) = to_ast_kind kind in
      KD_aux (KD_nabbrev (kind, id, to_ast_namescm name_scm_opt, to_ast_nexp k_env atyp), (l, ()))
 
 let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
@@ -1257,7 +1245,7 @@ let generate_enum_functions vs_ids (Defs defs) =
          if IdSet.mem name vs_ids then []
          else
            [ enum_val_spec name
-              [mk_qi_id BK_int kid; mk_qi_nc (range_constraint kid)]
+              [mk_qi_id K_int kid; mk_qi_nc (range_constraint kid)]
               (function_typ [atom_typ (nvar kid)] (mk_typ (Typ_id id)) no_effect);
              mk_fundef [funcl] ]
        in
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 0d7fd6e5..6a262df6 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -749,7 +749,7 @@ let reduce_cast typ exp l annot =
   let typ' = Env.base_typ_of env typ in
   match exp, destruct_exist env typ' with
   | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' ->
-     let nc_env = Env.add_typ_var l kid BK_int env in
+     let nc_env = Env.add_typ_var l kid K_int env in
      let nc_env = Env.add_constraint (nc_eq (nvar kid) (nconstant n)) nc_env in
      if prove nc_env nc
      then exp
@@ -2774,7 +2774,7 @@ let update_env_new_kids env deps typ_env_pre typ_env_post =
   let kbound =
     KBindings.merge (fun k x y ->
       match x,y with
-      | Some bk, None -> Some bk
+      | Some k, None -> Some k
       | _ -> None)
       (Env.get_typ_vars typ_env_post)
       (Env.get_typ_vars typ_env_pre)
@@ -3190,7 +3190,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
             { env with kid_deps =
                 List.fold_left (fun kds kid -> KBindings.add kid deps kds) env.kid_deps kids },
            Env.add_constraint nc
-             (List.fold_left (fun tenv kid -> Env.add_typ_var l kid BK_int tenv) tenv kids),
+             (List.fold_left (fun tenv kid -> Env.add_typ_var l kid K_int tenv) tenv kids),
            typ
        in
        if is_bitvector_typ typ then
@@ -4031,9 +4031,9 @@ let fill_in_type env typ =
   let tyvars = tyvars_of_typ typ in
   let subst = KidSet.fold (fun kid subst ->
     match Env.get_typ_var kid env with
-    | BK_type
-    | BK_order -> subst
-    | BK_int ->
+    | K_type
+    | K_order -> subst
+    | K_int ->
        (match solve env (nvar kid) with
        | None -> subst
        | Some n -> KBindings.add kid (nconstant n) subst)) tyvars KBindings.empty in
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index c50977ed..38854d48 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -70,15 +70,15 @@ type x = text (* identifier *)
 type ix = text (* infix identifier *)
 
 type 
-base_kind_aux =  (* base kind *)
-   BK_type (* kind of types *)
- | BK_int (* kind of natural number size expressions *)
- | BK_order (* kind of vector order specifications *)
+kind_aux =  (* base kind *)
+   K_type (* kind of types *)
+ | K_int (* kind of natural number size expressions *)
+ | K_order (* kind of vector order specifications *)
 
 
 type 
-base_kind = 
-   BK_aux of base_kind_aux * l
+kind =
+   K_aux of kind_aux * l
 
 
 type 
@@ -110,13 +110,7 @@ id_aux =  (* Identifier *)
    Id of x
  | DeIid of x (* remove infix status *)
 
-
-type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind) list
-
-
-type 
+type
 base_effect = 
    BE_aux of base_effect_aux * l
 
@@ -130,13 +124,7 @@ type
 id = 
    Id_aux of id_aux * l
 
-
-type 
-kind = 
-   K_aux of kind_aux * l
-
-
-type 
+type
 atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *)
    ATyp_id of id (* identifier *)
  | ATyp_var of kid (* ticked variable *)
@@ -425,7 +413,7 @@ name_scm_opt =
 
 type 
 default_typing_spec_aux =  (* Default kinding or typing assumption, and default order for literal vectors and vector shorthands *)
-   DT_order of base_kind * atyp
+   DT_order of kind * atyp
 
 
 type mpat_aux =  (* Mapping pattern. Mostly the same as normal patterns but only constructible parts *)
diff --git a/src/parser.mly b/src/parser.mly
index cd655217..fd6c9373 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -585,17 +585,13 @@ typ_list:
   | typ Comma typ_list
     { $1 :: $3 }
 
-base_kind:
+kind:
   | Int
-    { BK_aux (BK_int, loc $startpos $endpos) }
+    { K_aux (K_int, loc $startpos $endpos) }
   | TYPE
-    { BK_aux (BK_type, loc $startpos $endpos) }
+    { K_aux (K_type, loc $startpos $endpos) }
   | Order
-    { BK_aux (BK_order, loc $startpos $endpos) }
-
-kind:
-  | base_kind
-    { K_aux (K_kind [$1], loc $startpos $endpos) }
+    { K_aux (K_order, loc $startpos $endpos) }
 
 kopt:
   | Lparen kid Colon kind Rparen
@@ -1393,9 +1389,9 @@ register_def:
     { mk_reg_dec (DEC_config ($3, $5, $7)) $startpos $endpos }
 
 default_def:
-  | Default base_kind Inc
+  | Default kind Inc
     { mk_default (DT_order ($2, mk_typ ATyp_inc $startpos($3) $endpos)) $startpos $endpos }
-  | Default base_kind Dec
+  | Default kind Dec
     { mk_default (DT_order ($2, mk_typ ATyp_dec $startpos($3) $endpos)) $startpos $endpos }
 
 scattered_def:
@@ -1449,8 +1445,7 @@ def:
   | default_def
     { DEF_default $1 }
   | Constant id Eq typ
-    { DEF_kind (KD_aux (KD_nabbrev (K_aux (K_kind [BK_aux (BK_int, loc $startpos($1) $endpos($1))],
-					   loc $startpos($1) $endpos($1)), $2, mk_namesectn, $4),
+    { DEF_kind (KD_aux (KD_nabbrev (K_aux (K_int, loc $startpos($1) $endpos($1)), $2, mk_namesectn, $4),
 			loc $startpos $endpos)) }
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 630d5b1e..4b466326 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -598,12 +598,12 @@ let doc_quant_item_id ctx delimit (QI_aux (qi,_)) =
   | QI_id (KOpt_aux (KOpt_none kid,_)) ->
      if KBindings.mem kid ctx.kid_id_renames then None else
      Some (delimit (separate space [doc_var ctx kid; colon; string "Z"]))
-  | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (kind,_)],_),kid),_)) -> begin
+  | QI_id (KOpt_aux (KOpt_kind (K_aux (kind,_),kid),_)) -> begin
     if KBindings.mem kid ctx.kid_id_renames then None else
     match kind with
-    | BK_type -> Some (delimit (separate space [doc_var ctx kid; colon; string "Type"]))
-    | BK_int -> Some (delimit (separate space [doc_var ctx kid; colon; string "Z"]))
-    | BK_order -> None
+    | K_type -> Some (delimit (separate space [doc_var ctx kid; colon; string "Type"]))
+    | K_int -> Some (delimit (separate space [doc_var ctx kid; colon; string "Z"]))
+    | K_order -> None
   end
   | QI_id _ -> failwith "Quantifier with multiple kinds"
   | QI_const nc -> None
diff --git a/src/return_analysis.ml b/src/return_analysis.ml
index f60366fc..06565b01 100644
--- a/src/return_analysis.ml
+++ b/src/return_analysis.ml
@@ -114,7 +114,7 @@ let existentialize_annot funcl_annot annot =
        when Id.compare ty_id (mk_id "atom") = 0 ->
      let tyvars = Env.get_typ_vars funcl_env |> KBindings.bindings in
      let toplevel_kids =
-       List.filter (fun (kid, bk) -> match bk with BK_int -> true | _ -> false) tyvars |> List.map fst |> KidSet.of_list
+       List.filter (fun (kid, k) -> match k with K_int -> true | _ -> false) tyvars |> List.map fst |> KidSet.of_list
      in
      let new_kids = KidSet.diff (tyvars_of_nexp nexp) toplevel_kids in
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index f10c0059..2734e91f 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2096,7 +2096,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
         let quant_tyvars = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item qis) in
         let typ_tyvars = tyvars_of_typ fun_typ in
         let new_tyvars = KidSet.diff typ_tyvars quant_tyvars in
-        List.map (mk_qi_id BK_int) (KidSet.elements new_tyvars)
+        List.map (mk_qi_id K_int) (KidSet.elements new_tyvars)
       in
       let typquant = match typquant with
         | TypQ_aux (TypQ_tq qis, l) ->
@@ -2108,7 +2108,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
            in
            TypQ_aux (TypQ_tq qis, l)
         | _ ->
-           TypQ_aux (TypQ_tq (List.map (mk_qi_id BK_int) (KidSet.elements (tyvars_of_typ fun_typ))), l)
+           TypQ_aux (TypQ_tq (List.map (mk_qi_id K_int) (KidSet.elements (tyvars_of_typ fun_typ))), l)
       in
       let val_spec =
         VS_aux (VS_val_spec
diff --git a/src/specialize.ml b/src/specialize.ml
index 4d7a997f..6e625176 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -319,8 +319,8 @@ let specialize_id_valspec instantiations id ast =
        (* Remove type variables from the type quantifier. *)
        let kopts, constraints = quant_split typq in
        let kopts = List.filter (fun kopt -> not (is_typ_kopt kopt || is_order_kopt kopt)) kopts in
-       let typq = mk_typquant (List.map (mk_qi_id BK_type) typ_frees
-                               @ List.map (mk_qi_id BK_int) int_frees
+       let typq = mk_typquant (List.map (mk_qi_id K_type) typ_frees
+                               @ List.map (mk_qi_id K_int) int_frees
                                @ List.map mk_qi_kopt kopts
                                @ List.map mk_qi_nc constraints) in
        let typschm = mk_typschm typq typ in
diff --git a/src/type_check.ml b/src/type_check.ml
index 866aa071..d39ce27d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -209,11 +209,7 @@ and strip_kinded_id_aux = function
   | KOpt_none kid -> KOpt_none (strip_kid kid)
   | KOpt_kind (kind, kid) -> KOpt_kind (strip_kind kind, strip_kid kid)
 and strip_kind = function
-  | K_aux (k_aux, _) -> K_aux (strip_kind_aux k_aux, Parse_ast.Unknown)
-and strip_kind_aux = function
-  | K_kind base_kinds -> K_kind (List.map strip_base_kind base_kinds)
-and strip_base_kind = function
-  | BK_aux (bk_aux, _) -> BK_aux (bk_aux, Parse_ast.Unknown)
+  | K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown)
 
 let adding = Util.("Adding " |> darkgray |> clear)
 
@@ -250,11 +246,11 @@ module Env : sig
   val is_mutable : id -> t -> bool
   val get_constraints : t -> n_constraint list
   val add_constraint : n_constraint -> t -> t
-  val get_typ_var : kid -> t -> base_kind_aux
+  val get_typ_var : kid -> t -> kind_aux
   val get_typ_var_loc : kid -> t -> Ast.l
-  val get_typ_vars : t -> base_kind_aux KBindings.t
+  val get_typ_vars : t -> kind_aux KBindings.t
   val get_typ_var_locs : t -> Ast.l KBindings.t
-  val add_typ_var : l -> kid -> base_kind_aux -> t -> t
+  val add_typ_var : l -> kid -> kind_aux -> t -> t
   val get_ret_typ : t -> typ option
   val add_ret_typ : typ -> t -> t
   val add_typ_synonym : id -> (t -> typ_arg list -> typ) -> t -> t
@@ -320,7 +316,7 @@ end = struct
       registers : (effect * effect * typ) Bindings.t;
       variants : (typquant * type_union list) Bindings.t;
       mappings : (typquant * typ * typ) Bindings.t;
-      typ_vars : (Ast.l * base_kind_aux) KBindings.t;
+      typ_vars : (Ast.l * kind_aux) KBindings.t;
       typ_synonyms : (t -> typ_arg list -> typ) Bindings.t;
       num_defs : nexp Bindings.t;
       overloads : (id list) Bindings.t;
@@ -388,26 +384,26 @@ end = struct
   let get_typ_vars env = KBindings.map snd env.typ_vars
   let get_typ_var_locs env = KBindings.map fst env.typ_vars
 
-  let bk_counter = ref 0
-  let bk_name () = let kid = mk_kid ("bk#" ^ string_of_int !bk_counter) in incr bk_counter; kid
+  let k_counter = ref 0
+  let k_name () = let kid = mk_kid ("k#" ^ string_of_int !k_counter) in incr k_counter; kid
 
-  let kinds_typq kinds = mk_typquant (List.map (fun k -> mk_qi_id k (bk_name ())) kinds)
+  let kinds_typq kinds = mk_typquant (List.map (fun k -> mk_qi_id k (k_name ())) kinds)
 
   let builtin_typs =
     List.fold_left (fun m (name, kinds) -> Bindings.add (mk_id name) (kinds_typq kinds) m) Bindings.empty
-      [ ("range", [BK_int; BK_int]);
-        ("atom", [BK_int]);
-        ("vector", [BK_int; BK_order; BK_type]);
-        ("register", [BK_type]);
+      [ ("range", [K_int; K_int]);
+        ("atom", [K_int]);
+        ("vector", [K_int; K_order; K_type]);
+        ("register", [K_type]);
         ("bit", []);
         ("unit", []);
         ("int", []);
         ("nat", []);
         ("bool", []);
         ("real", []);
-        ("list", [BK_type]);
+        ("list", [K_type]);
         ("string", []);
-        ("itself", [BK_int])
+        ("itself", [K_int])
       ]
 
   let builtin_mappings =
@@ -517,10 +513,10 @@ end = struct
          try
            let (l, _) = KBindings.find kid env.typ_vars in
            rebindings := kid :: !rebindings;
-           { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) (l, BK_int) env.typ_vars }
+           { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) (l, K_int) env.typ_vars }
          with
          | Not_found ->
-            { env with typ_vars = KBindings.add kid (l, BK_int) env.typ_vars }
+            { env with typ_vars = KBindings.add kid (l, K_int) env.typ_vars }
        in
 
        let env = List.fold_left add_typ_var env kids in
@@ -612,9 +608,9 @@ end = struct
     | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id)
     | Typ_var kid -> begin
       match KBindings.find kid env.typ_vars with
-      | (_, BK_type) -> ()
+      | (_, K_type) -> ()
       | (_, k) -> typ_error l ("Kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ
-                               ^ " is " ^ string_of_base_kind_aux k ^ " rather than Type")
+                               ^ " is " ^ string_of_kind_aux k ^ " rather than Type")
       | exception Not_found ->
          typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ)
     end
@@ -646,10 +642,10 @@ end = struct
     | Nexp_var kid ->
        begin
          match get_typ_var kid env with
-         | BK_int -> ()
+         | K_int -> ()
          | kind -> typ_error l ("Constraint is badly formed, "
                                 ^ string_of_kid kid ^ " has kind "
-                                ^ string_of_base_kind_aux kind ^ " but should have kind Int")
+                                ^ string_of_kind_aux kind ^ " but should have kind Int")
        end
     | Nexp_constant _ -> ()
     | Nexp_app (id, nexps) ->
@@ -665,10 +661,10 @@ end = struct
     | Ord_var kid ->
        begin
          match get_typ_var kid env with
-         | BK_order -> ()
+         | K_order -> ()
          | kind -> typ_error l ("Order is badly formed, "
                                 ^ string_of_kid kid ^ " has kind "
-                                ^ string_of_base_kind_aux kind ^ " but should have kind Order")
+                                ^ string_of_kind_aux kind ^ " but should have kind Order")
        end
     | Ord_inc | Ord_dec -> ()
   and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc_aux, l) as nc) =
@@ -681,10 +677,10 @@ end = struct
     | NC_set (kid, _) when KidSet.mem kid exs -> ()
     | NC_set (kid, _) -> begin
         match get_typ_var kid env with
-        | BK_int -> ()
+        | K_int -> ()
         | kind -> typ_error l ("Set constraint is badly formed, "
                                ^ string_of_kid kid ^ " has kind "
-                               ^ string_of_base_kind_aux kind ^ " but should have kind Int")
+                               ^ string_of_kind_aux kind ^ " but should have kind Int")
       end
     | NC_or (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
     | NC_and (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
@@ -716,7 +712,7 @@ end = struct
   let get_val_spec id env =
     try
       let bind = Bindings.find id env.top_val_specs in
-      typ_debug (lazy ("get_val_spec: Env has " ^ string_of_list ", " (fun (kid, (_, bk)) -> string_of_kid kid ^ " => " ^ string_of_base_kind_aux bk) (KBindings.bindings env.typ_vars)));
+      typ_debug (lazy ("get_val_spec: Env has " ^ string_of_list ", " (fun (kid, (_, k)) -> string_of_kid kid ^ " => " ^ string_of_kind_aux k) (KBindings.bindings env.typ_vars)));
       let bind' = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in
       typ_debug (lazy ("get_val_spec: freshened to " ^ string_of_bind bind'));
       bind'
@@ -752,7 +748,7 @@ end = struct
        let existential_arg typq = function
          | None -> typq
          | Some (exs, nc, _) ->
-            List.fold_left (fun typq kid -> quant_add (mk_qi_id BK_int kid) typq) (quant_add (mk_qi_nc nc) typq) exs
+            List.fold_left (fun typq kid -> quant_add (mk_qi_id K_int kid) typq) (quant_add (mk_qi_nc nc) typq) exs
        in
        let typq = List.fold_left existential_arg typq base_args in
        let arg_typs = List.map2 (fun typ -> function Some (_, _, typ) -> typ | None -> typ) arg_typs base_args in
@@ -1003,7 +999,7 @@ end = struct
     then typ_error (kid_loc kid) ("type variable " ^ string_of_kid kid ^ " is already bound")
     else
       begin
-        typ_print (lazy (adding ^ "type variable " ^ string_of_kid kid ^ " : " ^ string_of_base_kind_aux k));
+        typ_print (lazy (adding ^ "type variable " ^ string_of_kid kid ^ " : " ^ string_of_kind_aux k));
         { env with typ_vars = KBindings.add kid (l, k) env.typ_vars }
       end
 
@@ -1116,9 +1112,8 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t =
     | QI_aux (qi, _) -> add_quant_item_aux env qi
   and add_quant_item_aux env = function
     | QI_const constr -> Env.add_constraint constr env
-    | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var l kid BK_int env
-    | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (k, _)], _), kid), _)) -> Env.add_typ_var l kid k env
-    | QI_id (KOpt_aux (_, l)) -> typ_error l "Type variable had non base kinds!"
+    | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var l kid K_int env
+    | QI_id (KOpt_aux (KOpt_kind (K_aux (k, _), kid), _)) -> Env.add_typ_var l kid k env
   in
   match quant with
   | TypQ_aux (TypQ_no_forall, _) -> env
@@ -1150,10 +1145,10 @@ let destruct_exist env typ =
   | _ -> None
 
 let add_existential l kids nc env =
-  let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env kids in
+  let env = List.fold_left (fun env kid -> Env.add_typ_var l kid K_int env) env kids in
   Env.add_constraint nc env
 
-let add_typ_vars l kids env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env kids
+let add_typ_vars l kids env = List.fold_left (fun env kid -> Env.add_typ_var l kid K_int env) env kids
 
 let is_exist = function
   | Typ_aux (Typ_exist (_, _, _), _) -> true
@@ -1344,7 +1339,7 @@ let solve env nexp =
       try KBindings.find kid !bindings with
       | Not_found -> fresh_var kid
     in
-    let env = Env.add_typ_var Parse_ast.Unknown (mk_kid "solve#") BK_int env in
+    let env = Env.add_typ_var Parse_ast.Unknown (mk_kid "solve#") K_int env in
     let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env))
                                  (nc_constraint env var_of (nc_eq (nvar (mk_kid "solve#")) nexp))
     in
@@ -1868,7 +1863,7 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t
      let env = match existential_kids, existential_nc with
        | [], None -> env
        | _, Some enc ->
-          let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env existential_kids in
+          let env = List.fold_left (fun env kid -> Env.add_typ_var l kid K_int env) env existential_kids in
           Env.add_constraint enc env
        | _, None -> assert false (* Cannot have existential_kids without existential_nc *)
      in
@@ -1945,16 +1940,16 @@ let infer_lit env (L_aux (lit_aux, l) as lit) =
   | L_undef -> typ_error l "Cannot infer the type of undefined"
 
 let is_nat_kid kid = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_int, _)], _), kid'), _) -> Kid.compare kid kid' = 0
+  | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid'), _) -> Kid.compare kid kid' = 0
   | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0
   | _ -> false
 
 let is_order_kid kid = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid'), _) -> Kid.compare kid kid' = 0
+  | KOpt_aux (KOpt_kind (K_aux (K_order, _), kid'), _) -> Kid.compare kid kid' = 0
   | _ -> false
 
 let is_typ_kid kid = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid'), _) -> Kid.compare kid kid' = 0
+  | KOpt_aux (KOpt_kind (K_aux (K_type, _), kid'), _) -> Kid.compare kid kid' = 0
   | _ -> false
 
 let rec instantiate_quants quants kid uvar = match quants with
@@ -2883,7 +2878,7 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _)
      begin
        match typ_nexps typ with
        | [nexp] ->
-          Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid BK_int env)
+          Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid K_int env)
        | [] ->
           typ_error l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to")
        | nexps ->
@@ -2896,7 +2891,7 @@ and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_arg_aux (typ_
   match typ_pat_aux, typ_arg_aux with
   | TP_wild, _ -> env
   | TP_var kid, Typ_arg_nexp nexp ->
-     Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid BK_int env)
+     Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid K_int env)
   | _, Typ_arg_typ typ -> bind_typ_pat env typ_pat typ
   | _, Typ_arg_order _ -> typ_error l "Cannot bind type pattern against order"
   | _, _ -> typ_error l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat)
@@ -3238,7 +3233,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        match destruct_numeric env (typ_of inferred_f), destruct_numeric env (typ_of inferred_t) with
        | Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) ->
           let loop_kid = mk_kid ("loop_" ^ string_of_id v) in
-          let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env (loop_kid :: kids1 @ kids2) in
+          let env = List.fold_left (fun env kid -> Env.add_typ_var l kid K_int env) env (loop_kid :: kids1 @ kids2) in
           let env = Env.add_constraint (nc_and nc1 nc2) env in
           let env = Env.add_constraint (nc_and (nc_lteq nexp1 (nvar loop_kid)) (nc_lteq (nvar loop_kid) nexp2)) env in
           let loop_vtyp = atom_typ (nvar loop_kid) in
@@ -3392,7 +3387,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
              | [], None -> env
              | _, Some enc ->
                 let enc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) nc) enc ex_kids in
-                let env = List.fold_left (fun env kid -> Env.add_typ_var l (prepend_kid ex_tag kid) BK_int env) env ex_kids in
+                let env = List.fold_left (fun env kid -> Env.add_typ_var l (prepend_kid ex_tag kid) K_int env) env ex_kids in
                 Env.add_constraint enc env
              | _, None -> assert false (* Cannot have ex_kids without ex_nc *)
            in
@@ -3428,7 +3423,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
          typ_debug (lazy (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)));
          if ex_kids = [] then () else (typ_debug (lazy ("EX GOAL: " ^ string_of_option string_of_n_constraint ex_nc)); ex_goal := ex_nc);
          record_unifiers unifiers;
-         let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env ex_kids in
+         let env = List.fold_left (fun env kid -> Env.add_typ_var l kid K_int env) env ex_kids in
          let typs' = List.map (subst_unifiers unifiers) typs in
          let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in
          let ret_typ' =
@@ -4385,12 +4380,11 @@ let kinded_id_arg kind_id =
   let typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) in
   match kind_id with
   | KOpt_aux (KOpt_none kid, _) -> typ_arg (Typ_arg_nexp (nvar kid))
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_int, _)], _), kid), _) -> typ_arg (Typ_arg_nexp (nvar kid))
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid), _) ->
+  | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid), _) -> typ_arg (Typ_arg_nexp (nvar kid))
+  | KOpt_aux (KOpt_kind (K_aux (K_order, _), kid), _) ->
      typ_arg (Typ_arg_order (Ord_aux (Ord_var kid, Parse_ast.Unknown)))
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid), _) ->
+  | KOpt_aux (KOpt_kind (K_aux (K_type, _), kid), _) ->
      typ_arg (Typ_arg_typ (mk_typ (Typ_var kid)))
-  | KOpt_aux (KOpt_kind (K_aux (K_kind kinds, _), kid), l) -> typ_error l "Badly formed kind"
 
 let fold_union_quant quants (QI_aux (qi, l)) =
   match qi with
@@ -4401,7 +4395,7 @@ let check_type_union env variant typq (Tu_aux (tu, l)) =
   let ret_typ = app_typ variant (List.fold_left fold_union_quant [] (quant_items typq)) in
   match tu with
   | Tu_ty_id (Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) as typ, v) ->
-     let typq = mk_typquant (List.map (mk_qi_id BK_type) (KidSet.elements (typ_frees typ))) in
+     let typq = mk_typquant (List.map (mk_qi_id K_type) (KidSet.elements (typ_frees typ))) in
      env
      |> Env.add_union_id v (typq, typ)
      |> Env.add_val_spec v (typq, typ)
@@ -4441,7 +4435,7 @@ let mk_synonym typq typ =
 let check_kinddef env (KD_aux (kdef, (l, _))) =
   let kd_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented kind def") in
   match kdef with
-  | KD_nabbrev ((K_aux(K_kind([BK_aux (BK_int, _)]),_) as kind), id, nmscm, nexp) ->
+  | KD_nabbrev (K_aux (K_int, _) as kind, id, nmscm, nexp) ->
      [DEF_kind (KD_aux (KD_nabbrev (kind, id, nmscm, nexp), (l, None)))],
      Env.add_num_def id nexp env
   | _ -> kd_err ()
diff --git a/src/type_check.mli b/src/type_check.mli
index 1081af08..f08272de 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -127,13 +127,13 @@ module Env : sig
 
   val add_constraint : n_constraint -> t -> t
 
-  val get_typ_var : kid -> t -> base_kind_aux
+  val get_typ_var : kid -> t -> kind_aux
 
-  val get_typ_vars : t -> base_kind_aux KBindings.t
+  val get_typ_vars : t -> kind_aux KBindings.t
 
   val get_typ_var_locs : t -> Ast.l KBindings.t
 
-  val add_typ_var : Ast.l -> kid -> base_kind_aux -> t -> t
+  val add_typ_var : Ast.l -> kid -> kind_aux -> t -> t
 
   val is_record : id -> t -> bool