Fix #3266

src/typechecker/FStar.TypeChecker.Rel.fst

@@ -4194,7 +4194,7 @@ and solve_t' (problem:tprob) (wl:worklist) : solution =
         | Some (sub_probs, wl) ->
             let sc_prob, wl = mk_t_problem wl [] orig s1 EQ s2 None "match scrutinee" in
             let sub_probs = ([], sc_prob)::sub_probs in
-            let formula = U.mk_conj_l (List.map (fun (scope, p) -> close_forall wl.tcenv scope (p_guard p)) sub_probs) in
+            let formula = U.mk_conj_l (List.map (fun (scope, p) -> close_forall (p_env wl orig) scope (p_guard p)) sub_probs) in
             let tx = UF.new_transaction () in
             let wl = solve_prob orig (Some formula) [] wl in
             begin match solve (attempt (List.map snd sub_probs) ({wl with smt_ok = false})) with

tests/bug-reports/Bug2172.fst

@@ -0,0 +1,12 @@
+module Bug2172
+
+// one existential quantification over two variables (`p2` below) is
+// different from two extistential quantifications over one variable
+// each (`p1` below)
+
+let p1 = exists (x: int). exists (y: int). 0 == x + y
+let p2 = exists (x: int)         (y: int). 0 == x + y
+
+let _ = assert p1
+let _ = assert p2
+let _ = assert (p1 <==> p2)

tests/bug-reports/Bug3266.fst

@@ -0,0 +1,22 @@
+module Bug3266
+
+assume
+val s : Type0
+let st (a:Type) : Type = a & s
+
+let functor_laws
+  (map : (a:_ -> st a -> unit))
+  = unit
+
+noeq
+type functor = {
+  map : a:Type -> st a -> unit;
+  laws : functor_laws map;
+}
+
+#set-options "--defensive abort"
+
+let ff : functor = {
+    map = (fun a (stf: st a) -> let x, s1 = stf in ()); //if you remove the pattern matching on stf then no error is reported
+    laws = admit () //if you remove the admit here, again no error
+}

tests/bug-reports/Makefile

@@ -78,7 +78,7 @@ SHOULD_VERIFY_CLOSED=\
 	Bug3120a.fst Bug3120b.fst Bug3186.fst Bug3185.fst Bug3210.fst			\
 	Bug3213.fst Bug3213b.fst Bug3207.fst Bug3207b.fst Bug3207c.fst			\
 	Bug2155.fst Bug3224a.fst Bug3224b.fst Bug3236.fst Bug3252.fst \
-  BugBoxInjectivity.fst BugTypeParamProjector.fst
+	BugBoxInjectivity.fst BugTypeParamProjector.fst Bug2172.fst Bug3266.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst