From 292723c76a04a26a10f27361b95d7717d405bed7 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 9 Jan 2025 19:05:45 -0800
Subject: [PATCH] Suppress erasable warning for props.

---
 src/typechecker/FStarC.TypeChecker.Env.fst    |  7 +++++++
 src/typechecker/FStarC.TypeChecker.Env.fsti   |  5 +++++
 .../FStarC.TypeChecker.Normalize.fst          | 15 +++++++++++++
 .../FStarC.TypeChecker.Normalize.fsti         |  1 +
 src/typechecker/FStarC.TypeChecker.Quals.fst  | 21 ++++++++++++-------
 5 files changed, 42 insertions(+), 7 deletions(-)

diff --git a/src/typechecker/FStarC.TypeChecker.Env.fst b/src/typechecker/FStarC.TypeChecker.Env.fst
index fdbe934d36f..a648f4a1a99 100644
--- a/src/typechecker/FStarC.TypeChecker.Env.fst
+++ b/src/typechecker/FStarC.TypeChecker.Env.fst
@@ -1056,6 +1056,13 @@ let rec non_informative env t =
     | 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
   match sig_t.n with
diff --git a/src/typechecker/FStarC.TypeChecker.Env.fsti b/src/typechecker/FStarC.TypeChecker.Env.fsti
index 18977ca95e8..706803ea477 100644
--- a/src/typechecker/FStarC.TypeChecker.Env.fsti
+++ b/src/typechecker/FStarC.TypeChecker.Env.fsti
@@ -346,6 +346,11 @@ val fv_has_erasable_attr   : env -> fv -> bool
    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)
diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fst b/src/typechecker/FStarC.TypeChecker.Normalize.fst
index 530a90e2068..53ce3ee1d78 100644
--- a/src/typechecker/FStarC.TypeChecker.Normalize.fst
+++ b/src/typechecker/FStarC.TypeChecker.Normalize.fst
@@ -2821,6 +2821,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
  *
diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fsti b/src/typechecker/FStarC.TypeChecker.Normalize.fsti
index 163e0770339..6c11179a83a 100644
--- a/src/typechecker/FStarC.TypeChecker.Normalize.fsti
+++ b/src/typechecker/FStarC.TypeChecker.Normalize.fsti
@@ -35,6 +35,7 @@ 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 -> option term
+val non_info_sort_norm: Env.env -> term -> bool
 
 (*
  * The maybe versions of ghost_to_pure only promote
diff --git a/src/typechecker/FStarC.TypeChecker.Quals.fst b/src/typechecker/FStarC.TypeChecker.Quals.fst
index f10d456b067..c930f87653d 100644
--- a/src/typechecker/FStarC.TypeChecker.Quals.fst
+++ b/src/typechecker/FStarC.TypeChecker.Quals.fst
@@ -210,13 +210,20 @@ let check_erasable env quals (r:Range.range) se =
       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 && Some? (non_info_norm_weak env body) then log_issue lbname Error_MustEraseMissing [
-        text (BU.format1 "Values of type `%s` will be erased during extraction, \
-              but its interface hides this fact." (show lbname));
-        text (BU.format1 "Add the `erasable` \
-              attribute to the `val %s` declaration for this symbol in the interface" (show lbname));
-      ]
+      let val_decl = Env.try_lookup_val_decl env lbname.fv_name.v in
+      if has_iface_val && Some? val_decl then
+        let _, body, _ = U.abs_formals lb.lbdef in
+          let Some ((us, t), _) = val_decl in
+        let known_to_be_erasable =
+          let env = Env.push_univ_vars env us in
+          N.non_info_sort_norm env t in
+        if not known_to_be_erasable && Some? (non_info_norm_weak env body) then
+          log_issue lbname Error_MustEraseMissing [
+            text (BU.format1 "Values of type `%s` will be erased during extraction, \
+                  but its interface hides this fact." (show lbname));
+            text (BU.format1 "Add the `erasable` \
+                  attribute to the `val %s` declaration for this symbol in the interface" (show lbname));
+          ]
     | _ -> ()
   end;
   if se_has_erasable_attr