3 files changed, 40 insertions, 0 deletions
diff --git a/test/typecheck/pass/shadow_let.sail b/test/typecheck/pass/shadow_let.sail
new file mode 100644
index 00000000..8a30744c
--- /dev/null
+++ b/test/typecheck/pass/shadow_let.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+register R : int
+
+val foo : int(1) -> unit
+val bar : int(2) -> unit
+
+function main((): unit) -> unit = {
+  let 'x : {'z, 'z == 1. int('z)} = 1;
+  let 'y = x;
+  foo(x);
+  let 'x : {'z, 'z == 2. int('z)} = 2;
+  foo(y);
+}
+\ No newline at end of file
diff --git a/test/typecheck/pass/shadow_let/v1.expect b/test/typecheck/pass/shadow_let/v1.expect
new file mode 100644
index 00000000..3cd21dc0
--- /dev/null
+++ b/test/typecheck/pass/shadow_let/v1.expect
@@ -0,0 +1,12 @@
+Type error:
+[[96mshadow_let/v1.sail[0m]:13:6-7
+13[96m |[0m  bar(y);
+  [91m |[0m      [91m^[0m
+  [91m |[0m Tried performing type coercion from int('_x#1) to int(2) on y
+  [91m |[0m Coercion failed because:
+  [91m |[0m int('_x#1) is not a subtype of int(2)
+  [91m |[0m [[96mshadow_let/v1.sail[0m]:9:6-8
+  [91m |[0m 9[96m |[0m  let 'x : {'z, 'z == 1. int('z)} = 1;
+  [91m |[0m  [93m |[0m      [93m^^[0m
+  [91m |[0m  [93m |[0m '_x#1 bound here
+  [91m |[0m 
diff --git a/test/typecheck/pass/shadow_let/v1.sail b/test/typecheck/pass/shadow_let/v1.sail
new file mode 100644
index 00000000..d7dc20a5
--- /dev/null
+++ b/test/typecheck/pass/shadow_let/v1.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+register R : int
+
+val foo : int(1) -> unit
+val bar : int(2) -> unit
+
+function main((): unit) -> unit = {
+  let 'x : {'z, 'z == 1. int('z)} = 1;
+  let 'y = x;
+  foo(x);
+  let 'x : {'z, 'z == 2. int('z)} = 2;
+  bar(y);
+}
+\ No newline at end of file