Erase functions to functions instead of unit.

This only works if extraction can see through the type definitions,
in general this requires `--cmi`.

Fixes #3366

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
+
 let rec translate_term_to_mlty (g:uenv) (t0:term) : mlty =
     let arg_as_mlty (g:uenv) (a, _) : mlty =
         if is_type g a //This is just an optimization; we could in principle always emit MLTY_Erased, at the expense of more magics
@@ -743,6 +752,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*)
@@ -801,12 +813,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 =
@@ -1207,7 +1221,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
@@ -1485,13 +1499,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

@@ -1022,20 +1022,36 @@ 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_abs {body} -> non_informative env body
+    // | 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_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 a non-function.
+        Some unit_const
+      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
+      // (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
+    | _ -> None
 
 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,9 +342,9 @@ 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
+(* `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
 
 val try_lookup_effect_lid  : env -> lident -> option term
 val lookup_effect_lid      : env -> lident -> term

src/typechecker/FStarC.TypeChecker.Normalize.fst

@@ -1426,38 +1426,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
@@ -2832,7 +2836,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,7 @@ 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
 
 (*
  * The maybe versions of ghost_to_pure only promote

src/typechecker/FStarC.TypeChecker.Quals.fst

@@ -211,7 +211,7 @@ let check_erasable env quals (r:Range.range) se =
         | 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 [
+      if has_iface_val && Some? (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"
@@ -235,7 +235,7 @@ let check_erasable env quals (r:Range.range) se =
 
     | Sig_let {lbs=(false, [lb])} ->
       let _, body, _ = U.abs_formals lb.lbdef in
-      if not (N.non_info_norm env body)
+      if None? (N.non_info_norm env body)
       then raise_error body Errors.Fatal_QulifierListNotPermitted [
                   text "Illegal attribute: \
                    the `erasable` attribute is only permitted on inductive type definitions \

src/typechecker/FStarC.TypeChecker.Rel.fst

@@ -4550,7 +4550,7 @@ and solve_c (problem:problem comp) (wl:worklist) : solution =
             if is_polymonadic &&
                Env.is_erasable_effect env c1.effect_name &&
                not (Env.is_erasable_effect env c2.effect_name) &&
-               not (N.non_info_norm env c1.result_typ)
+               None? (N.non_info_norm env c1.result_typ)
             then Errors.raise_error r Errors.Error_TypeError
                                      (BU.format3 "Cannot lift erasable expression from %s ~> %s since its type %s is informative"
                                        (string_of_lid c1.effect_name)
@@ -4729,7 +4729,7 @@ and solve_c (problem:problem comp) (wl:worklist) : solution =
            else N.ghost_to_pure2 env (c1, c2) in
 
          match c1.n, c2.n with
-         | GTotal t1, Total t2 when (Env.non_informative env t2) ->
+         | GTotal t1, Total t2 when Some? (Env.non_informative env t2) ->
            solve_t (problem_using_guard orig t1 problem.relation t2 None "result type") wl
 
          | GTotal _, Total _ ->

src/typechecker/FStarC.TypeChecker.TcEffect.fst

@@ -1928,7 +1928,7 @@ Errors.with_ctx (BU.format1 "While checking layered effect definition `%s`" (str
         let env = Env.push_univ_vars env0 us in
         let env = Env.push_binders env [a_b] in
         let _, r = List.fold_left (fun (env, r) b ->
-          let r = r && N.non_info_norm env b.binder_bv.sort in
+          let r = r && Some? (N.non_info_norm env b.binder_bv.sort) in
           Env.push_binders env [b], r) (env, true) rest_bs in
         if r &&
            Substitutive_combinator? bind_kind &&

src/typechecker/FStarC.TypeChecker.TcTerm.fst

@@ -178,7 +178,7 @@ let check_erasable_binder_attributes env attrs (binder_ty:typ) =
     List.iter
       (fun attr ->
         if U.is_fvar Const.erasable_attr attr
-        && not (N.non_info_norm env binder_ty)
+        && None? (N.non_info_norm env binder_ty)
         then raise_error attr Errors.Fatal_QulifierListNotPermitted
                 ("Incompatible attributes:  an erasable attribute on a binder must bind a name at an non-informative type"))
 
@@ -2683,7 +2683,7 @@ and check_application_args env head (chead:comp) ghead args expected_topt : term
                    //this argument is effectful, warn if the function would be erased
                    //special casing for ignore, may be use an attribute instead?
                    let warn_effectful_args  =
-                     (TcUtil.must_erase_for_extraction env chead.res_typ) &&
+                     Some? (TcUtil.must_erase_for_extraction env chead.res_typ) &&
                      (not (match (U.un_uinst head).n with
                            | Tm_fvar fv -> S.fv_eq_lid fv (Parser.Const.psconst "ignore")
                            | _ -> true))
@@ -3077,7 +3077,7 @@ and tc_pat env (pat_t:typ) (p0:pat) :
           //Data constructors are marked with the "erasable" attribute
           //if their types are; matching on this constructor incurs
           //a ghost effect
-          let erasable = Env.non_informative env t in
+          let erasable = Some? (Env.non_informative env t) in
           if List.length formals <> List.length args
           then fail "Pattern is not a fully-applied data constructor";
           let rec aux (subst, args_out, bvs, guard) formals args =
@@ -4732,7 +4732,7 @@ let tc_tparams env0 (tps:binders) : (binders & Env.env & universes) =
 
 let rec __typeof_tot_or_gtot_term_fastpath (env:env) (t:term) (must_tot:bool) : option typ =
   let mk_tm_type u = S.mk (Tm_type u) t.pos in
-  let effect_ok k = (not must_tot) || (N.non_info_norm env k) in
+  let effect_ok k = (not must_tot) || Some? (N.non_info_norm env k) in
   let t = SS.compress t in
   match t.n with
   | Tm_delayed _
@@ -4822,7 +4822,7 @@ let rec __typeof_tot_or_gtot_term_fastpath (env:env) (t:term) (must_tot:bool) :
     let k = U.comp_result c in
     if (not must_tot) ||
        (c |> U.comp_effect_name |> Env.norm_eff_name env |> lid_equals Const.effect_PURE_lid) ||
-       (N.non_info_norm env k)
+       Some? (N.non_info_norm env k)
     then Some k
     else None
 

src/typechecker/FStarC.TypeChecker.Util.fst

@@ -1188,10 +1188,10 @@ let mk_indexed_bind env
 
   if (Env.is_erasable_effect env m &&
       not (Env.is_erasable_effect env p) &&
-      not (N.non_info_norm env ct1.result_typ)) ||
+      None? (N.non_info_norm env ct1.result_typ)) ||
      (Env.is_erasable_effect env n &&
       not (Env.is_erasable_effect env p) &&
-      not (N.non_info_norm env ct2.result_typ))
+      None? (N.non_info_norm env ct2.result_typ))
   then raise_error r1 Errors.Fatal_UnexpectedEffect [
            text "Cannot apply bind" ^/^ doc_of_string (bind_name ()) ^/^ text "since" ^/^ pp p
              ^/^ text "is not erasable and one of the computations is informative."
@@ -3191,7 +3191,7 @@ let maybe_add_implicit_binders (env:env) (bs:binders) : binders =
 
 let must_erase_for_extraction (g:env) (t:typ) =
   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);
+  if !dbg_Extraction then BU.print2 "must_erase=%s: %s\n" (show res) (show t);
   res
 
 let effect_extraction_mode env l =
@@ -3267,7 +3267,7 @@ let check_non_informative_type_for_lift env m1 m2 t (r:Range.range) : unit =
   //raise an error if m1 is erasable, m2 is not erasable, and t is informative
   if Env.is_erasable_effect env m1       &&
      not (Env.is_erasable_effect env m2) &&
-     not (N.non_info_norm env t)
+     None? (N.non_info_norm env t)
   then Errors.raise_error r Errors.Error_TypeError
           (BU.format3 "Cannot lift erasable expression from %s ~> %s since its type %s is informative"
             (string_of_lid m1)

src/typechecker/FStarC.TypeChecker.Util.fsti

@@ -147,7 +147,7 @@ val remove_reify: term -> term
 val maybe_lift: env -> term -> lident -> lident -> typ -> term
 val maybe_monadic: env -> term -> lident -> typ -> term
 
-val must_erase_for_extraction: env -> term -> bool
+val must_erase_for_extraction: env -> term -> option term
 
 //layered effect utilities