More error messages improvments

30 files changed, 128 insertions, 151 deletions

diff --git a/src/error_format.ml b/src/error_format.ml
index 3e91f065..9e125efa 100644
--- a/src/error_format.ml
+++ b/src/error_format.ml
@@ -46,6 +46,28 @@ let format_code_single' fname in_chan lnum cnum_from cnum_to contents ppf =
   format_endline (blank_prefix ^ underline_single ppf.loc_color cnum_from cnum_to) ppf;
   contents { ppf with indent = blank_prefix ^ " " }
 
+let underline_double_from color cnum_from eol =
+  Util.(String.make cnum_from ' ' ^ clear (color ("^" ^ String.make (eol - cnum_from - 1) '-')))
+
+let underline_double_to color cnum_to =
+  Util.(clear (color (String.make (cnum_to - 1) '-' ^ "^")))
+
+let format_code_double' fname in_chan lnum_from cnum_from lnum_to cnum_to contents ppf =
+  skip_lines in_chan (lnum_from - 1);
+  let line_from = input_line in_chan in
+  skip_lines in_chan (lnum_to - lnum_from - 1);
+  let line_to = input_line in_chan in
+  let line_to_prefix = string_of_int lnum_to ^ Util.(clear (cyan " |")) in
+  let line_from_padding = String.make (String.length (string_of_int lnum_to) - String.length (string_of_int lnum_from)) ' ' in
+  let line_from_prefix = string_of_int lnum_from ^ line_from_padding ^ Util.(clear (cyan " |")) in
+  let blank_prefix = String.make (String.length (string_of_int lnum_to)) ' ' ^ Util.(clear (ppf.loc_color " |")) in
+  format_endline (Printf.sprintf "[%s]:%d:%d-%d:%d" Util.(fname |> cyan |> clear) lnum_from cnum_from lnum_to cnum_to) ppf;
+  format_endline (line_from_prefix ^ line_from) ppf;
+  format_endline (blank_prefix ^ underline_double_from ppf.loc_color cnum_from (String.length line_from)) ppf;
+  format_endline (line_to_prefix ^ line_to) ppf;
+  format_endline (blank_prefix ^ underline_double_to ppf.loc_color cnum_to) ppf;
+  contents { ppf with indent = blank_prefix ^ " " }
+
 let format_code_single fname lnum cnum_from cnum_to contents ppf =
   try
     let in_chan = open_in fname in
@@ -57,17 +79,31 @@ let format_code_single fname lnum cnum_from cnum_to contents ppf =
   with
   | _ -> ()
 
+let format_code_double fname lnum_from cnum_from lnum_to cnum_to contents ppf =
+  try
+    let in_chan = open_in fname in
+    begin
+      try format_code_double' fname in_chan lnum_from cnum_from lnum_to cnum_to contents ppf
+      with
+      | _ -> close_in_noerr in_chan; ()
+    end
+  with
+  | _ -> ()
+
 let format_pos p1 p2 contents ppf =
   let open Lexing in
   if p1.pos_lnum == p2.pos_lnum
   then format_code_single p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) (p2.pos_cnum - p2.pos_bol) contents ppf
-  else failwith "Range"
+  else format_code_double p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol) contents ppf
 
-let format_loc l contents =
+let rec format_loc l contents =
   match l with
-  | Parse_ast.Unknown -> failwith "No location"
+  | Parse_ast.Unknown -> contents
   | Parse_ast.Range (p1, p2) -> format_pos p1 p2 contents
-  | _ -> failwith "not range"
+  | Parse_ast.Unique (_, l) -> format_loc l contents
+  | Parse_ast.Documented (_, l) -> format_loc l contents
+  | Parse_ast.Generated l ->
+     fun ppf -> (format_endline "Code generated nearby:" ppf; format_loc l contents ppf)
 
 type message =
   | Location of Parse_ast.l * message
diff --git a/src/reporting.ml b/src/reporting.ml
index f27e4c03..7aa68296 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -95,159 +95,26 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-let rec skip_lines in_chan = function
-  | n when n <= 0 -> ()
-  | n -> ignore (input_line in_chan); skip_lines in_chan (n - 1)
-
-let rec read_lines in_chan = function
-  | n when n <= 0 -> []
-  | n ->
-     let l = input_line in_chan in
-     let ls = read_lines in_chan (n - 1) in
-     l :: ls
-
-let termcode n = "\x1B[" ^ string_of_int n ^ "m"
-
-let print_code1 ff fname lnum1 cnum1 cnum2 =
-  try
-    let in_chan = open_in fname in
-    begin
-      try
-        skip_lines in_chan (lnum1 - 1);
-        let line = input_line in_chan in
-        Format.fprintf ff "%s%s%s"
-                       (Str.string_before line cnum1)
-                       Util.(Str.string_before (Str.string_after line cnum1) (cnum2 - cnum1) |> red_bg |> clear)
-                       (Str.string_after line cnum2);
-        close_in in_chan
-      with e -> (close_in_noerr in_chan;
-                 prerr_endline (Printf.sprintf "print_code1: %s %d %d %d %s" fname lnum1 cnum1 cnum2 (Printexc.to_string e)))
-    end
-  with _ -> ()
-
-let format_pos ff p =
-  let open Lexing in
-  begin
-    Format.fprintf ff "file \"%s\", line %d, character %d:\n\n"
-                   p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol);
-    print_code1 ff p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) (p.pos_cnum - p.pos_bol + 1);
-    Format.fprintf ff "\n\n";
-    Format.pp_print_flush ff ()
-  end
-
-let print_code2 ff fname lnum1 cnum1 lnum2 cnum2 =
-  try
-    let in_chan = open_in fname in
-    begin
-      try
-        skip_lines in_chan (lnum1 - 1);
-        let line = input_line in_chan in
-        Format.fprintf ff "%s%s\n"
-                       (Str.string_before line cnum1)
-                       Util.(Str.string_after line cnum1 |> red_bg |> clear);
-        let lines = read_lines in_chan (lnum2 - lnum1 - 1) in
-        List.iter (fun l -> Format.fprintf ff "%s\n" Util.(l |> red_bg |> clear)) lines;
-        let line = input_line in_chan in
-        Format.fprintf ff "%s%s"
-                       Util.(Str.string_before line cnum2 |> red_bg |> clear)
-                       (Str.string_after line cnum2);
-        close_in in_chan
-      with e -> (close_in_noerr in_chan; prerr_endline (Printexc.to_string e))
-    end
-  with _ -> ()
-
-let format_pos2 ff p1 p2 =
-  let open Lexing in
-  begin
-    Format.fprintf ff "file \"%s\", line %d, character %d to line %d, character %d\n\n"
-                   p1.pos_fname
-                   p1.pos_lnum (p1.pos_cnum - p1.pos_bol + 1)
-                   p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
-    if p1.pos_lnum == p2.pos_lnum
-    then print_code1 ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) (p2.pos_cnum - p2.pos_bol)
-    else print_code2 ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
-    Format.pp_print_flush ff ()
-  end
-
-let format_just_pos ff p1 p2 =
-  let open Lexing in
-  Format.fprintf ff "file \"%s\", line %d, character %d to line %d, character %d"
-                 p1.pos_fname
-                 p1.pos_lnum (p1.pos_cnum - p1.pos_bol + 1)
-                 p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
-  Format.pp_print_flush ff ()
-
-(* reads the part between p1 and p2 from the file *)
-
-let read_from_file_pos2 p1 p2 =
-  let (s, e, multi) = if p1.Lexing.pos_lnum = p2.Lexing.pos_lnum then
-                  (* everything in the same line, so really only read this small part*)
-                  (p1.Lexing.pos_cnum, p2.Lexing.pos_cnum, None) 
-               else (*multiline, so start reading at beginning of line *)
-                  (p1.Lexing.pos_bol, p2.Lexing.pos_cnum, Some (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) in
-
-  let ic = open_in p1.Lexing.pos_fname in
-  let _ = seek_in ic s in
-  let l = (e - s) in
-  let buf = Bytes.create l in
-  let _ = input ic buf 0 l in
-  let _ = match multi with None -> () | Some sk -> Bytes.fill buf 0 sk ' ' in
-  let _ = close_in ic in
-  (buf, not (multi = None))
-
-let rec format_loc_aux ?code:(code=true) ff = function
-  | Parse_ast.Unknown ->
-     Format.fprintf ff "no location information available"
-  | Parse_ast.Generated l ->
-     Format.fprintf ff "code generated: original nearby source is ";
-     format_loc_aux ~code:code ff l
-  | Parse_ast.Unique (n, l) ->
-     Format.fprintf ff "code unique (%d): original nearby source is " n;
-     format_loc_aux ~code:code ff l
-  | Parse_ast.Range (p1, p2) when code ->
-     format_pos2 ff p1 p2
-  | Parse_ast.Range (p1, p2) ->
-     format_just_pos ff p1 p2
-  | Parse_ast.Documented (_, l) ->
-     format_loc_aux ~code:code ff l
-
-let format_loc_source ff = function
-  | Parse_ast.Range (p1, p2) ->
-     let (s, multi_line) = read_from_file_pos2 p1 p2 in
-     if multi_line then
-       Format.fprintf ff "  original input:\n%s\n" (Bytes.to_string s)
-     else
-       Format.fprintf ff "  original input: \"%s\"\n" (Bytes.to_string s)
-  | _ -> ()
-
-let format_loc ff l =
- (format_loc_aux ff l;
-  Format.pp_print_newline ff ();
-  Format.pp_print_flush ff ()
-);;
-
-let print_err_loc l = 
-   (format_loc Format.err_formatter l)
-
-let print_pos p = format_pos Format.std_formatter p
-let print_err_pos p = format_pos Format.err_formatter p
-
-let loc_to_string ?code:(code=true) l =
-  let _ = Format.flush_str_formatter () in
-  let _ = format_loc_aux ~code:code Format.str_formatter l in
-  let s = Format.flush_str_formatter () in
-  s
-
 type pos_or_loc = Loc of Parse_ast.l | Pos of Lexing.position
 
 let print_err_internal fatal verb_loc p_l m1 m2 =
   let open Error_format in
+  prerr_endline (m1 ^ ":");
   begin match p_l with
   | Loc l -> format_message (Location (l, Line m2)) err_formatter
-  | _ -> failwith "Pos"
+  | Pos p -> format_message (Location (Parse_ast.Range (p, p), Line m2)) err_formatter
   end;
   if fatal then exit 1 else ()
 
+let loc_to_string ?code:(code=true) l =
+  let open Error_format in
+  if code then
+    let b = Buffer.create 160 in
+    format_message (Location (l, Line "")) (buffer_formatter b);
+    Buffer.contents b
+  else
+    "LOC"
+
 let print_err fatal verb_loc l m1 m2 =
   print_err_internal fatal verb_loc (Loc l) m1 m2
 
diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect
index 34fdea2b..b1597759 100644
--- a/test/typecheck/pass/bool_constraint/v1.expect
+++ b/test/typecheck/pass/bool_constraint/v1.expect
@@ -1 +1,20 @@
-Fatal error: exception Failure("No location")
+Type error:
+[bool_constraint/v1.sail]:12:19-20
+12 |  if b then n else 4
+   |                   ^
+   | Tried performing type coercion from int(4) to {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} on 4
+   | Coercion failed because:
+   | int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)}
+   | [bool_constraint/v1.sail]:11:0-13:1
+   | 11 |function foo(b, n) = {
+   |    |^---------------------
+   | 13 |}
+   |    |^
+   |    | 'b bound here
+   | [bool_constraint/v1.sail]:11:0-13:1
+   | 11 |function foo(b, n) = {
+   |    |^---------------------
+   | 13 |}
+   |    |^
+   |    | 'n bound here
+   | 
diff --git a/test/typecheck/pass/bool_constraint/v2.expect b/test/typecheck/pass/bool_constraint/v2.expect
index 989226fb..c7a355e1 100644
--- a/test/typecheck/pass/bool_constraint/v2.expect
+++ b/test/typecheck/pass/bool_constraint/v2.expect
@@ -1,3 +1,4 @@
+Type error:
 [bool_constraint/v2.sail]:38:4-32
 38 |    _prove(constraint('n <= 14))
    |    ^--------------------------^
diff --git a/test/typecheck/pass/bool_constraint/v3.expect b/test/typecheck/pass/bool_constraint/v3.expect
index 51692dd7..63791a70 100644
--- a/test/typecheck/pass/bool_constraint/v3.expect
+++ b/test/typecheck/pass/bool_constraint/v3.expect
@@ -1,3 +1,4 @@
+Type error:
 [bool_constraint/v3.sail]:46:4-32
 46 |    _prove(constraint('n <= 14))
    |    ^--------------------------^
diff --git a/test/typecheck/pass/bool_constraint/v4.expect b/test/typecheck/pass/bool_constraint/v4.expect
index df65fc8a..420909bf 100644
--- a/test/typecheck/pass/bool_constraint/v4.expect
+++ b/test/typecheck/pass/bool_constraint/v4.expect
@@ -1,3 +1,4 @@
+Type error:
 [bool_constraint/v4.sail]:46:4-32
 46 |    _prove(constraint('n <= 13))
    |    ^--------------------------^
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
index f3771c9d..8c95193d 100644
--- a/test/typecheck/pass/constrained_struct/v1.expect
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -1,3 +1,4 @@
+Type error:
 [constrained_struct/v1.sail]:10:18-26
 10 |type MyStruct64 = MyStruct(65)
    |                  ^------^
diff --git a/test/typecheck/pass/constraint_ctor/v1.expect b/test/typecheck/pass/constraint_ctor/v1.expect
index b2c62a8c..cf3b9399 100644
--- a/test/typecheck/pass/constraint_ctor/v1.expect
+++ b/test/typecheck/pass/constraint_ctor/v1.expect
@@ -1,3 +1,4 @@
+Type error:
 [constraint_ctor/v1.sail]:10:2-29
 10 |  _prove(constraint('x >= 4));
    |  ^-------------------------^
diff --git a/test/typecheck/pass/constraint_ctor/v2.expect b/test/typecheck/pass/constraint_ctor/v2.expect
index a6774adc..0e56f0a4 100644
--- a/test/typecheck/pass/constraint_ctor/v2.expect
+++ b/test/typecheck/pass/constraint_ctor/v2.expect
@@ -1,3 +1,4 @@
+Type error:
 [constraint_ctor/v2.sail]:18:2-30
 18 |  _prove(constraint('x >= 24));
    |  ^--------------------------^
diff --git a/test/typecheck/pass/constraint_ctor/v3.expect b/test/typecheck/pass/constraint_ctor/v3.expect
index bd93a7e1..37d1dff2 100644
--- a/test/typecheck/pass/constraint_ctor/v3.expect
+++ b/test/typecheck/pass/constraint_ctor/v3.expect
@@ -1,3 +1,4 @@
+Type error:
 [constraint_ctor/v3.sail]:18:2-30
 18 |  _prove(constraint('x >= 23));
    |  ^--------------------------^
diff --git a/test/typecheck/pass/constraint_ctor/v4.expect b/test/typecheck/pass/constraint_ctor/v4.expect
index 942db0a4..64893e4d 100644
--- a/test/typecheck/pass/constraint_ctor/v4.expect
+++ b/test/typecheck/pass/constraint_ctor/v4.expect
@@ -1,3 +1,4 @@
+Type error:
 [constraint_ctor/v4.sail]:17:33-36
 17 |function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
    |                                 ^-^
diff --git a/test/typecheck/pass/constraint_ctor/v5.expect b/test/typecheck/pass/constraint_ctor/v5.expect
index 93fb2a43..fc2ef615 100644
--- a/test/typecheck/pass/constraint_ctor/v5.expect
+++ b/test/typecheck/pass/constraint_ctor/v5.expect
@@ -1,3 +1,4 @@
+Type error:
 [constraint_ctor/v5.sail]:27:2-29
 27 |  _prove(constraint('x >= 4));
    |  ^-------------------------^
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index 651dda4c..cc8b874f 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -1,3 +1,4 @@
+Type error:
 [exist_synonym/v1.sail]:6:41-42
 6 |let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
   |                                         ^
diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect
index d5617688..c01d8359 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -1,3 +1,4 @@
+Type error:
 [exist_synonym/v2.sail]:6:40-41
 6 |let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
   |                                        ^
diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
index 34fdea2b..c237ae2d 100644
--- a/test/typecheck/pass/exist_synonym/v3.expect
+++ b/test/typecheck/pass/exist_synonym/v3.expect
@@ -1 +1,3 @@
-Fatal error: exception Failure("No location")
+Type error:
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)
+
diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect
index 34fdea2b..1cbc3df8 100644
--- a/test/typecheck/pass/exist_synonym/v4.expect
+++ b/test/typecheck/pass/exist_synonym/v4.expect
@@ -1 +1,3 @@
-Fatal error: exception Failure("No location")
+Type error:
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 2 & 2 <= 4), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)
+
diff --git a/test/typecheck/pass/function_namespace/v1.expect b/test/typecheck/pass/function_namespace/v1.expect
index 15ab6962..2bb734aa 100644
--- a/test/typecheck/pass/function_namespace/v1.expect
+++ b/test/typecheck/pass/function_namespace/v1.expect
@@ -1,3 +1,4 @@
+Type error:
 [function_namespace/v1.sail]:9:6-10
 9 |  let test = true;
   |      ^--^
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index 22a3756d..ac4428c6 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -1,3 +1,4 @@
+Type error:
 [global_type_var/v1.sail]:23:13-15
 23 |let _ = test(32)
    |             ^^
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index 360a6e48..93eb628b 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -1,3 +1,4 @@
+Type error:
 [global_type_var/v2.sail]:23:13-15
 23 |let _ = test(64)
    |             ^^
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index 8e687370..6def5172 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -1,3 +1,4 @@
+Type error:
 [global_type_var/v3.sail]:15:23-27
 15 |    let y : atom(64) = size in
    |                       ^--^
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index e9db69f5..c8217478 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -1,3 +1,4 @@
+Type error:
 [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 06800859..f0c2fab3 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -1,3 +1,4 @@
+Type error:
 [if_infer/v2.sail]:10:10-38
 10 |  let _ = 0b1001[if R then 0 else f()];
    |          ^--------------------------^
diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect
index b701032d..7e0e74bb 100644
--- a/test/typecheck/pass/if_infer/v3.expect
+++ b/test/typecheck/pass/if_infer/v3.expect
@@ -1,3 +1,4 @@
+Type error:
 [if_infer/v3.sail]:10:10-38
 10 |  let _ = 0b1001[if R then 0 else f()];
    |          ^--------------------------^
diff --git a/test/typecheck/pass/not_pattern/v1.expect b/test/typecheck/pass/not_pattern/v1.expect
index 2b766c43..aeefb901 100644
--- a/test/typecheck/pass/not_pattern/v1.expect
+++ b/test/typecheck/pass/not_pattern/v1.expect
@@ -1,3 +1,4 @@
+Type error:
 [not_pattern/v1.sail]:12:6-7
 12 |    ~(y) => (),
    |      ^
diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect
index 096b09a7..ce61cf2a 100644
--- a/test/typecheck/pass/vec_length/v1.expect
+++ b/test/typecheck/pass/vec_length/v1.expect
@@ -1,3 +1,4 @@
+Type error:
 [vec_length/v1.sail]:6:10-15
 6 |  let y = x[10];
   |          ^---^
diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect
index c42b12ad..3d40cdb0 100644
--- a/test/typecheck/pass/vec_length/v1_inc.expect
+++ b/test/typecheck/pass/vec_length/v1_inc.expect
@@ -1,3 +1,4 @@
+Type error:
 [vec_length/v1_inc.sail]:6:10-15
 6 |  let y = x[10];
   |          ^---^
diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect
index 7b0e6634..c77ecaa7 100644
--- a/test/typecheck/pass/vec_length/v2.expect
+++ b/test/typecheck/pass/vec_length/v2.expect
@@ -1,3 +1,4 @@
+Type error:
 [vec_length/v2.sail]:7:10-25
 7 |  let z = [x with 10 = y];
   |          ^-------------^
diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect
index f7ef04e4..cff65f62 100644
--- a/test/typecheck/pass/vec_length/v2_inc.expect
+++ b/test/typecheck/pass/vec_length/v2_inc.expect
@@ -1,3 +1,4 @@
+Type error:
 [vec_length/v2_inc.sail]:7:10-25
 7 |  let z = [x with 10 = y];
   |          ^-------------^
diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect
new file mode 100644
index 00000000..e3afecee
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v3.expect
@@ -0,0 +1,14 @@
+Type error:
+[vec_length/v3.sail]:6:10-12:3
+6  |  let y = x[
+   |          ^-
+12 |  ];
+   |--^
+   | No overloading for vector_access, tried:
+   | * bitvector_access
+   |    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)
+   | 
diff --git a/test/typecheck/pass/vec_length/v3.sail b/test/typecheck/pass/vec_length/v3.sail
new file mode 100644
index 00000000..8736278e
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v3.sail
@@ -0,0 +1,14 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[
+
+
+
+
+    10
+  ];
+  ()
+}