Erase functions to fun

src/extraction/FStarC.Extraction.ML.Modul.fst

@@ -822,7 +822,7 @@ let rec extract_sigelt_iface (g:uenv) (se:sigelt) : uenv & iface =
     | Sig_declare_typ {lid; t} ->
       let quals = se.sigquals in
       if quals |> List.contains Assumption
-      && not (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t)
+      && None? (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t)
       then let g, bindings = Term.extract_lb_iface g (false, [always_fail lid t]) in
            g, iface_of_bindings bindings
       else g, empty_iface //it's not assumed, so wait for the corresponding Sig_let to generate code
@@ -999,7 +999,7 @@ let extract_bundle env se =
     | _ -> failwith "Unexpected signature element"
 
 let lb_is_irrelevant (g:env_t) (lb:letbinding) : bool =
-  Env.non_informative (tcenv_of_uenv g) lb.lbtyp && // result type is non informative
+  Some? (Env.non_informative (tcenv_of_uenv g) lb.lbtyp) && // result type is non informative
   not (Term.is_arity g lb.lbtyp) &&  // but not a type definition
   U.is_pure_or_ghost_effect lb.lbeff // and not top-level effectful
 
@@ -1129,7 +1129,7 @@ let rec extract_sig (g:env_t) (se:sigelt) : env_t & list mlmodule1 =
     | Sig_declare_typ {lid; t} ->
       let quals = se.sigquals in
       if quals |> List.contains Assumption
-      && not (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t)
+      && None? (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t)
       then let always_fail =
              { se with sigel = Sig_let {lbs=(false, [always_fail lid t]); lids=[]} } in
            let g, mlm = extract_sig g always_fail in //extend the scope with the new name

src/extraction/FStarC.Extraction.ML.Term.fst

@@ -689,6 +689,15 @@ let head_of_type_is_extract_as_impure_effect g t =
   | Tm_fvar fv -> has_extract_as_impure_effect g fv
   | _ -> false
 
+let ty_of_must_erase (g: uenv) (t: term) =
+  let rec go t =
+    match t.n with
+    | Tm_abs {bs;body} -> {t with n=Tm_arrow {bs; comp=mk_Total (go body)}}
+    | Tm_constant Const_unit -> t_unit in
+  match TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t with
+  | Some r -> Some (go r)
+  | None -> None
+
 exception NotSupportedByExtension
 let translate_typ_t = g:uenv -> t:term -> mlty
 
@@ -762,6 +771,9 @@ let rec translate_term_to_mlty' (g:uenv) (t0:term) : mlty =
           | Tm_name bv ->
             bv_as_mlty env bv
 
+          | Tm_fvar fv when fv_eq_lid fv PC.unit_lid ->
+            MLTY_Erased
+
           | Tm_fvar fv ->
             (* it is not clear whether description in the thesis covers type applications with 0 args.
                However, this case is needed to translate types like nnat, and so far seems to work as expected*)
@@ -820,12 +832,14 @@ let rec translate_term_to_mlty' (g:uenv) (t0:term) : mlty =
           end
         | _ -> false
     in
-    if TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t0
-    then MLTY_Erased
-    else let mlt = aux g t0 in
-         if is_top_ty mlt
-         then MLTY_Top
-         else mlt
+    let t0 =
+      match ty_of_must_erase g t0 with
+      | Some repl -> repl
+      | None -> t0 in
+    let mlt = aux g t0 in
+    if is_top_ty mlt
+    then MLTY_Top
+    else mlt
 
 
 and binders_as_ml_binders (g:uenv) (bs:binders) : list (mlident & mlty) & uenv =
@@ -1239,7 +1253,7 @@ let rec extract_lb_sig (g:uenv) (lbs:letbindings) : list lb_sig =
                   let expected_t = term_as_mlty g lbtyp in
                   (lbname_, f_e, (lbtyp, ([], ([],expected_t))), false, has_c_inline, lbdef)
               in
-              if TcUtil.must_erase_for_extraction (tcenv_of_uenv g) lbtyp
+              if Some? (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) lbtyp)
               then (lbname_, f_e, (lbtyp, ([], ([], MLTY_Erased))), false, has_c_inline, lbdef)
               else  //              debug g (fun () -> printfn "Let %s at type %s; expected effect is %A\n" (show lbname) (Print.typ_to_string t) f_e);
                 match lbtyp.n with
@@ -1517,13 +1531,18 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr & e_tag & mlty) =
         | Tm_uinst(t, _) ->
           term_as_mlexpr g t
 
+        | Tm_constant Const_unit ->
+          ml_unit, E_PURE, MLTY_Erased
+
         | Tm_constant c ->
           let tcenv = tcenv_of_uenv g in
           let _, ty, _ = TcTerm.typeof_tot_or_gtot_term tcenv t true in  //AR: TODO: type_of_well_typed?
-          if TcUtil.must_erase_for_extraction tcenv ty
-          then ml_unit, E_PURE, MLTY_Erased
-          else let ml_ty = term_as_mlty g ty in
-               with_ty ml_ty (mlexpr_of_const t.pos c), E_PURE, ml_ty
+          (match TcUtil.must_erase_for_extraction tcenv ty with
+          | Some repl ->
+            term_as_mlexpr g repl
+          | None ->
+            let ml_ty = term_as_mlty g ty in
+            with_ty ml_ty (mlexpr_of_const t.pos c), E_PURE, ml_ty)
 
         | Tm_name _ -> //lookup in g; decide if its in left or right; tag is Pure because it's just a variable
           if is_type g t //Here, we really need to be certain that g is a type; unclear if level ensures it

src/typechecker/FStarC.TypeChecker.Core.fst

@@ -670,7 +670,7 @@ let rec iter2 (xs ys:list 'a) (f: 'a -> 'a -> 'b -> result 'b) (b:'b)
       iter2 xs ys f b
     | _ -> fail "Lists of differing length"
 
-let is_non_informative g t = N.non_info_norm g t
+let is_non_informative g t = Some? (N.non_info_norm g t)
 
 let non_informative g t
   : bool

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
 
@@ -1027,18 +1022,46 @@ let is_erasable_effect env l =
 
 let rec non_informative env t =
     match (U.unrefine t).n with
-    | Tm_type _ -> true
-    | Tm_fvar fv ->
-      fv_eq_lid fv Const.unit_lid
-      || fv_eq_lid fv Const.squash_lid
-      || fv_eq_lid fv Const.erased_lid
-      || fv_has_erasable_attr env fv
+    | Tm_type _ -> Some unit_const
+    | Tm_fvar fv when 
+           fv_eq_lid fv Const.unit_lid
+        || fv_eq_lid fv Const.squash_lid
+        || fv_eq_lid fv Const.erased_lid ->
+      Some unit_const
+    | Tm_fvar fv when fv_has_erasable_attr env fv ->
+      // Note: this is unsound (see #3366), but only happens when we compile without `--cmi`.
+      Some unit_const
     | Tm_app {hd=head} -> non_informative env head
     | 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)
-    | _ -> false
+    | Tm_arrow {bs;comp=c} ->
+      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.
+        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)
+        match non_informative env (comp_result c) with
+        | Some body -> Some (mk (Tm_abs { body; rc_opt = None; bs }) t.pos)
+        | None -> None
+      else
+        // Effectful computations may not be erased
+        None
+    | Tm_meta {tm} -> non_informative env tm
+    | _ -> None
+
+let rec non_informative_sort t =
+  match (U.unrefine t).n with
+  | Tm_fvar fv when fv_eq_lid fv Const.prop_lid -> true
+  | Tm_arrow {comp=c} -> non_informative_sort (comp_result c)
+  | Tm_meta {tm} -> non_informative_sort tm
+  | _ -> false
 
 let num_effect_indices env name r =
   let sig_t = name |> lookup_effect_lid env |> SS.compress in

src/typechecker/FStarC.TypeChecker.Env.fsti

@@ -342,7 +342,16 @@ 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
-val non_informative        : env -> typ -> bool
+
+(* `non_informative env t` is `Some i` if the type `t: Type` is noninformative,
+   and any `x: t ...` can be erased to `i`. *)
+val non_informative        : env -> typ -> option term
+
+(* `non_informative_sort t` is `true` if the type family `t: ... -> Type` only ranges over noninformative types,
+   i.e., any `x: s ...` such that `s ... : t ...` can be erased.
+   (practically, this means that `t` is of the form `... -> prop`) *)
+val non_informative_sort   : 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

@@ -1434,38 +1434,42 @@ let rec norm : cfg -> env -> stack -> term -> term =
             log cfg (fun () -> BU.print1 ">> metadata = %s\n" (show m));
             begin match m with
               | Meta_monadic (m_from, ty) ->
+                let nonerasable_case () =
+                  reduce_impure_comp cfg env stack head (Inl m_from) ty in
                 if cfg.steps.for_extraction
                 then (
                   //In Extraction, we want to erase sub-terms with erasable effect
-                  //Or pure terms with non-informative return types
-                  if Env.is_erasable_effect cfg.tcenv m_from
-                  || (U.is_pure_effect m_from && Env.non_informative cfg.tcenv ty)
-                  then (
+                  if Env.is_erasable_effect cfg.tcenv m_from then
                     rebuild cfg env stack (S.mk (Tm_meta {tm=U.exp_unit; meta=m}) t.pos)
-                  )
-                  else (
-                    reduce_impure_comp cfg env stack head (Inl m_from) ty
-                  )
+                  //Or pure terms with non-informative return types
+                  else if not (U.is_pure_effect m_from) then
+                    nonerasable_case ()
+                  else match Env.non_informative cfg.tcenv ty with
+                    | None -> nonerasable_case ()
+                    | Some tm ->
+                      rebuild cfg env stack (S.mk (Tm_meta {tm; meta=m}) t.pos)
                 )
-                else 
-                  reduce_impure_comp cfg env stack head (Inl m_from) ty
+                else
+                  nonerasable_case ()
 
               | Meta_monadic_lift (m_from, m_to, ty) ->
+                let nonerasable_case () =
+                  reduce_impure_comp cfg env stack head (Inr (m_from, m_to)) ty in
                 if cfg.steps.for_extraction
                 then (
                   //In Extraction, we want to erase sub-terms with erasable effect
-                  //Or pure terms with non-informative return types
-                  if Env.is_erasable_effect cfg.tcenv m_from
-                  ||  Env.is_erasable_effect cfg.tcenv m_to
-                  || (U.is_pure_effect m_from && Env.non_informative cfg.tcenv ty)
-                  then (
+                  if Env.is_erasable_effect cfg.tcenv m_from || Env.is_erasable_effect cfg.tcenv m_to then
                     rebuild cfg env stack (S.mk (Tm_meta {tm=U.exp_unit; meta=m}) t.pos)
-                  )
-                  else (
-                    reduce_impure_comp cfg env stack head (Inr (m_from, m_to)) ty
-                  )
+                  //Or pure terms with non-informative return types
+                  else if not (U.is_pure_effect m_from) then
+                    nonerasable_case ()
+                  else match Env.non_informative cfg.tcenv ty with
+                    | None -> nonerasable_case ()
+                    | Some tm ->
+                      rebuild cfg env stack (S.mk (Tm_meta {tm; meta=m}) t.pos)
                 )
-                else reduce_impure_comp cfg env stack head (Inr (m_from, m_to)) ty
+                else
+                  nonerasable_case ()
 
               | _ ->
                 if cfg.steps.unmeta
@@ -2816,6 +2820,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. *)
@@ -2825,6 +2831,21 @@ let non_info_norm env t =
   in
   non_informative env (normalize steps env t)
 
+let non_info_sort_norm env t =
+  let steps = [UnfoldUntil (Env.delta_depth_of_fv env (S.fvconst PC.prop_lid)); // do not unfold prop
+               AllowUnboundUniverses;
+               EraseUniverses;
+               Primops;
+               Beta; Iota;
+               HNF;
+               (* We could use Weak too were it not that we need
+                * to descend in the codomain of arrows. *)
+               Unascribe;   //remove ascriptions
+               ForExtraction //and refinement types
+               ]
+  in
+  non_informative_sort (normalize steps env t)
+
 (*
  * Ghost T to Pure T promotion
  *
@@ -2838,7 +2859,7 @@ let non_info_norm env t =
  *)
 
 let maybe_promote_t env non_informative_only t =
-  not non_informative_only || non_info_norm env t
+  not non_informative_only || Some? (non_info_norm env t)
 
 let ghost_to_pure_aux env non_informative_only c =
     match c.n with

src/typechecker/FStarC.TypeChecker.Normalize.fsti

@@ -34,7 +34,8 @@ val whnf_steps: list step
 val unfold_whnf':         steps -> Env.env -> term -> term
 val unfold_whnf:          Env.env -> term -> term
 val reduce_uvar_solutions:Env.env -> term -> term
-val non_info_norm: Env.env -> term -> bool
+val non_info_norm: Env.env -> term -> option term
+val non_info_sort_norm: Env.env -> term -> bool
 
 (*
  * The maybe versions of ghost_to_pure only promote