More error messages improvments

28 files changed, 77 insertions, 3 deletions

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
+  ];
+  ()
+}