TC: report length found vs length expected in vector literal errors

src/lib/type_check.ml

@@ -2385,7 +2385,11 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
           (tyvars, nc, elem_typ)
         )
         else if prove __POS__ env (nc_eq (nint literal_len) (nexp_simp len)) then (tyvars, nc, elem_typ)
-        else typ_error l "Vector literal with incorrect length"
+        else
+          typ_error l
+            ("Vector literal with incorrect length: found " ^ string_of_int literal_len ^ " elements, but expected "
+           ^ string_of_nexp len
+            )
       in
       match check_or_infer_sequence ~at:l env vec tyvars nc (Some elem_typ) with
       | Some (vec, elem_typ) ->

test/typecheck/fail/vector_lit_length.expect

@@ -0,0 +1,5 @@
+Type error:
+fail/vector_lit_length.sail:4.27-33:
+4 |  let v : vector(1, int) = [1, 2];
+  |                           ^----^
+  | Vector literal with incorrect length: found 2 elements, but expected 1

test/typecheck/fail/vector_lit_length.sail

@@ -0,0 +1,6 @@
+default Order dec
+
+function test() -> unit = {
+  let v : vector(1, int) = [1, 2];
+  ()
+}