Experiment with making vector and bitvector distinct types

Only change that should be needed for 99.9% of uses is to change
vector('n, 'ord, bit) to bitvector('n, 'ord), and adding

$ifndef FEATURE_BITVECTOR_TYPE
type bitvector('n, dec) = vector('n, dec, bit)
$endif

for to support any Sail before this

Currently I have all C, Typechecking, and SMT tests passing, as well
as the RISC-V spec building OCaml and C completely unmodified.

31 files changed, 107 insertions, 143 deletions

diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect
index c40aa5ec..5c52861f 100644
--- a/test/typecheck/pass/Replicate/v1.expect
+++ b/test/typecheck/pass/Replicate/v1.expect
@@ -2,7 +2,7 @@ Type error:
 [Replicate/v1.sail]:14:4-30
 14 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from bitvector(('M * div('N, 'M)), dec) to bitvector('N, dec) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index acadd4e2..7d4891f9 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [Replicate/v2.sail]:13:4-30
 13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from {('ex119# : Int), true. vector(('M * 'ex119#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from {('ex128# : Int), true. bitvector(('M * 'ex128#), dec)} to bitvector('N, dec) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail
index 7e5c873a..cf29212f 100644
--- a/test/typecheck/pass/add_vec_lit.sail
+++ b/test/typecheck/pass/add_vec_lit.sail
@@ -1,13 +1,13 @@
 default Order inc
 
 val add_vec = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
-  (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit)
+  (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
 val add_range = {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
 val cast unsigned : forall ('n : Int).
-  vector('n, inc, bit) -> range(0, 2 ^ 'n - 1)
+  bitvector('n, inc) -> range(0, 2 ^ 'n - 1)
 
 overload operator + = {add_vec, add_range}
 
diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail
index 2021bf67..3f4b8632 100644
--- a/test/typecheck/pass/arm_FPEXC1.sail
+++ b/test/typecheck/pass/arm_FPEXC1.sail
@@ -1,17 +1,17 @@
 default Order dec
 
 val vector_access = {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall ('n : Int).
-  (vector('n, dec, bit), int) -> bit
+  (bitvector('n, dec), int) -> bit
 
 val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
-  (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit)
+  (bitvector('n, dec), atom('m), atom('o)) -> bitvector('m - ('o - 1), dec)
 
 val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
-  (vector('n, dec, bit), atom('m), atom('o), vector('m - ('o - 1), dec, bit)) -> vector('n, dec, bit)
+  (bitvector('n, dec), atom('m), atom('o), bitvector('m - ('o - 1), dec)) -> bitvector('n, dec)
 
-register _FPEXC32_EL2 : vector(32, dec, bit)
+register _FPEXC32_EL2 : bitvector(32, dec)
 
-val set_FPEXC32_EL2 : vector(32, dec, bit) -> unit effect {wreg}
+val set_FPEXC32_EL2 : bitvector(32, dec) -> unit effect {wreg}
 
 function set_FPEXC32_EL2 value_name = {
   _FPEXC32_EL2[0 .. 0] = [value_name[0]];
@@ -26,10 +26,10 @@ function set_FPEXC32_EL2 value_name = {
   _FPEXC32_EL2[30 .. 30] = [value_name[30]]
 }
 
-val get_FPEXC32_EL2 : unit -> vector(32, dec, bit) effect {rreg}
+val get_FPEXC32_EL2 : unit -> bitvector(32, dec) effect {rreg}
 
 function get_FPEXC32_EL2 () = {
-  value_name : vector(32, dec, bit) = 0x04000700;
+  value_name : bitvector(32, dec) = 0x04000700;
   value_name[0 .. 0] = [_FPEXC32_EL2[0]];
   value_name[1 .. 1] = [_FPEXC32_EL2[1]];
   value_name[2 .. 2] = [_FPEXC32_EL2[2]];
@@ -44,11 +44,11 @@ function get_FPEXC32_EL2 () = {
   value_name
 }
 
-val set_FPEXC : vector(32, dec, bit) -> unit effect {rreg, wreg}
+val set_FPEXC : bitvector(32, dec) -> unit effect {rreg, wreg}
 
 function set_FPEXC val_name = {
-  r : vector(32, dec, bit) = val_name;
-  __tmp_45 : vector(32, dec, bit) = get_FPEXC32_EL2();
+  r : bitvector(32, dec) = val_name;
+  __tmp_45 : bitvector(32, dec) = get_FPEXC32_EL2();
   __tmp_45[31 .. 0] = r;
   set_FPEXC32_EL2(__tmp_45)
 }
diff --git a/test/typecheck/pass/bitfield_pc.sail b/test/typecheck/pass/bitfield_pc.sail
index 9764289a..889e27ce 100644
--- a/test/typecheck/pass/bitfield_pc.sail
+++ b/test/typecheck/pass/bitfield_pc.sail
@@ -1,6 +1,8 @@
+default Order dec
+
 $include <vector_dec.sail>
 
-bitfield PC_t : vector(16, dec, bit) = {
+bitfield PC_t : bitvector(16, dec) = {
   H : 15 .. 8,
   L :  7 .. 0
 }
diff --git a/test/typecheck/pass/bitvector_param.sail b/test/typecheck/pass/bitvector_param.sail
index 77fe7dc3..784a77f9 100644
--- a/test/typecheck/pass/bitvector_param.sail
+++ b/test/typecheck/pass/bitvector_param.sail
@@ -1,32 +1,7 @@
 default Order dec
 
 $include <flow.sail>
-
-type bits ('n : Int) = vector('n, dec, bit)
-
-val vector_subrange = {
-  ocaml: "subrange",
-  lem: "subrange_vec_dec",
-  c: "vector_subrange",
-  coq: "subrange_vec_dec"
-} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
-  (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1)
-
-val vector_update_subrange_dec = {ocaml: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
-  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
-
-val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o.
-  (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit)
-
-overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc}
-
-val bitvector_concat = {c: "append", ocaml: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
-  (bits('n), bits('m)) -> bits('n + 'm)
-
-val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
-  (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
-
-overload append = {bitvector_concat, vector_concat}
+$include <vector_dec.sail>
 
 type xlen : Int = 64
 type ylen : Int = 1
diff --git a/test/typecheck/pass/decode_patterns.sail b/test/typecheck/pass/decode_patterns.sail
index d54e9416..6f28ec18 100644
--- a/test/typecheck/pass/decode_patterns.sail
+++ b/test/typecheck/pass/decode_patterns.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-val decode : vector(16, dec, bit) -> unit
+val decode : bitvector(16, dec) -> unit
 
 scattered function decode
 
@@ -22,11 +22,11 @@ function clause decode 0x00 @ 0b001 @ [b : bit] @ 0x0 =
 
 end decode
 
-val decode2 : vector(16, dec, bit) -> unit
+val decode2 : bitvector(16, dec) -> unit
 
 function decode2 x =
   match x {
-    0x00 @ 0b000 @ [b : bit]  @ 0x0 =>
+    0x00 @ 0b000 @ [b : bit] @ 0x0 =>
       if b == bitone then {
         ()
       } else {
diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail
index de15edf8..1d0e1d20 100644
--- a/test/typecheck/pass/exist_tlb.sail
+++ b/test/typecheck/pass/exist_tlb.sail
@@ -1,17 +1,17 @@
 $include <flow.sail>
 
 val extz : forall ('n : Int) ('m : Int) ('ord : Order).
-  vector('n, 'ord, bit) -> vector('m, 'ord, bit)
+  bitvector('n, 'ord) -> bitvector('m, 'ord)
 
 val exts : forall ('n : Int) ('m : Int) ('ord : Order).
-  vector('n, 'ord, bit) -> vector('m, 'ord, bit)
+  bitvector('n, 'ord) -> bitvector('m, 'ord)
 
 overload EXTZ = {extz}
 
 overload EXTS = {exts}
 
 val add_vec : forall ('n : Int) ('ord : Order).
-  (vector('n, 'ord, bit), vector('n, 'ord, bit)) -> vector('n, 'ord, bit)
+  (bitvector('n, 'ord), bitvector('n, 'ord)) -> bitvector('n, 'ord)
 
 overload operator + = {add_vec}
 
@@ -21,15 +21,15 @@ overload ~ = {bool_not}
 
 default Order dec
 
-register CP0LLBit : vector(1, dec, bit)
+register CP0LLBit : bitvector(1, dec)
 
-register CP0LLAddr : vector(64, dec, bit)
+register CP0LLAddr : bitvector(64, dec)
 
 enum MemAccessType = {Instruction, LoadData, StoreData}
 
-type regno = vector(5, dec, bit)
+type regno = bitvector(5, dec)
 
-type imm16 = vector(16, dec, bit)
+type imm16 = bitvector(16, dec)
 
 enum Exception = {
   EInt,
@@ -55,12 +55,12 @@ enum Exception = {
 
 enum WordType = {B, H, W, D}
 
-val rGPR : vector(5, dec, bit) -> vector(64, dec, bit) effect {rreg}
+val rGPR : bitvector(5, dec) -> bitvector(64, dec) effect {rreg}
 
-val isAddressAligned : (vector(64, dec, bit), WordType) -> bool
+val isAddressAligned : (bitvector(64, dec), WordType) -> bool
 
 val SignalExceptionBadAddr : forall ('o : Type).
-  (Exception, vector(64, dec, bit)) -> 'o
+  (Exception, bitvector(64, dec)) -> 'o
 
 val wordWidthBytes : WordType -> {|1, 2, 4, 8|}
 
@@ -72,29 +72,29 @@ function wordWidthBytes w = match w {
 }
 
 val MEMr_reserve_wrapper : forall ('n : Int).
-  (vector(64, dec, bit), atom('n)) -> vector(8 * 'n, dec, bit) effect {rmem}
+  (bitvector(64, dec), atom('n)) -> bitvector(8 * 'n, dec) effect {rmem}
 
 val MEMr_wrapper : forall ('n : Int).
-  (vector(64, dec, bit), atom('n)) -> vector(8 * 'n, dec, bit) effect {rmem}
+  (bitvector(64, dec), atom('n)) -> bitvector(8 * 'n, dec) effect {rmem}
 
-val wGPR : (vector(5, dec, bit), vector(64, dec, bit)) -> unit effect {wreg}
+val wGPR : (bitvector(5, dec), bitvector(64, dec)) -> unit effect {wreg}
 
-val addrWrapper : (vector(64, dec, bit), MemAccessType, WordType) -> vector(64, dec, bit)
+val addrWrapper : (bitvector(64, dec), MemAccessType, WordType) -> bitvector(64, dec)
 
-function addrWrapper (addr : vector(64, dec, bit), accessType : MemAccessType, width : WordType) = addr
+function addrWrapper (addr : bitvector(64, dec), accessType : MemAccessType, width : WordType) = addr
 
-val TLBTranslate : (vector(64, dec, bit), MemAccessType) -> vector(64, dec, bit)
+val TLBTranslate : (bitvector(64, dec), MemAccessType) -> bitvector(64, dec)
 
-function TLBTranslate (vAddr : vector(64, dec, bit), accessType : MemAccessType) = vAddr
+function TLBTranslate (vAddr : bitvector(64, dec), accessType : MemAccessType) = vAddr
 
 union ast = {Load : (WordType, bool, bool, regno, regno, imm16)}
 
 val execute : ast -> unit effect {rmem, rreg, wreg}
 
 function execute Load(width, signed, linked, base, rt, offset) = {
-  vAddr : vector(64, dec, bit) = addrWrapper(EXTS(offset) + rGPR(base), LoadData, width);
+  vAddr : bitvector(64, dec) = addrWrapper(EXTS(offset) + rGPR(base), LoadData, width);
   if ~(isAddressAligned(vAddr, width)) then SignalExceptionBadAddr(AdEL, vAddr) else let pAddr = TLBTranslate(vAddr, LoadData) in {
-    memResult : {'t, 't in {1, 2, 4, 8}. vector(8 * 't, dec, bit)} = if linked then {
+    memResult : {'t, 't in {1, 2, 4, 8}. bitvector(8 * 't, dec)} = if linked then {
       CP0LLBit = 0b1;
       CP0LLAddr = pAddr;
       MEMr_reserve_wrapper(pAddr, wordWidthBytes(width))
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index 7bb8a4ab..78711c2b 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex196#)
+   | * datasize('ex205#)
    | 
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index 4b9bd7cc..40657d0c 100644
--- a/test/typecheck/pass/existential_ast3/v1.expect
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))
    | Coercion failed because:
-   | (int(33), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#))
+   | (int(33), int('ex167#)) is not a subtype of (int('ex162#), int('ex163#))
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex153# bound here
+   |    | 'ex162# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex154# bound here
+   |    | 'ex163# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex158# bound here
+   |    | 'ex167# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index 52eb2f13..8954736e 100644
--- a/test/typecheck/pass/existential_ast3/v2.expect
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))
    | Coercion failed because:
-   | (int(31), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#))
+   | (int(31), int('ex167#)) is not a subtype of (int('ex162#), int('ex163#))
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex153# bound here
+   |    | 'ex162# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex154# bound here
+   |    | 'ex163# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex158# bound here
+   |    | 'ex167# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index 0e43cd52..d0fcdc06 100644
--- a/test/typecheck/pass/existential_ast3/v3.expect
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -3,5 +3,5 @@ Type error:
 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
    |         ^-----------------------------^
    | Could not resolve quantifiers for Ctor
-   | * (datasize(64) & (0 <= 'ex197# & ('ex197# + 1) <= 64))
+   | * (datasize(64) & (0 <= 'ex206# & ('ex206# + 1) <= 64))
    | 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index 011ecbdf..e236d4b6 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -5,8 +5,7 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex115# & ('ex115# + 1) <= 3)
+   |    * (0 <= 'ex124# & ('ex124# + 1) <= 3)
    | * plain_vector_access
-   |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex118# & ('ex118# + 1) <= 3)
+   |    No valid casts resulted in unification
    | 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index 9a34f688..fa7fb9ff 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -5,8 +5,7 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex115# & ('ex115# + 1) <= 4)
+   |    * (0 <= 'ex124# & ('ex124# + 1) <= 4)
    | * plain_vector_access
-   |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex118# & ('ex118# + 1) <= 4)
+   |    No valid casts resulted in unification
    | 
diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect
index 7e0e74bb..b7447d0f 100644
--- a/test/typecheck/pass/if_infer/v3.expect
+++ b/test/typecheck/pass/if_infer/v3.expect
@@ -6,5 +6,5 @@ Type error:
    | * bitvector_access
    |    Numeric type is non-simple
    | * plain_vector_access
-   |    Numeric type is non-simple
+   |    No valid casts resulted in unification
    | 
diff --git a/test/typecheck/pass/nexp_synonym/v1.expect b/test/typecheck/pass/nexp_synonym/v1.expect
index 9ba21c2c..2f547747 100644
--- a/test/typecheck/pass/nexp_synonym/v1.expect
+++ b/test/typecheck/pass/nexp_synonym/v1.expect
@@ -2,7 +2,7 @@ Type error:
 [nexp_synonym/v1.sail]:7:20-31
 7 |let v : bits(LEN) = 0xFFFF_FFFF
   |                    ^---------^
-  | Tried performing type coercion from vector(32, dec, bit) to bits(LEN) on 0xFFFFFFFF
+  | Tried performing type coercion from bitvector(32, dec) to bits(LEN) on 0xFFFFFFFF
   | Coercion failed because:
   | Mismatched argument types in subtype check
   | 
diff --git a/test/typecheck/pass/nexp_synonym/v2.expect b/test/typecheck/pass/nexp_synonym/v2.expect
index 68d664f7..c4bd774c 100644
--- a/test/typecheck/pass/nexp_synonym/v2.expect
+++ b/test/typecheck/pass/nexp_synonym/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [nexp_synonym/v2.sail]:7:20-32
 7 |let v : bits(LEN) = 0xFFFF_FFFFF
   |                    ^----------^
-  | Tried performing type coercion from vector(36, dec, bit) to bits(LEN) on 0xFFFFFFFFF
+  | Tried performing type coercion from bitvector(36, dec) to bits(LEN) on 0xFFFFFFFFF
   | Coercion failed because:
   | Mismatched argument types in subtype check
   | 
diff --git a/test/typecheck/pass/nlflow.sail b/test/typecheck/pass/nlflow.sail
index 95d2d280..9c426819 100644
--- a/test/typecheck/pass/nlflow.sail
+++ b/test/typecheck/pass/nlflow.sail
@@ -7,7 +7,7 @@ $include <exception_basic.sail>
 
 val foo : forall 'n, 'n != 8. int('n) -> unit
 
-function test(xs: vector(4, dec, bit)) -> unit = {
+function test(xs: bitvector(4, dec)) -> unit = {
   if xs == 0b1000 then {
     throw(Exception())
   };
diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail
index dc625084..dd1734f6 100644
--- a/test/typecheck/pass/nzcv.sail
+++ b/test/typecheck/pass/nzcv.sail
@@ -1,9 +1,9 @@
 default Order dec
 
 val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
-  (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit)
+  (bitvector('n, dec), atom('m), atom('o)) -> bitvector('m - ('o - 1), dec)
 
-val test : vector(4, dec, bit) -> unit
+val test : bitvector(4, dec) -> unit
 
 function test nzcv = {
   N = 0b0;
diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail
index 1d7e15b1..02453c72 100644
--- a/test/typecheck/pass/procstate1.sail
+++ b/test/typecheck/pass/procstate1.sail
@@ -2,13 +2,13 @@ default Order dec
 
 infix 4 ==
 
-val operator == = {lem: "eq_vec"} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
+val operator == = {lem: "eq_vec"} : forall 'n. (bitvector('n, dec), bitvector('n, dec)) -> bool
 
 struct ProcState ('n : Int) = {
-  N : vector('n, dec, bit),
-  Z : vector(1, dec, bit),
-  C : vector(1, dec, bit),
-  V : vector(1, dec, bit)
+  N : bitvector('n, dec),
+  Z : bitvector(1, dec),
+  C : bitvector(1, dec),
+  V : bitvector(1, dec)
 }
 
 register PSTATE : ProcState(1)
diff --git a/test/typecheck/pass/pure_record.sail b/test/typecheck/pass/pure_record.sail
index 15f14a3b..fe324914 100644
--- a/test/typecheck/pass/pure_record.sail
+++ b/test/typecheck/pass/pure_record.sail
@@ -1,24 +1,24 @@
 default Order dec
 
-struct State ('a : Type) = {
-  N : vector(1, dec, 'a),
-  Z : vector(1, dec, bit)
+struct State = {
+  N : bitvector(1, dec),
+  Z : bitvector(1, dec)
 }
 
-val myStateM : unit -> State(bit) effect {undef}
+val myStateM : unit -> State effect {undef}
 
 function myStateM () = {
-  r : State(bit) = undefined;
+  r : State = undefined;
   r.N = 0b1;
   r.Z = 0b1;
   r
 }
 
-let myState : State(bit) = struct { N = 0b1, Z = 0b1 }
+let myState : State = struct { N = 0b1, Z = 0b1 }
 
 val test : unit -> unit effect {undef}
 
 function test () = {
-  myState2 : State(bit) = struct { N = undefined, Z = 0b1 };
-  myState3 : State(bit) = { myState2 with N = 0b0 }
+  myState2 : State = struct { N = undefined, Z = 0b1 };
+  myState3 : State = { myState2 with N = 0b0 }
 }
diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail
index 588fd324..fe6651db 100644
--- a/test/typecheck/pass/pure_record2.sail
+++ b/test/typecheck/pass/pure_record2.sail
@@ -1,24 +1,24 @@
 default Order dec
 
-struct State('a: Type, 'n: Int) = {
-  N : vector('n, dec, 'a),
-  Z : vector(1, dec, bit)
+struct State('n: Int) = {
+  N : bitvector('n, dec),
+  Z : bitvector(1, dec)
 }
 
-val myStateM : unit -> State(bit, 1) effect {undef}
+val myStateM : unit -> State(1) effect {undef}
 
 function myStateM () = {
-  r : State(bit, 1) = undefined;
+  r : State(1) = undefined;
   r.N = 0b1;
   r.Z = 0b1;
   r
 }
 
-let myState : State(bit, 1) = struct { N = 0b1, Z = 0b1 }
+let myState : State(1) = struct { N = 0b1, Z = 0b1 }
 
 val test : unit -> unit effect {undef}
 
 function test () = {
-  myState2 : State(bit, 1) = struct { N = undefined, Z = 0b1 };
-  myState3 : State(bit, 1) = { myState2 with N = 0b0 }
+  myState2 : State(1) = struct { N = undefined, Z = 0b1 };
+  myState3 : State(1) = { myState2 with N = 0b0 }
 }
diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail
index de388c3e..b1080a1a 100644
--- a/test/typecheck/pass/pure_record3.sail
+++ b/test/typecheck/pass/pure_record3.sail
@@ -1,27 +1,27 @@
 default Order dec
 
-struct State('a: Type, 'n: Int) = {
-  N : vector('n, dec, 'a),
-  Z : vector(1, dec, bit)
+struct State('n: Int) = {
+  N : bitvector('n, dec),
+  Z : bitvector(1, dec)
 }
 
-register procState : State(bit, 1)
+register procState : State(1)
 
-val myStateM : unit -> State(bit, 1) effect {undef}
+val myStateM : unit -> State(1) effect {undef}
 
 function myStateM () = {
-  r : State(bit, 1) = undefined;
+  r : State(1) = undefined;
   r.N = 0b1;
   r.Z = 0b1;
   r
 }
 
-let myState : State(bit, 1) = struct { N = 0b1, Z = 0b1 }
+let myState : State(1) = struct { N = 0b1, Z = 0b1 }
 
 val test : unit -> unit effect {undef}
 
 function test () = {
-  myState1 : State(bit, 1) = undefined;
-  myState2 : State(bit, 1) = struct { N = undefined, Z = 0b1 };
-  myState3 : State(bit, 1) = { myState2 with N = 0b0 }
+  myState1 : State(1) = undefined;
+  myState2 : State(1) = struct { N = undefined, Z = 0b1 };
+  myState3 : State(1) = { myState2 with N = 0b0 }
 }
diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect
index f007c917..24439bed 100644
--- a/test/typecheck/pass/reg_32_64/v2.expect
+++ b/test/typecheck/pass/reg_32_64/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [reg_32_64/v2.sail]:21:18-22
 21 |  (*R)['d .. 0] = data
    |                  ^--^
-   | Tried performing type coercion from vector('d, dec, bit) to vector((('d - 0) + 1), dec, bit) on data
+   | Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | This error occured because of a previous error:
diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect
index ce61cf2a..36bd848e 100644
--- a/test/typecheck/pass/vec_length/v1.expect
+++ b/test/typecheck/pass/vec_length/v1.expect
@@ -7,6 +7,5 @@ Type error:
   |    Could not resolve quantifiers for bitvector_access
   |    * (0 <= 10 & (10 + 1) <= 8)
   | * plain_vector_access
-  |    Could not resolve quantifiers for plain_vector_access
-  |    * (0 <= 10 & (10 + 1) <= 8)
+  |    No valid casts resulted in unification
   | 
diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect
index 3d40cdb0..efbfcc54 100644
--- a/test/typecheck/pass/vec_length/v1_inc.expect
+++ b/test/typecheck/pass/vec_length/v1_inc.expect
@@ -7,6 +7,5 @@ Type error:
   |    Could not resolve quantifiers for bitvector_access
   |    * (0 <= 10 & (10 + 1) <= 8)
   | * plain_vector_access
-  |    Could not resolve quantifiers for plain_vector_access
-  |    * (0 <= 10 & (10 + 1) <= 8)
+  |    No valid casts resulted in unification
   | 
diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect
index c77ecaa7..9ce8f9a2 100644
--- a/test/typecheck/pass/vec_length/v2.expect
+++ b/test/typecheck/pass/vec_length/v2.expect
@@ -7,6 +7,5 @@ Type error:
   |    Could not resolve quantifiers for bitvector_update
   |    * (0 <= 10 & (10 + 1) <= 8)
   | * plain_vector_update
-  |    Could not resolve quantifiers for plain_vector_update
-  |    * (0 <= 10 & (10 + 1) <= 8)
+  |    No valid casts resulted in unification
   | 
diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect
index cff65f62..dba312ea 100644
--- a/test/typecheck/pass/vec_length/v2_inc.expect
+++ b/test/typecheck/pass/vec_length/v2_inc.expect
@@ -7,6 +7,5 @@ Type error:
   |    Could not resolve quantifiers for bitvector_update
   |    * (0 <= 10 & (10 + 1) <= 8)
   | * plain_vector_update
-  |    Could not resolve quantifiers for plain_vector_update
-  |    * (0 <= 10 & (10 + 1) <= 8)
+  |    No valid casts resulted in unification
   | 
diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect
index e3afecee..88e6fa50 100644
--- a/test/typecheck/pass/vec_length/v3.expect
+++ b/test/typecheck/pass/vec_length/v3.expect
@@ -9,6 +9,5 @@ Type error:
    |    Could not resolve quantifiers for bitvector_access
    |    * (0 <= 10 & (10 + 1) <= 8)
    | * plain_vector_access
-   |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 10 & (10 + 1) <= 8)
+   |    No valid casts resulted in unification
    | 
diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail
index 6de87a8c..e11a8654 100644
--- a/test/typecheck/pass/vec_pat1.sail
+++ b/test/typecheck/pass/vec_pat1.sail
@@ -1,15 +1,15 @@
 default Order inc
 
 val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
-  (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit)
+  (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
 val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"}: forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
-  (vector('l, inc, bit), atom('m), atom('o)) -> vector('o + 1 - 'm, inc, bit)
+  (bitvector('l, inc), atom('m), atom('o)) -> bitvector('o + 1 - 'm, inc)
 
 val bitvector_concat = {ocaml: "append", lem: "concat_vec"} : forall ('m : Int) ('p : Int).
-  (vector('m, inc, bit), vector('p, inc, bit)) -> vector('m + 'p, inc, bit)
+  (bitvector('m, inc), bitvector('p, inc)) -> bitvector('m + 'p, inc)
 
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (vector('n, inc, bit), vector('n, inc, bit)) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bitvector('n, inc), bitvector('n, inc)) -> bool
 
 infix 4 ==
 overload operator == = {eq_vec}
@@ -18,6 +18,6 @@ overload operator + = {bv_add}
 
 overload append = {bitvector_concat}
 
-val test : (vector(3, inc, bit), vector(3, inc, bit)) -> vector(3, inc, bit)
+val test : (bitvector(3, inc), bitvector(3, inc)) -> bitvector(3, inc)
 
-function test (x : vector(1, inc, bit) @ 0b1 @ 0b0, z) = (x @ 0b11) + z
+function test (x : bitvector(1, inc) @ 0b1 @ 0b0, z) = (x @ 0b11) + z
diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail
index b82d6c8c..9f7f4e49 100644
--- a/test/typecheck/pass/vector_subrange_gen.sail
+++ b/test/typecheck/pass/vector_subrange_gen.sail
@@ -1,23 +1,17 @@
 
-val vector_access : forall ('l : Int) ('o : Order) ('a : Type), 'l >= 0.
-  (vector('l, 'o, 'a), range(0, 'l - 1)) -> 'a
-
-val vector_append : forall ('l1 : Int) ('l2 : Int) ('o : Order) ('a : Type), 'l1 >= 0 & 'l2 >= 0.
-  (vector('l1, 'o, 'a), vector('l2, 'o, 'a)) -> vector('l1 + 'l2, 'o, 'a)
-
 val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
-  (vector('l, inc, bit), atom('m), atom('o)) -> vector('o - 'm + 1, inc, bit)
+  (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 "length" : forall ('n : Int). vector('n, inc, bit) -> atom('n)
+val bitvector_length = "length" : forall ('n : Int). bitvector('n, inc) -> atom('n)
 
-overload __size = {length}
+overload __size = {bitvector_length}
 
 default Order inc
 
 val test : forall 'n 'm, 'n >= 5.
-  vector('n, inc, bit) -> vector('n - 1, inc, bit)
+  bitvector('n, inc) -> bitvector('n - 1, inc)
 
 function test v = {
   z = vector_subrange(v, 0, sub('n, 2));