teach IR typechecker to reject refutable import patterns

Author: ggreif

src/ir_def/check_ir.ml

@@ -1057,7 +1057,10 @@ and check_dec env dec  =
   | LetD (pat, exp) ->
     ignore (check_pat_exhaustive env pat);
     check_exp env exp;
-    typ exp <: pat.note
+    typ exp <: pat.note;
+    check env pat.at
+      Ir_utils.(expected_irrefutable dec ==> is_irrefutable pat)
+      "refutable pattern in import"
   | VarD (id, t, exp) ->
     check_exp env exp;
     typ exp <: t

src/ir_def/ir_utils.ml

@@ -7,3 +7,8 @@ let rec is_irrefutable p = match p.it with
   | WildP | VarP _ -> true
   | TagP _ | LitP _ | OptP _ -> false
 
+
+let expected_irrefutable : dec -> bool = function
+  | { it = LetD (_, { it = VarE id; _ }); _ } ->
+    Lib.String.starts_with "file$" id
+  | _ -> false

src/lib/lib.ml

@@ -195,6 +195,11 @@ struct
     else
       None
 
+  let starts_with prefix s = (* in OCaml 4.13 *)
+    match chop_prefix prefix s with
+    | Some _ -> true
+    | _ -> false
+
   let chop_suffix suffix s =
     let suffix_len = String.length suffix in
     let s_len = String.length s in

src/lib/lib.mli

@@ -154,6 +154,7 @@ sig
   val split : string -> char -> string list
   val breakup : string -> int -> string list
   val find_from_opt : (char -> bool) -> string -> int -> int option
+  val starts_with : string -> string -> bool
   val chop_prefix : string -> string -> string option
   val chop_suffix : string -> string -> string option
   val lightweight_escaped : string -> string

test/fail/nat-module.mo

@@ -0,0 +1 @@
+module { public let why = 42 }

test/fail/ok/refutable-import.run-ir.ok

@@ -0,0 +1,2 @@
+Ill-typed intermediate code after Desugaring (use -v to see dumped IR):
+refutable-import.mo:1.8-1.20: IR type error [M0000], refutable pattern in import

test/fail/ok/refutable-import.run-ir.ret.ok

@@ -0,0 +1 @@
+Return code 1

test/fail/ok/refutable-import.tc.ok

@@ -0,0 +1,4 @@
+refutable-import.mo:1.8-1.20: warning [M0145], this pattern of type
+  module {why : Nat}
+does not cover value
+  {why = 0 or 1 or _}

test/fail/refutable-import.mo

@@ -0,0 +1,5 @@
+import { why = 42 } = "nat-module";
+
+//SKIP run
+//SKIP run-low
+//SKIP comp