diff --git a/lib/vector.sail b/lib/vector.sail
index 355287a1b..49e522f57 100644
--- a/lib/vector.sail
+++ b/lib/vector.sail
@@ -397,6 +397,6 @@ val signed = pure {
 
 $endif
 
-overload __size = {__id, bitvector_length}
+overload __size = {__id, bitvector_length, vector_length}
 
 $endif
diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml
index 26ba2e377..9f8c800dd 100644
--- a/src/lib/type_check.ml
+++ b/src/lib/type_check.ml
@@ -1145,6 +1145,8 @@ let rec rewrite_sizeof' l env (Nexp_aux (aux, _) as nexp) =
         | Typ_app (id, [A_aux (A_nexp n, _)]) when string_of_id id = "atom" -> prove __POS__ env (nc_eq (nvar v) n)
         | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)]) when string_of_id id = "bitvector" ->
             Kid.compare v v' = 0
+        | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _); _]) when string_of_id id = "vector" ->
+            Kid.compare v v' = 0
         | _ -> false
       in
       begin
diff --git a/test/typecheck/pass/implicit_vector.sail b/test/typecheck/pass/implicit_vector.sail
new file mode 100644
index 000000000..c6a86fd76
--- /dev/null
+++ b/test/typecheck/pass/implicit_vector.sail
@@ -0,0 +1,7 @@
+default Order dec
+$include <prelude.sail>
+
+val f : forall 'n, 'n > 0. (implicit('n), vector('n, int)) -> unit
+val g : forall 'n, 'n > 0. vector('n, int) -> unit
+
+function g(bv) = f(bv)