Merge pull request #3762 from mtzguido/imps

Tc: fix implicit vs explicit check

src/typechecker/FStarC.TypeChecker.TcTerm.fst

@@ -140,35 +140,32 @@ let check_no_escape (head_opt : option term)
    the user is expected to write f #a to apply f, matching the
    implicit qualifier at the binding site.
 
-   However, they do not (and cannot, there's no syntax for it) provide
-   the attributes of the binding site at the application site.
+   However, users do not provide the attributes of the
+   binding site at the application site. NEVERTHELESS, we do
+   internally add the attributes in the application node, and
+   as we sometimes re-check terms, aq could contain attributes.
+   These should just be ignored and replaced by those of b.
 
    So, this function checks that the implicit flags match and takes
    the attributes from the binding site, i.e., expected_aq.
 *)
 let check_expected_aqual_for_binder (aq:aqual) (b:binder) (pos:Range.range) : aqual =
-  match
-    let expected_aq = U.aqual_of_binder b in
-    match aq, expected_aq with
-    | None, None -> Inr aq
-    | None, Some eaq ->
-      if eaq.aqual_implicit //programmer should have written #
-      then Inl "expected implicit annotation on the argument"
-      else Inr expected_aq //keep the attributes
-    | Some aq, None ->
-      Inl "expected an explicit argument (without annotation)"
-    | Some aq, Some eaq ->
-      if aq.aqual_implicit <> eaq.aqual_implicit
-      then Inl "mismatch"
-      else Inr expected_aq //keep the attributes
-  with
-  | Inl err ->
+  let expected_aq = U.aqual_of_binder b in
+  // All we check is that the "plicity" matches, and
+  // keep attributes of the binder.
+  let is_imp (a:aqual) : bool = match a with | Some a -> a.aqual_implicit | _ -> false in
+  if is_imp aq <> is_imp expected_aq then begin
     let open FStarC.Pprint in
+    let open FStarC.Errors.Msg in
     let msg = [
-      Errors.Msg.text ("Inconsistent argument qualifiers: " ^ err ^ ".");
+      text "Inconsistent argument qualifiers.";
+      text (BU.format2 "Expected an %splicit argument, got an %splicit one."
+              (if is_imp aq then "im" else "ex")
+              (if is_imp expected_aq then "im" else "ex"));
     ] in
     raise_error pos Errors.Fatal_InconsistentImplicitQualifier msg
-  | Inr r -> r
+  end;
+  expected_aq
 
 let check_erasable_binder_attributes env attrs (binder_ty:typ) =
     attrs |>

tests/error-messages/ArgsMismatch.fst

@@ -0,0 +1,31 @@
+module ArgsMismatch
+
+(* Attributes on arguments don't matter at all for applications. *)
+
+let foo (#x:int) (y:int) = x+y
+
+[@@expect_failure] let _ = foo 1 2
+[@@expect_failure] let _ = foo #1 #2
+                   let _ = foo #1 2
+[@@expect_failure] let _ = foo 1 #2
+
+let bar (#[@@@1]x:int) (y:int) = x+y
+
+[@@expect_failure] let _ = bar 1 2
+[@@expect_failure] let _ = bar #1 #2
+                   let _ = bar #1 2
+[@@expect_failure] let _ = bar 1 #2
+
+let baz (#x:int) ([@@@2]y:int) = x+y
+
+[@@expect_failure] let _ = baz 1 2
+[@@expect_failure] let _ = baz #1 #2
+                   let _ = baz #1 2
+[@@expect_failure] let _ = baz 1 #2
+
+let qux (#[@@@1]x:int) ([@@@2]y:int) = x+y
+
+[@@expect_failure] let _ = qux 1 2
+[@@expect_failure] let _ = qux #1 #2
+                   let _ = qux #1 2
+[@@expect_failure] let _ = qux 1 #2

tests/error-messages/ArgsMismatch.fst.json_output.expected

@@ -0,0 +1,36 @@
+>> Got issues: [
+{"msg":["Too many arguments to function of type y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":7,"col":33},"end_pos":{"line":7,"col":34}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":7,"col":33},"end_pos":{"line":7,"col":34}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+>>]
+>> Got issues: [
+{"msg":["Inconsistent argument qualifiers.","Expected an implicit argument, got an explicit one."],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":8,"col":35},"end_pos":{"line":8,"col":36}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":8,"col":35},"end_pos":{"line":8,"col":36}}},"number":92,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+>>]
+>> Got issues: [
+{"msg":["Too many arguments to function of type y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":10,"col":34},"end_pos":{"line":10,"col":35}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":10,"col":34},"end_pos":{"line":10,"col":35}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___1`","While typechecking the top-level declaration `[@@expect_failure] let uu___1`"]}
+>>]
+>> Got issues: [
+{"msg":["Too many arguments to function of type y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":14,"col":33},"end_pos":{"line":14,"col":34}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":14,"col":33},"end_pos":{"line":14,"col":34}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___1`","While typechecking the top-level declaration `[@@expect_failure] let uu___1`"]}
+>>]
+>> Got issues: [
+{"msg":["Inconsistent argument qualifiers.","Expected an implicit argument, got an explicit one."],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":15,"col":35},"end_pos":{"line":15,"col":36}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":15,"col":35},"end_pos":{"line":15,"col":36}}},"number":92,"ctx":["While typechecking the top-level declaration `let uu___1`","While typechecking the top-level declaration `[@@expect_failure] let uu___1`"]}
+>>]
+>> Got issues: [
+{"msg":["Too many arguments to function of type y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":17,"col":34},"end_pos":{"line":17,"col":35}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":17,"col":34},"end_pos":{"line":17,"col":35}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___2`","While typechecking the top-level declaration `[@@expect_failure] let uu___2`"]}
+>>]
+>> Got issues: [
+{"msg":["Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":21,"col":33},"end_pos":{"line":21,"col":34}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":21,"col":33},"end_pos":{"line":21,"col":34}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___2`","While typechecking the top-level declaration `[@@expect_failure] let uu___2`"]}
+>>]
+>> Got issues: [
+{"msg":["Inconsistent argument qualifiers.","Expected an implicit argument, got an explicit one."],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":22,"col":35},"end_pos":{"line":22,"col":36}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":22,"col":35},"end_pos":{"line":22,"col":36}}},"number":92,"ctx":["While typechecking the top-level declaration `let uu___2`","While typechecking the top-level declaration `[@@expect_failure] let uu___2`"]}
+>>]
+>> Got issues: [
+{"msg":["Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":24,"col":34},"end_pos":{"line":24,"col":35}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":24,"col":34},"end_pos":{"line":24,"col":35}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___3`","While typechecking the top-level declaration `[@@expect_failure] let uu___3`"]}
+>>]
+>> Got issues: [
+{"msg":["Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":28,"col":33},"end_pos":{"line":28,"col":34}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":28,"col":33},"end_pos":{"line":28,"col":34}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___3`","While typechecking the top-level declaration `[@@expect_failure] let uu___3`"]}
+>>]
+>> Got issues: [
+{"msg":["Inconsistent argument qualifiers.","Expected an implicit argument, got an explicit one."],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":29,"col":35},"end_pos":{"line":29,"col":36}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":29,"col":35},"end_pos":{"line":29,"col":36}}},"number":92,"ctx":["While typechecking the top-level declaration `let uu___3`","While typechecking the top-level declaration `[@@expect_failure] let uu___3`"]}
+>>]
+>> Got issues: [
+{"msg":["Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Error","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":31,"col":34},"end_pos":{"line":31,"col":35}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":31,"col":34},"end_pos":{"line":31,"col":35}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___4`","While typechecking the top-level declaration `[@@expect_failure] let uu___4`"]}
+>>]

tests/error-messages/ArgsMismatch.fst.output.expected

@@ -0,0 +1,80 @@
+>> Got issues: [
+* Error 173 at ArgsMismatch.fst(7,33-7,34):
+  - Too many arguments to function of type y: Prims.int -> Prims.int
+  - Got 2 arguments
+  - Remaining type is Prims.int
+
+>>]
+>> Got issues: [
+* Error 92 at ArgsMismatch.fst(8,35-8,36):
+  - Inconsistent argument qualifiers.
+  - Expected an implicit argument, got an explicit one.
+
+>>]
+>> Got issues: [
+* Error 173 at ArgsMismatch.fst(10,34-10,35):
+  - Too many arguments to function of type y: Prims.int -> Prims.int
+  - Got 2 arguments
+  - Remaining type is Prims.int
+
+>>]
+>> Got issues: [
+* Error 173 at ArgsMismatch.fst(14,33-14,34):
+  - Too many arguments to function of type y: Prims.int -> Prims.int
+  - Got 2 arguments
+  - Remaining type is Prims.int
+
+>>]
+>> Got issues: [
+* Error 92 at ArgsMismatch.fst(15,35-15,36):
+  - Inconsistent argument qualifiers.
+  - Expected an implicit argument, got an explicit one.
+
+>>]
+>> Got issues: [
+* Error 173 at ArgsMismatch.fst(17,34-17,35):
+  - Too many arguments to function of type y: Prims.int -> Prims.int
+  - Got 2 arguments
+  - Remaining type is Prims.int
+
+>>]
+>> Got issues: [
+* Error 173 at ArgsMismatch.fst(21,33-21,34):
+  - Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int
+  - Got 2 arguments
+  - Remaining type is Prims.int
+
+>>]
+>> Got issues: [
+* Error 92 at ArgsMismatch.fst(22,35-22,36):
+  - Inconsistent argument qualifiers.
+  - Expected an implicit argument, got an explicit one.
+
+>>]
+>> Got issues: [
+* Error 173 at ArgsMismatch.fst(24,34-24,35):
+  - Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int
+  - Got 2 arguments
+  - Remaining type is Prims.int
+
+>>]
+>> Got issues: [
+* Error 173 at ArgsMismatch.fst(28,33-28,34):
+  - Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int
+  - Got 2 arguments
+  - Remaining type is Prims.int
+
+>>]
+>> Got issues: [
+* Error 92 at ArgsMismatch.fst(29,35-29,36):
+  - Inconsistent argument qualifiers.
+  - Expected an implicit argument, got an explicit one.
+
+>>]
+>> Got issues: [
+* Error 173 at ArgsMismatch.fst(31,34-31,35):
+  - Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int
+  - Got 2 arguments
+  - Remaining type is Prims.int
+
+>>]