5 files changed, 87 insertions, 7 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index 0871272b..73ad5362 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -440,6 +440,7 @@ module Env : sig
   val get_typ_var_loc : kid -> t -> Ast.l
   val get_typ_vars : t -> kind_aux KBindings.t
   val get_typ_var_locs : t -> Ast.l KBindings.t
+  val shadows : kid -> t -> int
   val add_typ_var_shadow : l -> kinded_id -> t -> t * kid option
   val add_typ_var : l -> kinded_id -> t -> t
   val get_ret_typ : t -> typ option
@@ -1224,6 +1225,8 @@ end = struct
     with
     | Not_found -> Unbound
 
+  let shadows v env = match KBindings.find_opt v env.shadow_vars with Some n -> n | None -> 0
+                 
   let add_typ_var_shadow l (KOpt_aux (KOpt_kind (K_aux (k, _), v), _)) env =
     if KBindings.mem v env.typ_vars then begin
         let n = match KBindings.find_opt v env.shadow_vars with Some n -> n | None -> 0 in
@@ -1399,6 +1402,16 @@ let bind_numeric l typ env =
      nexp, add_existential l (List.map (mk_kopt K_int) kids) nc env
   | None -> typ_error env l ("Expected " ^ string_of_typ typ ^ " to be numeric")
 
+let rec check_shadow_leaks l inner_env outer_env typ =
+  let vars = tyvars_of_typ typ in
+  List.iter (fun var ->
+      if Env.shadows var inner_env > Env.shadows var outer_env then
+        typ_error outer_env l
+          ("Type variable " ^ string_of_kid var ^ " would leak into a scope where it is shadowed")
+      else ())
+    (KidSet.elements vars);
+  typ
+   
 (** Pull an (potentially)-existentially qualified type into the global
    typing environment **)
 let bind_existential l name typ env =
@@ -2845,12 +2858,14 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
        | LB_val (P_aux (P_typ (ptyp, _), _) as pat, bind) ->
           Env.wf_typ env ptyp;
           let checked_bind = crule check_exp env bind ptyp in
-          let tpat, env = bind_pat_no_guard env pat ptyp in
-          annot_exp (E_let (LB_aux (LB_val (tpat, checked_bind), (let_loc, None)), crule check_exp env exp typ)) typ
+          let tpat, inner_env = bind_pat_no_guard env pat ptyp in
+          annot_exp (E_let (LB_aux (LB_val (tpat, checked_bind), (let_loc, None)), crule check_exp inner_env exp typ))
+            (check_shadow_leaks l inner_env env typ)
        | LB_val (pat, bind) ->
           let inferred_bind = irule infer_exp env bind in
-          let tpat, env = bind_pat_no_guard env pat (typ_of inferred_bind) in
-          annot_exp (E_let (LB_aux (LB_val (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ
+          let tpat, inner_env = bind_pat_no_guard env pat (typ_of inferred_bind) in
+          annot_exp (E_let (LB_aux (LB_val (tpat, inferred_bind), (let_loc, None)), crule check_exp inner_env exp typ))
+            (check_shadow_leaks l inner_env env typ)
      end
   | E_app_infix (x, op, y), _ ->
      check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ
@@ -3960,9 +3975,10 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        | LB_val (pat, bind) ->
           let inferred_bind = irule infer_exp env bind in
           inferred_bind, pat, typ_of inferred_bind in
-     let tpat, env = bind_pat_no_guard env pat ptyp in
-     let inferred_exp = irule infer_exp env exp in
-     annot_exp (E_let (LB_aux (LB_val (tpat, bind_exp), (let_loc, None)), inferred_exp)) (typ_of inferred_exp)
+     let tpat, inner_env = bind_pat_no_guard env pat ptyp in
+     let inferred_exp = irule infer_exp inner_env exp in
+     annot_exp (E_let (LB_aux (LB_val (tpat, bind_exp), (let_loc, None)), inferred_exp))
+       (check_shadow_leaks l inner_env env (typ_of inferred_exp))
   | E_ref id when Env.is_register id env ->
      let _, _, typ = Env.get_register id env in
      annot_exp (E_ref id) (register_typ typ)
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)
+}