From fe87bb2c265fde375a1977f8e38c0b1e9162872a Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 19 Mar 2020 23:09:54 +0000
Subject: Improve a particularly unhelpful type error

From:

No type variable 'ex14#

to:

Type error:
[../and_let_bool.sail]:6:19-50
6 |  and_bool(let y : bool = x in not_bool(y), x)
  |           ^-----------------------------^
  | The type variable 'ex14# would leak into an outer scope.
  |
  | Try adding a type annotation to this expression.
  | This error was caused by:
  | [../and_let_bool.sail]:6:23-24
  | 6 |  and_bool(let y : bool = x in not_bool(y), x)
  |   |               ^
  |   | Type variable 'ex14# was introduced here
  |
---
 src/type_check.ml | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index f11b955a..82bc92d8 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -439,6 +439,7 @@ module Env : sig
   val add_constraint : n_constraint -> t -> t
   val get_typ_var : kid -> t -> kind_aux
   val get_typ_var_loc : kid -> t -> Ast.l
+  val get_typ_var_loc_opt : kid -> t -> Ast.l option
   val get_typ_vars : t -> kind_aux KBindings.t
   val get_typ_var_locs : t -> Ast.l KBindings.t
   val shadows : kid -> t -> int
@@ -536,6 +537,11 @@ end = struct
   let allow_unknowns env = env.allow_unknowns
   let set_allow_unknowns b env = { env with allow_unknowns = b }
 
+  let get_typ_var_loc_opt kid env =
+    match KBindings.find_opt kid env.typ_vars with
+    | Some (l, _) -> Some l
+    | None -> None
+                               
   let get_typ_var kid env =
     try snd (KBindings.find kid env.typ_vars) with
     | Not_found -> typ_error env (kid_loc kid) ("No type variable " ^ string_of_kid kid)
@@ -1404,12 +1410,26 @@ let bind_numeric l typ 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 =
+  typ_debug (lazy ("Shadow leaks: " ^ string_of_typ 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 ())
+      else
+        match Env.get_typ_var_loc_opt var outer_env with
+        | Some _ -> ()
+        | None ->
+           match Env.get_typ_var_loc_opt var inner_env with
+           | Some leak_l ->
+              typ_raise outer_env l
+                (Err_because
+                   (Err_other ("The type variable " ^ string_of_kid var
+                               ^ " would leak into an outer scope.\n\nTry adding a type annotation to this expression."),
+                    leak_l,
+                    Err_other ("Type variable " ^ string_of_kid var ^ " was introduced here")))
+           | None -> Reporting.unreachable l __POS__ "Found a type with an unknown type variable"
+    )
     (KidSet.elements vars);
   typ
    
-- 
cgit v1.2.3