Improve error messages and debugging

Work on improving the formatting and quality of error messages

When sail is invoked with sail -i, any type errors now drop the user
down to the interactive prompt, with the interactive environment being
the environment at the point the type error occurred, this means the
typechecker state can be interactively queried in the interpreter to help
diagnose type errors.

26 files changed, 180 insertions, 276 deletions

diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect
index dc76a65f..34fdea2b 100644
--- a/test/typecheck/pass/bool_constraint/v1.expect
+++ b/test/typecheck/pass/bool_constraint/v1.expect
@@ -1,27 +1 @@
-Type error at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
-
-  if b then n else 4
-
-Tried performing type coercion from int(4) to {'m, ('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)}
-  in context
-  * 4 == 'ex39#
-  * not('b)
-  where
-  * 'b bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1
-
-function foo(b, n) = {
-  if b then n else 4
-}
-
-  * 'ex39# bound at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
-
-  if b then n else 4
-
-  * 'n bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1
-
-function foo(b, n) = {
-  if b then n else 4
-}
-
+Fatal error: exception Failure("No location")
diff --git a/test/typecheck/pass/bool_constraint/v2.expect b/test/typecheck/pass/bool_constraint/v2.expect
index 847ef329..989226fb 100644
--- a/test/typecheck/pass/bool_constraint/v2.expect
+++ b/test/typecheck/pass/bool_constraint/v2.expect
@@ -1,5 +1,5 @@
-Type error at file "bool_constraint/v2.sail", line 38, character 5 to line 38, character 32
-
-    _prove(constraint('n <= 14))
-
-Cannot prove 'n <= 14
+[bool_constraint/v2.sail]:38:4-32
+38 |    _prove(constraint('n <= 14))
+   |    ^--------------------------^
+   | Cannot prove 'n <= 14
+   | 
diff --git a/test/typecheck/pass/bool_constraint/v3.expect b/test/typecheck/pass/bool_constraint/v3.expect
index ca87fac1..51692dd7 100644
--- a/test/typecheck/pass/bool_constraint/v3.expect
+++ b/test/typecheck/pass/bool_constraint/v3.expect
@@ -1,5 +1,5 @@
-Type error at file "bool_constraint/v3.sail", line 46, character 5 to line 46, character 32
-
-    _prove(constraint('n <= 14))
-
-Cannot prove 'n <= 14
+[bool_constraint/v3.sail]:46:4-32
+46 |    _prove(constraint('n <= 14))
+   |    ^--------------------------^
+   | Cannot prove 'n <= 14
+   | 
diff --git a/test/typecheck/pass/bool_constraint/v4.expect b/test/typecheck/pass/bool_constraint/v4.expect
index 07363175..df65fc8a 100644
--- a/test/typecheck/pass/bool_constraint/v4.expect
+++ b/test/typecheck/pass/bool_constraint/v4.expect
@@ -1,5 +1,5 @@
-Type error at file "bool_constraint/v4.sail", line 46, character 5 to line 46, character 32
-
-    _prove(constraint('n <= 13))
-
-Cannot prove 'n <= 13
+[bool_constraint/v4.sail]:46:4-32
+46 |    _prove(constraint('n <= 13))
+   |    ^--------------------------^
+   | Cannot prove 'n <= 13
+   | 
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
index ab25cbc4..f3771c9d 100644
--- a/test/typecheck/pass/constrained_struct/v1.expect
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -1,5 +1,5 @@
-Type error at file "constrained_struct/v1.sail", line 10, character 19 to line 10, character 26
-
-type MyStruct64 = MyStruct(65)
-
-Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct
+[constrained_struct/v1.sail]:10:18-26
+10 |type MyStruct64 = MyStruct(65)
+   |                  ^------^
+   | Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct
+   | 
diff --git a/test/typecheck/pass/constraint_ctor/v1.expect b/test/typecheck/pass/constraint_ctor/v1.expect
index c3886af8..b2c62a8c 100644
--- a/test/typecheck/pass/constraint_ctor/v1.expect
+++ b/test/typecheck/pass/constraint_ctor/v1.expect
@@ -1,5 +1,5 @@
-Type error at file "constraint_ctor/v1.sail", line 10, character 3 to line 10, character 29
-
-  _prove(constraint('x >= 4));
-
-Cannot prove 'x >= 4
+[constraint_ctor/v1.sail]:10:2-29
+10 |  _prove(constraint('x >= 4));
+   |  ^-------------------------^
+   | Cannot prove 'x >= 4
+   | 
diff --git a/test/typecheck/pass/constraint_ctor/v2.expect b/test/typecheck/pass/constraint_ctor/v2.expect
index a315b3b7..a6774adc 100644
--- a/test/typecheck/pass/constraint_ctor/v2.expect
+++ b/test/typecheck/pass/constraint_ctor/v2.expect
@@ -1,5 +1,5 @@
-Type error at file "constraint_ctor/v2.sail", line 18, character 3 to line 18, character 30
-
-  _prove(constraint('x >= 24));
-
-Cannot prove 'x >= 24
+[constraint_ctor/v2.sail]:18:2-30
+18 |  _prove(constraint('x >= 24));
+   |  ^--------------------------^
+   | Cannot prove 'x >= 24
+   | 
diff --git a/test/typecheck/pass/constraint_ctor/v3.expect b/test/typecheck/pass/constraint_ctor/v3.expect
index e0edd01a..bd93a7e1 100644
--- a/test/typecheck/pass/constraint_ctor/v3.expect
+++ b/test/typecheck/pass/constraint_ctor/v3.expect
@@ -1,5 +1,5 @@
-Type error at file "constraint_ctor/v3.sail", line 18, character 3 to line 18, character 30
-
-  _prove(constraint('x >= 23));
-
-Cannot prove 'x >= 23
+[constraint_ctor/v3.sail]:18:2-30
+18 |  _prove(constraint('x >= 23));
+   |  ^--------------------------^
+   | Cannot prove 'x >= 23
+   | 
diff --git a/test/typecheck/pass/constraint_ctor/v4.expect b/test/typecheck/pass/constraint_ctor/v4.expect
index 06eb9d22..942db0a4 100644
--- a/test/typecheck/pass/constraint_ctor/v4.expect
+++ b/test/typecheck/pass/constraint_ctor/v4.expect
@@ -1,5 +1,5 @@
-Type error at file "constraint_ctor/v4.sail", line 17, character 34 to line 17, character 36
-
-function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
-
-Could not prove 23 <= 22 for type constructor Bar
+[constraint_ctor/v4.sail]:17:33-36
+17 |function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+   |                                 ^-^
+   | Could not prove 23 <= 22 for type constructor Bar
+   | 
diff --git a/test/typecheck/pass/constraint_ctor/v5.expect b/test/typecheck/pass/constraint_ctor/v5.expect
index b6df0222..93fb2a43 100644
--- a/test/typecheck/pass/constraint_ctor/v5.expect
+++ b/test/typecheck/pass/constraint_ctor/v5.expect
@@ -1,5 +1,5 @@
-Type error at file "constraint_ctor/v5.sail", line 27, character 3 to line 27, character 29
-
-  _prove(constraint('x >= 4));
-
-Cannot prove 'x >= 4
+[constraint_ctor/v5.sail]:27:2-29
+27 |  _prove(constraint('x >= 4));
+   |  ^-------------------------^
+   | Cannot prove 'x >= 4
+   | 
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index fb1b2619..651dda4c 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -1,6 +1,7 @@
-Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, character 42
-
-let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
-
-Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 33). regno('n)} on 4
-Coercion failed because: Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)
+[exist_synonym/v1.sail]:6:41-42
+6 |let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
+  |                                         ^
+  | Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 33). regno('n)} on 4
+  | Coercion failed because:
+  | Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)
+  | 
diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect
index 5bde04ba..d5617688 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -1,6 +1,7 @@
-Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, character 41
-
-let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
-
-Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 8). regno('n)} on 4
-Coercion failed because: Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)
+[exist_synonym/v2.sail]:6:40-41
+6 |let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
+  |                                        ^
+  | Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 8). regno('n)} on 4
+  | Coercion failed because:
+  | Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)
+  | 
diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
index 154ddc52..34fdea2b 100644
--- a/test/typecheck/pass/exist_synonym/v3.expect
+++ b/test/typecheck/pass/exist_synonym/v3.expect
@@ -1,3 +1 @@
-Type error at no location information available
-
-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)
+Fatal error: exception Failure("No location")
diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect
index 86d6f93b..34fdea2b 100644
--- a/test/typecheck/pass/exist_synonym/v4.expect
+++ b/test/typecheck/pass/exist_synonym/v4.expect
@@ -1,3 +1 @@
-Type error at no location information available
-
-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)
+Fatal error: exception Failure("No location")
diff --git a/test/typecheck/pass/function_namespace/v1.expect b/test/typecheck/pass/function_namespace/v1.expect
index 6e40adc0..15ab6962 100644
--- a/test/typecheck/pass/function_namespace/v1.expect
+++ b/test/typecheck/pass/function_namespace/v1.expect
@@ -1,5 +1,5 @@
-Type error at file "function_namespace/v1.sail", line 9, character 7 to line 9, character 10
-
-  let test = true;
-
-Local variable test is already bound as a function name
+[function_namespace/v1.sail]:9:6-10
+9 |  let test = true;
+  |      ^--^
+  | Local variable test is already bound as a function name
+  | 
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index 7b87ec21..22a3756d 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -1,24 +1,11 @@
-Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23, character 15
-
-let _ = test(32)
-
-Tried performing type coercion from int(32) to int('size) on 32
-Coercion failed because:
-  int(32) is not a subtype of int('size)
-  in context
-  * 'size == '_size
-  * ('_size == 32 | '_size == 64)
-  * ('_size#0 == 32 | '_size#0 == 64)
-  where
-  * '_size bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
-
-let (size as 'size) : {|32, 64|} = 32
-
-  * '_size#0 bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32
-
-let (size as 'size) : {|32, 64|} = 32
-
-  * 'size bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18
-
-let (size as 'size) : {|32, 64|} = 32
-
+[global_type_var/v1.sail]:23:13-15
+23 |let _ = test(32)
+   |             ^^
+   | Tried performing type coercion from int(32) to int('size) on 32
+   | Coercion failed because:
+   | int(32) is not a subtype of int('size)
+   | [global_type_var/v1.sail]:5:13-18
+   | 5 |let (size as 'size) : {|32, 64|} = 32
+   |   |             ^---^
+   |   | 'size bound here
+   | 
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index 9b09a3f6..360a6e48 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -1,24 +1,11 @@
-Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23, character 15
-
-let _ = test(64)
-
-Tried performing type coercion from int(64) to int('size) on 64
-Coercion failed because:
-  int(64) is not a subtype of int('size)
-  in context
-  * 'size == '_size
-  * ('_size == 32 | '_size == 64)
-  * ('_size#0 == 32 | '_size#0 == 64)
-  where
-  * '_size bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
-
-let (size as 'size) : {|32, 64|} = 32
-
-  * '_size#0 bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
-
-let (size as 'size) : {|32, 64|} = 32
-
-  * 'size bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18
-
-let (size as 'size) : {|32, 64|} = 32
-
+[global_type_var/v2.sail]:23:13-15
+23 |let _ = test(64)
+   |             ^^
+   | Tried performing type coercion from int(64) to int('size) on 64
+   | Coercion failed because:
+   | int(64) is not a subtype of int('size)
+   | [global_type_var/v2.sail]:5:13-18
+   | 5 |let (size as 'size) : {|32, 64|} = 32
+   |   |             ^---^
+   |   | 'size bound here
+   | 
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index f5f5990a..8e687370 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -1,35 +1,11 @@
-Type error at file "global_type_var/v3.sail", line 15, character 24 to line 15, character 27
-
-    let y : atom(64) = size in
-
-Tried performing type coercion from int('_size) to int(64) on size
-Coercion failed because:
-  int('_size) is not a subtype of int(64)
-  in context
-  * not('fv10#size == 32)
-  * 'size == '_size
-  * ('_size == 32 | '_size == 64)
-  * ('_size#0 == 32 | '_size#0 == 64)
-  where
-  * '_size bound at file "global_type_var/v3.sail", line 5, character 6 to line 5, character 18
-
-let (size as 'size) : {|32, 64|} = 32
-
-  * '_size#0 bound at file "global_type_var/v3.sail", line 5, character 5 to line 5, character 32
-
-let (size as 'size) : {|32, 64|} = 32
-
-  * 'fv10#size bound at file "global_type_var/v3.sail", line 11, character 1 to line 17, character 3
-
-function test x =
-  if x == 32 then {
-    ()
-  } else {
-    let y : atom(64) = size in
-    ()
-  }
-
-  * 'size bound at file "global_type_var/v3.sail", line 5, character 14 to line 5, character 18
-
-let (size as 'size) : {|32, 64|} = 32
-
+[global_type_var/v3.sail]:15:23-27
+15 |    let y : atom(64) = size in
+   |                       ^--^
+   | Tried performing type coercion from int('_size) to int(64) on size
+   | Coercion failed because:
+   | int('_size) is not a subtype of int(64)
+   | [global_type_var/v3.sail]:5:5-18
+   | 5 |let (size as 'size) : {|32, 64|} = 32
+   |   |     ^-----------^
+   |   | '_size bound here
+   | 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index c29e4f26..e9db69f5 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -1,17 +1,11 @@
-Type error at file "if_infer/v1.sail", line 10, character 11 to line 10, character 37
-
-  let _ = 0b100[if R then 0 else f()];
-
-No overloadings for vector_access, tried:
-  bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 'ex40# & ('ex40# + 1) <= 3)
-    
-    Try adding named type variables for 
-    
-    
-  plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 'ex43# & ('ex43# + 1) <= 3)
-    
-    Try adding named type variables for 
-    
-    
+[if_infer/v1.sail]:10:10-37
+10 |  let _ = 0b100[if R then 0 else f()];
+   |          ^-------------------------^
+   | No overloading for vector_access, tried:
+   | * bitvector_access
+   |    Could not resolve quantifiers for bitvector_access
+   |    * (0 <= 'ex40# & ('ex40# + 1) <= 3)
+   | * plain_vector_access
+   |    Could not resolve quantifiers for plain_vector_access
+   |    * (0 <= 'ex43# & ('ex43# + 1) <= 3)
+   | 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index 3ea57413..06800859 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -1,17 +1,11 @@
-Type error at file "if_infer/v2.sail", line 10, character 11 to line 10, character 38
-
-  let _ = 0b1001[if R then 0 else f()];
-
-No overloadings for vector_access, tried:
-  bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 'ex40# & ('ex40# + 1) <= 4)
-    
-    Try adding named type variables for 
-    
-    
-  plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 'ex43# & ('ex43# + 1) <= 4)
-    
-    Try adding named type variables for 
-    
-    
+[if_infer/v2.sail]:10:10-38
+10 |  let _ = 0b1001[if R then 0 else f()];
+   |          ^--------------------------^
+   | No overloading for vector_access, tried:
+   | * bitvector_access
+   |    Could not resolve quantifiers for bitvector_access
+   |    * (0 <= 'ex40# & ('ex40# + 1) <= 4)
+   | * plain_vector_access
+   |    Could not resolve quantifiers for plain_vector_access
+   |    * (0 <= 'ex43# & ('ex43# + 1) <= 4)
+   | 
diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect
index 8b149bc8..b701032d 100644
--- a/test/typecheck/pass/if_infer/v3.expect
+++ b/test/typecheck/pass/if_infer/v3.expect
@@ -1,7 +1,9 @@
-Type error at file "if_infer/v3.sail", line 10, character 11 to line 10, character 38
-
-  let _ = 0b1001[if R then 0 else f()];
-
-No overloadings for vector_access, tried:
-  bitvector_access: Numeric type is non-simple
-  plain_vector_access: Numeric type is non-simple
+[if_infer/v3.sail]:10:10-38
+10 |  let _ = 0b1001[if R then 0 else f()];
+   |          ^--------------------------^
+   | No overloading for vector_access, tried:
+   | * bitvector_access
+   |    Numeric type is non-simple
+   | * plain_vector_access
+   |    Numeric type is non-simple
+   | 
diff --git a/test/typecheck/pass/not_pattern/v1.expect b/test/typecheck/pass/not_pattern/v1.expect
index 9de82d1f..2b766c43 100644
--- a/test/typecheck/pass/not_pattern/v1.expect
+++ b/test/typecheck/pass/not_pattern/v1.expect
@@ -1,5 +1,5 @@
-Type error at file "not_pattern/v1.sail", line 12, character 7 to line 12, character 7
-
-    ~(y) => (),
-
-Bindings are not allowed in this context
+[not_pattern/v1.sail]:12:6-7
+12 |    ~(y) => (),
+   |      ^
+   | Bindings are not allowed in this context
+   | 
diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect
index 68a4ca70..096b09a7 100644
--- a/test/typecheck/pass/vec_length/v1.expect
+++ b/test/typecheck/pass/vec_length/v1.expect
@@ -1,13 +1,11 @@
-Type error at file "vec_length/v1.sail", line 6, character 11 to line 6, character 15
-
-  let y = x[10];
-
-No overloadings for vector_access, tried:
-  bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
-  plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+[vec_length/v1.sail]:6:10-15
+6 |  let y = x[10];
+  |          ^---^
+  | 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/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect
index 7ce8fd99..c42b12ad 100644
--- a/test/typecheck/pass/vec_length/v1_inc.expect
+++ b/test/typecheck/pass/vec_length/v1_inc.expect
@@ -1,13 +1,11 @@
-Type error at file "vec_length/v1_inc.sail", line 6, character 11 to line 6, character 15
-
-  let y = x[10];
-
-No overloadings for vector_access, tried:
-  bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
-  plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+[vec_length/v1_inc.sail]:6:10-15
+6 |  let y = x[10];
+  |          ^---^
+  | 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/v2.expect b/test/typecheck/pass/vec_length/v2.expect
index d123cabd..7b0e6634 100644
--- a/test/typecheck/pass/vec_length/v2.expect
+++ b/test/typecheck/pass/vec_length/v2.expect
@@ -1,13 +1,11 @@
-Type error at file "vec_length/v2.sail", line 7, character 11 to line 7, character 25
-
-  let z = [x with 10 = y];
-
-No overloadings for vector_update, tried:
-  bitvector_update:
-    Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
-  plain_vector_update:
-    Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+[vec_length/v2.sail]:7:10-25
+7 |  let z = [x with 10 = y];
+  |          ^-------------^
+  | No overloading for vector_update, tried:
+  | * bitvector_update
+  |    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)
+  | 
diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect
index e7d2b52f..f7ef04e4 100644
--- a/test/typecheck/pass/vec_length/v2_inc.expect
+++ b/test/typecheck/pass/vec_length/v2_inc.expect
@@ -1,13 +1,11 @@
-Type error at file "vec_length/v2_inc.sail", line 7, character 11 to line 7, character 25
-
-  let z = [x with 10 = y];
-
-No overloadings for vector_update, tried:
-  bitvector_update:
-    Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
-  plain_vector_update:
-    Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+[vec_length/v2_inc.sail]:7:10-25
+7 |  let z = [x with 10 = y];
+  |          ^-------------^
+  | No overloading for vector_update, tried:
+  | * bitvector_update
+  |    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)
+  |