9 files changed, 65 insertions, 21 deletions
diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect
index 8b8e6b24..dc76a65f 100644
--- a/test/typecheck/pass/bool_constraint/v1.expect
+++ b/test/typecheck/pass/bool_constraint/v1.expect
@@ -6,7 +6,7 @@ Tried performing type coercion from int(4) to {'m, ('b & 'm == 'n | not('b) & 'm
 Coercion failed because:
   int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)}
   in context
-  * 4 == 'ex37#m
+  * 4 == 'ex39#
   * not('b)
   where
   * 'b bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1
@@ -15,7 +15,7 @@ Coercion failed because:
 [41m  if b then n else 4[0m
 [41m}[0m
 
-  * 'ex37#m bound at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
+  * 'ex39# bound at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
 
   if b then n else [41m4[0m
 
diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
index a647ef00..154ddc52 100644
--- a/test/typecheck/pass/exist_synonym/v3.expect
+++ b/test/typecheck/pass/exist_synonym/v3.expect
@@ -1,3 +1,3 @@
 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 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8)
+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 d8bad777..86d6f93b 100644
--- a/test/typecheck/pass/exist_synonym/v4.expect
+++ b/test/typecheck/pass/exist_synonym/v4.expect
@@ -1,3 +1,3 @@
 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 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8)
+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/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index 986e82c0..7b87ec21 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -6,15 +6,15 @@ 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 == 'ex10#
-  * ('ex10# == 32 | 'ex10# == 64)
-  * ('ex9# == 32 | 'ex9# == 64)
+  * 'size == '_size
+  * ('_size == 32 | '_size == 64)
+  * ('_size#0 == 32 | '_size#0 == 64)
   where
-  * 'ex10# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
+  * '_size 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
 
-  * 'ex9# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32
+  * '_size#0 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
 
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index f081d4af..9b09a3f6 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -6,15 +6,15 @@ 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 == 'ex10#
-  * ('ex10# == 32 | 'ex10# == 64)
-  * ('ex9# == 32 | 'ex9# == 64)
+  * 'size == '_size
+  * ('_size == 32 | '_size == 64)
+  * ('_size#0 == 32 | '_size#0 == 64)
   where
-  * 'ex10# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
+  * '_size 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
 
-  * 'ex9# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
+  * '_size#0 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
 
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index 43096686..f5f5990a 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -1,5 +1,35 @@
-Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, character 23
+Type error at file "global_type_var/v3.sail", line 15, character 24 to line 15, character 27
 
-val test : forall [41m'size[0m. atom('size) -> unit
+    let y : atom(64) = [41msize[0m 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 ([41msize as 'size[0m) : {|32, 64|} = 32
+
+  * '_size#0 bound at file "global_type_var/v3.sail", line 5, character 5 to line 5, character 32
+
+let [41m(size as 'size) : {|32, 64|}[0m = 32
+
+  * 'fv10#size bound at file "global_type_var/v3.sail", line 11, character 1 to line 17, character 3
+
+[41mfunction test x =[0m
+[41m  if x == 32 then {[0m
+[41m    ()[0m
+[41m  } else {[0m
+[41m    let y : atom(64) = size in[0m
+[41m    ()[0m
+[41m  }[0m
+
+  * 'size bound at file "global_type_var/v3.sail", line 5, character 14 to line 5, character 18
+
+let (size as [41m'size[0m) : {|32, 64|} = 32
 
-type variable ('size : Int) is already bound
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index e0ffbbb1..c29e4f26 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -4,13 +4,13 @@ Type error at file "if_infer/v1.sail", line 10, character 11 to line 10, charact
 
 No overloadings for vector_access, tried:
   bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 'ex38#ex37# & ('ex38#ex37# + 1) <= 3)
+    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 <= 'ex41#ex40# & ('ex41#ex40# + 1) <= 3)
+    Could not resolve quantifiers for plain_vector_access (0 <= 'ex43# & ('ex43# + 1) <= 3)
     
     Try adding named type variables for 
     
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index fe377730..3ea57413 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -4,13 +4,13 @@ Type error at file "if_infer/v2.sail", line 10, character 11 to line 10, charact
 
 No overloadings for vector_access, tried:
   bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 'ex38#ex37# & ('ex38#ex37# + 1) <= 4)
+    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 <= 'ex41#ex40# & ('ex41#ex40# + 1) <= 4)
+    Could not resolve quantifiers for plain_vector_access (0 <= 'ex43# & ('ex43# + 1) <= 4)
     
     Try adding named type variables for 
     
diff --git a/test/typecheck/pass/tyvar_shadow.sail b/test/typecheck/pass/tyvar_shadow.sail
new file mode 100644
index 00000000..973aa916
--- /dev/null
+++ b/test/typecheck/pass/tyvar_shadow.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+function main((): unit) -> unit = {
+  let x as int('x) = 3;
+  let x as int('x) = 4;
+  _prove(constraint('x + 'x == 8));
+  _not_prove(constraint('x + 'x == 6 | 'x + 'x == 7));
+
+  let y : {'n, 'n == 3. int('n)} = 3;
+  _prove(constraint('_y == 3))
+}
+