Some work on improving error messages

We now store the location where type variables were bound, so we can
use this information when printing error messages.

Factor type errors out into type_error.ml. This means that
Type_check.check is now Type_error.check, as it previously it handled
wrapping the type_errors into reporting_basic
errors. Type_check.check' has therefore been renamed to
Type_check.check.

4 files changed, 44 insertions, 10 deletions

diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index c2f05f5c..9ee4b202 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -2,5 +2,6 @@ Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, char
 
 let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
 
-Tried performing type coercion on 4
-Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 'n & 'n <= 33)
+Tried performing type coercion from atom(4) to {'n, 0 <= 'n & 'n <= 33. regno('n)} on 4
+Failed because
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('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 5926bcdb..e3414034 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -2,5 +2,6 @@ Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, char
 
 let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
 
-Tried performing type coercion on 4
-Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom('n) with (0 <= 'n & 'n <= 8)
+Tried performing type coercion from atom(4) to {'n, 0 <= 'n & 'n <= 8. regno('n)} on 4
+Failed because
+Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom('n) with (0 <= 'n & 'n <= 8)
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index ba475840..33d6cbcd 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -2,7 +2,23 @@ Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23,
 
 let _ = test(32)
 
-Tried performing type coercion on 32
+Tried performing type coercion from atom(32) to atom('size) on 32
 Failed because
-  atom(32) is not a subtype of atom('size)
-  in context 'size = 'ex8#, ('ex8# = 32 | 'ex8# = 64), ('ex7# = 32 | 'ex7# = 64)
+atom(32) is not a subtype of atom('size)
+in context
+* 'size = 'ex8#
+* ('ex8# = 32 | 'ex8# = 64)
+* ('ex7# = 32 | 'ex7# = 64)
+where
+* 'ex7# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32
+
+let (size as 'size) : {|32, 64|} = 32
+
+* 'ex8# 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 bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18
+
+let (size as 'size) : {|32, 64|} = 32
+
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index 8d641c4c..25304155 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -2,7 +2,23 @@ Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23,
 
 let _ = test(64)
 
-Tried performing type coercion on 64
+Tried performing type coercion from atom(64) to atom('size) on 64
 Failed because
-  atom(64) is not a subtype of atom('size)
-  in context 'size = 'ex8#, ('ex8# = 32 | 'ex8# = 64), ('ex7# = 32 | 'ex7# = 64)
+atom(64) is not a subtype of atom('size)
+in context
+* 'size = 'ex8#
+* ('ex8# = 32 | 'ex8# = 64)
+* ('ex7# = 32 | 'ex7# = 64)
+where
+* 'ex7# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
+
+let (size as 'size) : {|32, 64|} = 32
+
+* 'ex8# 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 bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18
+
+let (size as 'size) : {|32, 64|} = 32
+