Replace must_erase_during_extraction with erasable.

src/typechecker/FStarC.TypeChecker.Env.fst

@@ -932,13 +932,8 @@ let cache_in_fv_tab (tab:BU.smap 'a) (fv:fv) (f:unit -> (bool & 'a)) : 'a =
 let fv_has_erasable_attr env fv =
   let f () =
      let ex, erasable = fv_exists_and_has_attr env fv.fv_name.v Const.erasable_attr in
-     ex,erasable
-     //unfortunately, treating the Const.must_erase_for_extraction_attr
-     //in the same way here as erasable_attr leads to regressions in fragile proofs,
-     //notably in FStar.ModifiesGen, since this expands the class of computation types
-     //that can be promoted from ghost to tot. That in turn results in slightly different
-     //smt encodings, leading to breakages. So, sadly, I'm not including must_erase_for_extraction
-     //here. In any case, must_erase_for_extraction is transitionary and should be removed
+     let ex, must_erase_for_extraction = fv_exists_and_has_attr env fv.fv_name.v Const.must_erase_for_extraction_attr in
+     ex, erasable || must_erase_for_extraction
   in
   cache_in_fv_tab env.erasable_types_tab fv f
 
@@ -1034,10 +1029,12 @@ let rec non_informative env t =
       || fv_eq_lid fv Const.erased_lid
       || fv_has_erasable_attr env fv
     | Tm_app {hd=head} -> non_informative env head
+    | Tm_abs {body} -> non_informative env body
     | Tm_uinst (t, _) -> non_informative env t
     | Tm_arrow {comp=c} ->
       (is_pure_or_ghost_comp c && non_informative env (comp_result c))
       || is_erasable_effect env (comp_effect_name c)
+    | Tm_meta {tm} -> non_informative env tm
     | _ -> false
 
 let num_effect_indices env name r =

src/typechecker/FStarC.TypeChecker.Env.fsti

@@ -341,7 +341,11 @@ val fv_with_lid_has_attr   : env -> fv_lid:lid -> attr_lid:lid -> bool
 val fv_has_attr            : env -> fv -> attr_lid:lid -> bool
 val fv_has_strict_args     : env -> fv -> option (list int)
 val fv_has_erasable_attr   : env -> fv -> bool
+
+(* `non_informative env t` is true if the type family `t: (... -> Type) is noninformative,
+   i.e., any `x: t ...` can be erased to `()`. *)
 val non_informative        : env -> typ -> bool
+
 val try_lookup_effect_lid  : env -> lident -> option term
 val lookup_effect_lid      : env -> lident -> term
 val lookup_effect_abbrev   : env -> universes -> lident -> option (binders & comp)

src/typechecker/FStarC.TypeChecker.Normalize.fst

@@ -2808,6 +2808,8 @@ let non_info_norm env t =
   let steps = [UnfoldUntil delta_constant;
                AllowUnboundUniverses;
                EraseUniverses;
+               Primops;
+               Beta; Iota;
                HNF;
                (* We could use Weak too were it not that we need
                 * to descend in the codomain of arrows. *)

src/typechecker/FStarC.TypeChecker.Quals.fst

@@ -161,6 +161,26 @@ let check_sigelt_quals_pre (env:FStarC.TypeChecker.Env.env) se =
         then err []
       | _ -> ()
 
+// A faster under-approximation of non_info_norm.
+// We call this function on every let-binding that has an interface val
+// (while non_info_norm is only called on types),
+// so it needs to be fast and shouldn't unfold too much.
+// The regular non_info_norm doesn't set Weak,
+// which makes the normalizer reduce lets.
+let non_info_norm_weak env t =
+  let steps = [UnfoldUntil delta_constant;
+               AllowUnboundUniverses;
+               EraseUniverses;
+               Primops;
+               Beta; Iota;
+               HNF;
+               Weak;
+               Unascribe;   //remove ascriptions
+               ForExtraction //and refinement types
+               ]
+  in
+  non_informative env (N.normalize steps env t)
+
 let check_erasable env quals (r:Range.range) se =
   let lids = U.lids_of_sigelt se in
   let val_exists =
@@ -183,6 +203,22 @@ let check_erasable env quals (r:Range.range) se =
            text "Mismatch of attributes between declaration and definition.";
            text "Definition is marked `erasable` but the declaration is not.";
          ];
+  if not se_has_erasable_attr && not (Options.ide ()) then begin
+    match se.sigel with
+    | Sig_let {lbs=(false, [lb])} ->
+      let lbname = BU.right lb.lbname in
+      let has_iface_val = match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with
+        | Some iface_decls -> iface_decls |> BU.for_some (Parser.AST.decl_is_val (ident_of_lid lbname.fv_name.v))
+        | None -> false in
+      let _, body, _ = U.abs_formals lb.lbdef in
+      if has_iface_val && non_info_norm_weak env body then log_issue lbname Error_MustEraseMissing [
+        text (BU.format2 "Values of type `%s` will be erased during extraction, \
+              but its interface hides this fact. Add the `erasable` \
+              attribute to the `val %s` declaration for this symbol in the interface"
+              (show lbname) (show lbname));
+      ]
+    | _ -> ()
+  end;
   if se_has_erasable_attr
   then begin
     match se.sigel with
@@ -221,47 +257,6 @@ let check_erasable env quals (r:Range.range) se =
         ]
   end
 
-(*
- *  Given `val t : Type` in an interface
- *  and   `let t = e`    in the corresponding implementation
- *  The val declaration should contains the `must_erase_for_extraction` attribute
- *  if and only if `e` is a type that's non-informative (e..g., unit, t -> unit, etc.)
- *)
-let check_must_erase_attribute env se =
-  if Options.ide() then () else
-  match se.sigel with
-  | Sig_let {lbs; lids=l} ->
-    begin match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with
-     | None ->
-       ()
-
-     | Some iface_decls ->
-       snd lbs |> List.iter (fun lb ->
-           let lbname = BU.right lb.lbname in
-           let has_iface_val =
-               iface_decls |> BU.for_some (Parser.AST.decl_is_val (ident_of_lid lbname.fv_name.v))
-           in
-           if has_iface_val
-           then
-               let must_erase = TcUtil.must_erase_for_extraction env lb.lbdef in
-               let has_attr = Env.fv_has_attr env lbname C.must_erase_for_extraction_attr in
-               if must_erase && not has_attr
-               then log_issue lbname Error_MustEraseMissing [
-                        text (BU.format2 "Values of type `%s` will be erased during extraction, \
-                               but its interface hides this fact. Add the `must_erase_for_extraction` \
-                               attribute to the `val %s` declaration for this symbol in the interface"
-                               (show lbname) (show lbname));
-                      ]
-               else if has_attr && not must_erase
-               then log_issue lbname Error_MustEraseMissing [
-                        text (BU.format1 "Values of type `%s` cannot be erased during extraction, \
-                               but the `must_erase_for_extraction` attribute claims that it can. \
-                               Please remove the attribute."
-                               (show lbname));
-                      ])
-  end
-  | _ -> ()
-
 let check_typeclass_instance_attribute env (rng:Range.range) se =
   let is_tc_instance =
       se.sigattrs |> BU.for_some
@@ -316,6 +311,5 @@ let check_sigelt_quals_post env se =
   let quals = se.sigquals in
   let r = se.sigrng in
   check_erasable env quals r se;
-  check_must_erase_attribute env se;
   check_typeclass_instance_attribute env r se;
   ()

src/typechecker/FStarC.TypeChecker.Quals.fsti

@@ -29,7 +29,6 @@ after the function is typechecked.
 
 Currently, the only things that must be checked after the function is typechecked are:
 - The erasable attribute, since the defn must be elaborated. See #3253.
-- The must_erase attribute
 - The instance attribute for typeclasses
 *)
 

src/typechecker/FStarC.TypeChecker.Util.fst

@@ -3190,40 +3190,9 @@ let maybe_add_implicit_binders (env:env) (bs:binders) : binders =
 
 
 let must_erase_for_extraction (g:env) (t:typ) =
-    let rec descend env t = //t is expected to b in WHNF
-      match (SS.compress t).n with
-      | Tm_arrow _ ->
-           let bs, c = U.arrow_formals_comp t in
-           let env = FStarC.TypeChecker.Env.push_binders env bs in
-           (Env.is_erasable_effect env (U.comp_effect_name c))  //includes GHOST
-           || (U.is_pure_or_ghost_comp c && aux env (U.comp_result c))
-      | Tm_refine {b={sort=t}} ->
-           aux env t
-      | Tm_app {hd=head}
-      | Tm_uinst (head, _) ->
-           descend env head
-      | Tm_fvar fv ->
-           //special treatment for must_erase_for_extraction here
-           //See Env.type_is_erasable for more explanations
-           Env.fv_has_attr env fv C.must_erase_for_extraction_attr
-      | _ -> false
-    and aux env t =
-        let t = N.normalize [Env.Primops;
-                             Env.Weak;
-                             Env.HNF;
-                             Env.UnfoldUntil delta_constant;
-                             Env.Beta;
-                             Env.AllowUnboundUniverses;
-                             Env.Zeta;
-                             Env.Iota;
-                             Env.Unascribe] env t in
-//        debug g (fun () -> BU.print1 "aux %s\n" (show t));
-        let res = Env.non_informative env t || descend env t in
-        if !dbg_Extraction
-        then BU.print2 "must_erase=%s: %s\n" (if res then "true" else "false") (show t);
-        res
-    in
-    aux g t
+  let res = N.non_info_norm g t in
+  if !dbg_Extraction then BU.print2 "must_erase=%s: %s\n" (if res then "true" else "false") (show t);
+  res
 
 let effect_extraction_mode env l =
   l |> Env.norm_eff_name env

tests/micro-benchmarks/MustEraseForExtraction.fst

@@ -17,7 +17,8 @@ module MustEraseForExtraction
 [@@(expect_failure [318])]
 let t1 = unit
 
+[@@erasable]
 let t2 = unit
 
-[@@(expect_failure [318])]
+[@@(expect_failure [162])]
 let t3 = bool

tests/micro-benchmarks/MustEraseForExtraction.fsti

@@ -17,8 +17,8 @@ module MustEraseForExtraction
 
 val t1 : Type0
 
-[@@must_erase_for_extraction]
+[@@erasable]
 val t2 : Type0
 
-[@@must_erase_for_extraction]
+[@@erasable]
 val t3 : Type0

ulib/FStar.GSet.fsti

@@ -19,9 +19,9 @@ module FStar.GSet
 #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"
 
 (*
- * AR: mark it must_erase_for_extraction temporarily until CMI comes in
+ * AR: mark it erasable temporarily until CMI comes in
  *)
-[@@must_erase_for_extraction]
+[@@erasable]
 val set (a: Type u#a) : Type u#a
 
 val equal (#a:Type) (s1:set a) (s2:set a) : Type0

ulib/FStar.GhostSet.fsti

@@ -18,7 +18,7 @@ module FStar.GhostSet
 (** Ghost computational sets: membership is a ghost boolean function *)
 #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"
 
-[@@must_erase_for_extraction; erasable]
+[@@erasable]
 val set (a: Type u#a) : Type u#a
 
 let decide_eq a = x:a -> y:a -> GTot (b:bool { b <==> (x==y) })

ulib/FStar.Monotonic.HyperHeap.fsti

@@ -28,9 +28,9 @@ open FStar.Ghost
  *)
 
 (*
- * AR: mark it must_erase_for_extraction temporarily until CMI comes in
+ * AR: mark it erasable temporarily until CMI comes in
  *)
-[@@must_erase_for_extraction]
+[@@erasable]
 val rid :eqtype
 
 val reveal (r:rid) :GTot (list (int & int))

ulib/FStar.Pervasives.fsti

@@ -867,19 +867,7 @@ val plugin (x: int) : Tot unit
     elaborate and typecheck, but unfold before verification. *)
 val tcnorm : unit
 
-(** We erase all ghost functions and unit-returning pure functions to
-    [()] at extraction. This creates a small issue with abstract
-    types. Consider a module that defines an abstract type [t] whose
-    (internal) definition is [unit] and also defines [f: int -> t]. [f]
-    would be erased to be just [()] inside the module, while the
-    client calls to [f] would not, since [t] is abstract. To get
-    around this, when extracting interfaces, if we encounter an
-    abstract type, we tag it with this attribute, so that
-    extraction can treat it specially.
-
-    Note, since the use of cross-module inlining (the [--cmi] option),
-    this attribute is no longer necessary. We retain it for legacy,
-    but will remove it in the future. *)
+[@@deprecated "use [@@erasable] instead"]
 val must_erase_for_extraction : unit
 
 (** This attribute is used with the Dijkstra Monads for Free

ulib/FStar.TSet.fst

@@ -22,7 +22,7 @@ module P = FStar.PropositionalExtensionality
 module F = FStar.FunctionalExtensionality
 
 (*
- * AR: mark it must_erase_for_extraction temporarily until CMI comes in
+ * AR: mark it erasable temporarily until CMI comes in
  *)
 [@@erasable]
 let set a = F.restricted_t a (fun _ -> prop)

ulib/FStar.TSet.fsti

@@ -20,9 +20,9 @@ module FStar.TSet
 #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"
 
 (*
- * AR: mark it must_erase_for_extraction temporarily until CMI comes in
+ * AR: mark it erasable temporarily until CMI comes in
  *)
-[@@must_erase_for_extraction; erasable]
+[@@erasable]
 val set (a:Type u#a) : Type u#(max 1 a)
 
 val equal (#a:Type) (s1:set a) (s2:set a) : prop