Merge pull request #2736 from FStarLang/guido_2684

Removing bv sorts from checked files

src/syntax/FStar.Syntax.Subst.fst

@@ -826,13 +826,15 @@ let rec deep_compress (t:term) : term =
     | Tm_delayed _ -> failwith "Impossible"
     | Tm_fvar _
     | Tm_constant _
-    (* NOTE: the BVs here contain a sort, but it is not reached
-     * by substitutions, so we do not need to go into it. *)
-    | Tm_bvar _
-    | Tm_name _
     | Tm_unknown ->
         { t with vars = U.mk_ref None }
 
+    (* The sorts are not needed. Delete them. *)
+    | Tm_bvar bv ->
+      mk (Tm_bvar ({bv with sort = mk Tm_unknown}))
+    | Tm_name bv ->
+      mk (Tm_name ({bv with sort = mk Tm_unknown}))
+
     | Tm_uinst (f, us) ->
       let us = List.map deep_compress_univ us in
       mk (Tm_uinst (f, us))

tests/bug-reports/Bug2684a.fst

@@ -0,0 +1,56 @@
+module Bug2684a
+
+class typeclass (ty:Type0) = {
+  meh: unit;
+}
+
+assume val the_ty: Type0
+assume val the_pf: typeclass the_ty
+instance _: typeclass the_ty = the_pf
+
+// No bug if we:
+// - remove `pf` in `t3`
+// - try to remove the parameter of type `t2 p1` in `t3`
+assume val t1: Type0
+assume val t2: t1 -> Type0
+assume val t3: ty:Type0 -> pf:typeclass ty -> p1:t1 -> p2:t2 p1 -> Type0
+
+assume val t4: ty:Type0 -> pf:typeclass ty -> Type0
+
+// No bug if we don't use meta-programmed typeclass instantiation
+assume val t3_to_t4: #ty:Type0 -> {|pf:typeclass ty|} -> #p1:t1 -> #p2:t2 p1 -> t:t3 ty pf p1 p2 -> t4 ty pf
+
+assume val t4_pred: t4 the_ty the_pf -> prop
+assume val dtuple_pred: p1:t1 & p2:t2 p1 & t3 the_ty the_pf p1 p2 -> prop
+// No bug if instead of `nat` we have a `int`
+assume val nat_pred: nat -> prop
+
+//Bug is still there if `n1` has type `int`
+val the_lemma: p1:t1 -> p2:t2 p1 -> t:t3 the_ty the_pf p1 p2 -> n1:nat -> tl:t4 the_ty the_pf -> Lemma
+  (requires t4_pred tl)
+  (ensures True)
+let the_lemma p1 p2 t n1 tl =
+  // No bug if we remove this line, or if we instantiate the typeclass explicitly
+  let _ = t3_to_t4 t in
+  // No bug if we remove this line
+  let (|_, _, _|) = (|p1, p2, t|) in
+
+  // No bug if in the next 3 introduce/eliminate we
+  // - remove `n0 <= n1`
+  // - remove `nat_pred n0`
+  // - replace `dtuple_pred (|p1, p2, t|)` with `True`
+  // - remove one of the eliminates / introduce
+  introduce (exists n0. n0 <= n1 /\ nat_pred n0) ==> dtuple_pred (|p1, p2, t|)
+  with _. (
+    eliminate exists n0. n0 <= n1 /\ nat_pred n0
+    returns dtuple_pred (|p1, p2, t|)
+    with _. (
+      // No bug if we use `nat_pred` or a predicate for a new type
+      // Bug is still there if we use `dtuple_pred` instead of `t4_pred`
+      eliminate exists x. t4_pred x
+      returns dtuple_pred (|p1, p2, t|)
+      with _. (
+        admit()
+      )
+    )
+  )

tests/bug-reports/Bug2684b.fst

@@ -0,0 +1,14 @@
+module Bug2684b
+
+open FStar.Tactics
+
+assume val nat_dep: nat -> Type0
+
+assume val complex_type: ty:Type0 -> (#[exact (`())] _ : unit) -> l:nat -> nat_dep l -> Type0
+
+assume val a_function: #ty:Type0 -> (#[exact (`())] _ : unit) -> #x:nat -> #y:nat_dep x -> z:complex_type ty x y -> x':nat & y':nat_dep x' & complex_type ty x' y'
+
+val a_lemma: #ty:Type0 -> (#[exact (`())] _ : unit) -> #x:nat -> #y:nat_dep x -> z:complex_type ty x y -> unit
+let rec a_lemma #ty #tc #x #y z =
+  let (|_, _, _|) = a_function z in
+  ()

tests/bug-reports/Bug2684c.fst

@@ -0,0 +1,18 @@
+module Bug2684c
+
+open FStar.Tactics
+
+assume
+val nat_dep: nat -> Type0
+
+assume
+val complex_type: ty:Type0 -> (#[exact (`())] _ : unit) -> l:nat -> nat_dep l -> Type0
+
+assume
+val a_function: #ty:Type0 -> (#[exact (`())] _ : unit) -> #x:nat -> #y:nat_dep x -> z:complex_type ty x y -> x':nat & y':nat_dep x' & complex_type ty x' y'
+
+val a_lemma: #ty:Type0 -> (#[exact (`())] _ : unit) -> #x:nat -> #y:nat_dep x -> z:complex_type ty x y -> unit
+let rec a_lemma #ty #tc #x #y z =
+  let r = a_function z in
+  match r with
+  | Mkdtuple3 _ _ _  -> ()

tests/bug-reports/Bug2684d.fst

@@ -0,0 +1,10 @@
+module Bug2684d
+
+open FStar.Tactics
+
+val f : (#[exact (`1)] _ : int) -> Type0
+let f #_ = unit
+
+let elim (d : (y:f & z:unit{y == z} & w:unit{w == z})) : unit =
+  match d with
+  | Mkdtuple3 #_ #_ #_ x y z -> ()

tests/bug-reports/Makefile

@@ -47,7 +47,7 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug
   Bug1418.fst Bug171.fst Bug2496.fst Bug2478.fst Bug2414.fst Bug2515.fst \
   Bug2535.fst Bug2557.fst Bug2572.fst Bug2522.fst Bug2486.fst \
   Bug2552.fst Bug2597.fst Bug2471_B.fst Bug2605.fst Bug2614.fst Bug2622.fst \
-  Bug2637.fst Bug2641.fst Bug1486.fst PropProofs.fst
+  Bug2637.fst Bug2641.fst Bug1486.fst PropProofs.fst Bug2684a.fst Bug2684b.fst Bug2684c.fst Bug2684d.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst
@@ -141,6 +141,11 @@ Bug1383.verify: OTHERFLAGS += --warn_error @275 #Z3 warnings are fatal
 Bug1694.verify: OTHERFLAGS += --codegen OCaml
 Bug2210.verify: OTHERFLAGS += --codegen OCaml
 
+Bug2684a.verify: OTHERFLAGS += --cache_checked_modules
+Bug2684b.verify: OTHERFLAGS += --cache_checked_modules
+Bug2684c.verify: OTHERFLAGS += --cache_checked_modules
+Bug2684d.verify: OTHERFLAGS += --cache_checked_modules
+
 verify: $(subst .fst,.verify,$(SHOULD_VERIFY_CLOSED))
 
 %.iverify: %.fsti