Add a test for the private keyword

Improve the error message for trying to use a private definition
from a module that hasn't been required

editors/sail-mode.el

@@ -34,7 +34,7 @@
   '("val" "outcome" "function" "type" "struct" "union" "enum" "let" "var" "if" "then" "by"
     "else" "match" "in" "return" "register" "ref" "forall" "operator" "effect"
     "overload" "cast" "sizeof" "constant" "constraint" "default" "assert" "newtype" "from"
-    "pure" "monadic" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to"
+    "pure" "monadic" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to" "private"
     "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield"
     "mapping" "where" "with" "implicit" "instantiation" "impl" "forwards" "backwards"))
 

src/lib/type_check.ml

@@ -4482,7 +4482,7 @@ let check_fundef env def_annot (FD_aux (FD_function (recopt, tannot_opt, funcls)
         (* No val, so get the function type from annotations attached to clauses *)
         let bind = infer_funtyp l env tannot_opt funcls in
         (None, bind, env)
-    | exception Type_error (l, Err_not_in_scope (_, scope_l, item_scope, into_scope, priv)) ->
+    | exception Type_error (l, Err_not_in_scope (_, scope_l, item_scope, into_scope, is_opened, priv)) ->
         (* If we defined the function type with val in another module, but didn't require it. *)
         let reason = if priv then "private." else "not in scope." in
         typ_raise l
@@ -4491,6 +4491,7 @@ let check_fundef env def_annot (FD_aux (FD_function (recopt, tannot_opt, funcls)
                scope_l,
                item_scope,
                into_scope,
+               is_opened,
                priv
              )
           )

src/lib/type_env.ml

@@ -168,14 +168,15 @@ let filter_items_with f env bindings =
 let filter_items env bindings = filter_items_with (fun x -> x) env bindings
 
 let err_not_in_scope env msg l item =
+  let is_opened = Project.ModSet.mem item.mod_id env.opened in
   match env.global.modules with
-  | None -> Err_not_in_scope (msg, l, None, None, is_private item.visibility)
+  | None -> Err_not_in_scope (msg, l, None, None, is_opened, is_private item.visibility)
   | Some proj ->
       let module_name_opt mod_id =
         if Project.valid_module_id proj mod_id then Some (Project.module_name proj mod_id) else None
       in
       Err_not_in_scope
-        (msg, l, module_name_opt item.mod_id, module_name_opt env.current_module, is_private item.visibility)
+        (msg, l, module_name_opt item.mod_id, module_name_opt env.current_module, is_opened, is_private item.visibility)
 
 let get_item_with_loc get_loc l env item =
   if item_in_scope env item then item.item

src/lib/type_error.ml

@@ -460,7 +460,7 @@ let message_of_type_error type_error =
           None
         )
     | Err_no_num_ident id -> (Line ("No num identifier " ^ string_of_id id), None)
-    | Err_not_in_scope (explanation, Some l, item_scope, into_scope, priv) ->
+    | Err_not_in_scope (explanation, Some l, item_scope, into_scope, is_opened, priv) ->
         let suggest, in_mod, add_requires_here =
           match (item_scope, into_scope) with
           | None, None -> ("Try bringing the following into scope:", "", [])
@@ -496,16 +496,20 @@ let message_of_type_error type_error =
               ),
             None
           )
-        else
+        else (
+          let private_not_opened =
+            if not is_opened then [Line "The module containing this definition is also not required in this context"]
+            else []
+          in
           ( Seq
-              [
-                Line (Option.value ~default:"Cannot use private definition" explanation);
-                Line "";
-                Location ("", Some ("private definition here" ^ in_mod), l, Seq []);
-              ],
+              ([Line (Option.value ~default:"Cannot use private definition" explanation)]
+              @ private_not_opened
+              @ [Line ""; Location ("", Some ("private definition here" ^ in_mod), l, Seq [])]
+              ),
             None
           )
-    | Err_not_in_scope (explanation, None, _, _, _) -> (Line (Option.value ~default:"Not in scope" explanation), None)
+        )
+    | Err_not_in_scope (explanation, None, _, _, _, _) -> (Line (Option.value ~default:"Not in scope" explanation), None)
   in
   to_message type_error
 

src/lib/type_error.mli

@@ -78,7 +78,7 @@ type type_error =
   | Err_other of string
   | Err_inner of type_error * Parse_ast.l * string * type_error
   | Err_not_in_scope of
-      string option * Parse_ast.l option * string Project.spanned option * string Project.spanned option * bool
+      string option * Parse_ast.l option * string Project.spanned option * string Project.spanned option * bool * bool
   | Err_instantiation_info of int * type_error
   | Err_function_arg of Parse_ast.l * typ * type_error
   | Err_no_function_type of { id : id; functions : (typquant * typ) Bindings.t }

src/lib/type_internal.ml

@@ -85,7 +85,7 @@ type type_error =
   | Err_other of string
   | Err_inner of type_error * Parse_ast.l * string * type_error
   | Err_not_in_scope of
-      string option * Parse_ast.l option * string Project.spanned option * string Project.spanned option * bool
+      string option * Parse_ast.l option * string Project.spanned option * string Project.spanned option * bool * bool
   | Err_instantiation_info of int * type_error
   | Err_function_arg of Parse_ast.l * typ * type_error
   | Err_no_function_type of { id : id; functions : (typquant * typ) Bindings.t }

test/typecheck/project/fail_private.expect

@@ -0,0 +1,9 @@
+Type error:
+project/private/bmod.sail:4.4-7:
+4 |    foo("Cannot be called")
+  |    ^-^
+  | Cannot use private definition
+  | 
+  | project/private/amod.sail:3.17-20:
+  | 3 |private function foo(message : string) -> unit = {
+  |   |                 ^-^ private definition here in A

test/typecheck/project/fail_private.sail_project

@@ -0,0 +1,9 @@
+
+A {
+  files private/amod.sail
+}
+
+B {
+  requires A
+  files private/bmod.sail
+}

test/typecheck/project/fail_private_nr.expect

@@ -0,0 +1,10 @@
+Type error:
+project/private/bmod.sail:4.4-7:
+4 |    foo("Cannot be called")
+  |    ^-^
+  | Cannot use private definition
+  | The module containing this definition is also not required in this context
+  | 
+  | project/private/amod.sail:3.17-20:
+  | 3 |private function foo(message : string) -> unit = {
+  |   |                 ^-^ private definition here in A

test/typecheck/project/fail_private_nr.sail_project

@@ -0,0 +1,8 @@
+
+A {
+  files private/amod.sail
+}
+
+B {
+  files private/bmod.sail
+}

test/typecheck/project/private/amod.sail

@@ -0,0 +1,5 @@
+$include <string.sail>
+
+private function foo(message : string) -> unit = {
+  print_endline(message)
+}

test/typecheck/project/private/bmod.sail

@@ -0,0 +1,5 @@
+val main : unit -> unit
+
+function main() = {
+    foo("Cannot be called")
+}