Merge pull request #3356 from FStarLang/nik_3353

Adding a missing simplifcation rule

src/typechecker/FStar.TypeChecker.Normalize.fst

@@ -2360,7 +2360,9 @@ and maybe_simplify_aux (cfg:cfg) (env:env) (stack:stack) (tm:term) : term & bool
     match (SS.compress tm).n with
     | Tm_app {hd={n=Tm_uinst({n=Tm_fvar fv}, _)}; args}
     | Tm_app {hd={n=Tm_fvar fv}; args} ->
-      if S.fv_eq_lid fv PC.and_lid
+      if S.fv_eq_lid fv PC.squash_lid
+      then squashed_head_un_auto_squash_args tm
+      else if S.fv_eq_lid fv PC.and_lid
       then match args |> List.map simplify with
            | [(Some true, _); (_, (arg, _))]
            | [(_, (arg, _)); (Some true, _)] -> maybe_auto_squash arg, false

src/typechecker/FStar.TypeChecker.TermEqAndSimplify.fst

@@ -389,7 +389,9 @@ let simplify (debug:bool) (env:env_t) (tm:term) : term =
     match (SS.compress tm).n with
     | Tm_app {hd={n=Tm_uinst({n=Tm_fvar fv}, _)}; args}
     | Tm_app {hd={n=Tm_fvar fv}; args} ->
-      if S.fv_eq_lid fv PC.and_lid
+      if S.fv_eq_lid fv PC.squash_lid
+      then squashed_head_un_auto_squash_args tm
+      else if S.fv_eq_lid fv PC.and_lid
       then match args |> List.map simplify with
            | [(Some true, _); (_, (arg, _))]
            | [(_, (arg, _)); (Some true, _)] -> maybe_auto_squash arg

tests/bug-reports/Bug3353.fst

@@ -0,0 +1,31 @@
+module Bug3353
+
+// true when all elements of a list satisfy a predicate
+let rec for_allP (#a:Type) (pre:a -> prop) (l:list a): prop =
+  match l with
+  | [] -> True
+  | h::t -> pre h /\ for_allP pre t
+
+
+// a type, a predicate on that type, and some values
+assume val ty: Type0
+assume val pre: ty -> prop
+
+assume val v1: ty
+assume val v2: ty
+assume val v3: ty
+
+// Given a list of values...
+let all_v = [ v1 ]
+
+// ... we define this subtle squashed type...
+assume val all_v_pre: squash (norm [delta_only [`%all_v; `%for_allP]; iota; zeta] (for_allP pre all_v))
+
+#push-options "--fuel 0 --ifuel 0"
+let test () =
+  // ... to have `pre ...` in the global scope, with no fuel. Hooray!
+  assert(pre v1)
+
+assume val p : Type0
+let test2 (x : squash (p /\ True)) : squash p = ()
+

tests/bug-reports/Makefile

@@ -79,8 +79,9 @@ SHOULD_VERIFY_CLOSED=\
 	Bug3213.fst Bug3213b.fst Bug3207.fst Bug3207b.fst Bug3207c.fst			\
 	Bug2155.fst Bug3224a.fst Bug3224b.fst Bug3236.fst Bug3252.fst \
 	BugBoxInjectivity.fst BugTypeParamProjector.fst Bug2172.fst Bug3266.fst		\
-	Bug3264a.fst Bug3264b.fst Bug3286a.fst Bug3286b.fst Bug3320.fst Bug2583.fst	\
-	Bug2419.fst
+	Bug3264a.fst Bug3264b.fst Bug3286a.fst Bug3286b.fst Bug3320.fst Bug2583.fst \
+	Bug2419.fst Bug3353.fst
+
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst