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)} = [41m4[0m
 
-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)} = [41m4[0m
 
-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([41m32[0m)
 
-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)
+[1matom(32) is not a subtype of atom('size)[21m
+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 [41m(size as 'size) : {|32, 64|}[0m = 32
+
+* 'ex8# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
+
+let ([41msize as 'size[0m) : {|32, 64|} = 32
+
+* 'size bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18
+
+let (size as [41m'size[0m) : {|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([41m64[0m)
 
-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)
+[1matom(64) is not a subtype of atom('size)[21m
+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 [41m(size as 'size) : {|32, 64|}[0m = 32
+
+* 'ex8# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
+
+let ([41msize as 'size[0m) : {|32, 64|} = 32
+
+* 'size bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18
+
+let (size as [41m'size[0m) : {|32, 64|} = 32
+