4 files changed, 64 insertions, 0 deletions

diff --git a/test/typecheck/fail/shadow_leak_check.expect b/test/typecheck/fail/shadow_leak_check.expect
new file mode 100644
index 00000000..a92e0078
--- /dev/null
+++ b/test/typecheck/fail/shadow_leak_check.expect
@@ -0,0 +1,8 @@
+Type error:
+[shadow_leak_check.sail]:17:5-18:6
+17 |     let 'x = some_other_int();
+   |     ^-------------------------
+18 |     x
+   |-----^
+   | Type variable 'x would leak into a scope where it is shadowed
+   | 
diff --git a/test/typecheck/fail/shadow_leak_check.sail b/test/typecheck/fail/shadow_leak_check.sail
new file mode 100644
index 00000000..266a0469
--- /dev/null
+++ b/test/typecheck/fail/shadow_leak_check.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+function some_int() -> int = {
+  4
+}
+
+function some_other_int() -> int = {
+  5
+}
+
+val test : forall 'n 'm, 'n == 'm. (int('n), int('m)) -> unit
+
+function main() -> unit = {
+  let 'x = some_int();
+
+  let 'y: int('x) = {
+     let 'x = some_other_int();
+     x
+  };
+
+  _prove(constraint('x == 'y));
+
+  test(x, y)
+}
diff --git a/test/typecheck/fail/shadow_leak_infer.expect b/test/typecheck/fail/shadow_leak_infer.expect
new file mode 100644
index 00000000..63aba5d7
--- /dev/null
+++ b/test/typecheck/fail/shadow_leak_infer.expect
@@ -0,0 +1,8 @@
+Type error:
+[shadow_leak_infer.sail]:17:5-18:6
+17 |     let 'x = some_other_int();
+   |     ^-------------------------
+18 |     x
+   |-----^
+   | Type variable '_x would leak into a scope where it is shadowed
+   | 
diff --git a/test/typecheck/fail/shadow_leak_infer.sail b/test/typecheck/fail/shadow_leak_infer.sail
new file mode 100644
index 00000000..cb122cf9
--- /dev/null
+++ b/test/typecheck/fail/shadow_leak_infer.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+function some_int() -> int = {
+  4
+}
+
+function some_other_int() -> int = {
+  5
+}
+
+val test : forall 'n 'm, 'n == 'm. (int('n), int('m)) -> unit
+
+function main() -> unit = {
+  let 'x = some_int();
+
+  let 'y = {
+     let 'x = some_other_int();
+     x
+  };
+
+  _prove(constraint('x == 'y));
+
+  test(x, y)
+}