Correctly erased n-ary ghost functions.

src/typechecker/FStarC.TypeChecker.Env.fst

@@ -1037,7 +1037,13 @@ let rec non_informative env t =
       if is_ghost_effect (comp_effect_name c) || is_erasable_effect env (comp_effect_name c) then
         // Functions with a ghost effect can only be invoked in a ghost context,
         // therefore it is safe to erase them to unit, a non-function.
-        Some unit_const
+        if List.length bs <= 1 then
+          Some unit_const
+        else
+          // However, this is only true for the full application;
+          // `a -> b -> GTot c` is equivalent to `a -> Tot (b -> GTot c)`
+          // and needs to be erased to `fun x -> ()`.
+          Some (mk (Tm_abs { body = unit_const; rc_opt = None; bs = List.init bs }) t.pos)
       else if is_pure_comp c then
         // Only the result of a pure computation can be erased;
         // a pure function can be still be invoked in non-ghost contexts (see #3366)

ulib/FStar.ModifiesGen.fst

@@ -1184,6 +1184,7 @@ let loc_includes_loc_regions_restrict_to_regions
   (loc_includes (loc_regions false rs) (restrict_to_regions l rs))
 = Classical.forall_intro (loc_aux_includes_refl #al #c)
 
+#push-options "--z3rlimit_factor 2"
 let modifies_only_live_regions #al #c rs l h h' =
   let s = l in
   let c_rs = Set.complement rs in
@@ -1205,6 +1206,7 @@ let modifies_only_live_regions #al #c rs l h h' =
   modifies_only_live_regions_weak rs s_c_rs h h';
   loc_includes_restrict_to_regions s c_rs;
   modifies_loc_includes s h h' s_c_rs
+#pop-options
 
 let no_upd_fresh_region #al #c r l h0 h1 =
   modifies_only_live_regions (HS.mod_set (Set.singleton r)) l h0 h1