Merge pull request #4253 from mtzguido/4252

Tc: consider effect arguments in positivity check

Author: mtzguido

src/typechecker/FStarC.TypeChecker.Positivity.fst

@@ -877,12 +877,23 @@ let rec ty_strictly_positive_in_type (env:env)
           and that it is strictly positive in the return type");
        let sbs, c = U.arrow_formals_comp in_type in
        let return_type = FStarC.Syntax.Util.comp_result c in
+       let effect_args = U.comp_effect_args c in
        let ty_lid_not_to_left_of_arrow =
             L.for_all 
                (fun ({binder_bv=b}) -> mutuals_unused_in_type mutuals b.sort)
                sbs
        in
-       if ty_lid_not_to_left_of_arrow
+       (* We should also consider the effect arguments for positivity. See
+       https://github.com/FStarLang/FStar/issues/4252. We simply forbid the
+       effect args from mentioning the type. We do not track positivity
+       of effect definitions or mark arguments as positive. If this becomes
+       a limitation, we should revisit. *)
+       let mutuals_unused_in_effect_args =
+            L.for_all
+               (fun (a, _) -> mutuals_unused_in_type mutuals a)
+               effect_args
+       in
+       if ty_lid_not_to_left_of_arrow && mutuals_unused_in_effect_args
        then (
          (* and is strictly positive also in the return type  *)
          ty_strictly_positive_in_type 

tests/bug-reports/closed/Bug4252.fst

@@ -0,0 +1,18 @@
+module Bug4252
+
+[@@expect_failure [3]]
+noeq
+type t =
+  | C : (unit -> Pure unit True (fun _ -> (exists (x:t). True) ==> False)) -> t
+
+[@@expect_failure [3]]
+noeq
+type t' =
+  | C : (unit -> Pure unit True (fun _ -> forall (x:t'). False)) -> t'
+
+// let f1 (x : t) : Lemma False =
+//   match x with
+//   | C f -> f ()
+
+// let f2 : False =
+//   f1 (C (fun _ -> Classical.forall_intro f1))