From bbc0767286397456dd69b28aadd1222f4fdfd936 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 3 May 2024 08:23:08 -0700 Subject: [PATCH 1/4] Add test for #2172 Keeping open as there is a discrepancy between these two, but at least keep the test in CI so we do not regress. --- tests/bug-reports/Bug2172.fst | 12 ++++++++++++ tests/bug-reports/Makefile | 2 +- 2 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 tests/bug-reports/Bug2172.fst diff --git a/tests/bug-reports/Bug2172.fst b/tests/bug-reports/Bug2172.fst new file mode 100644 index 00000000000..055514abb71 --- /dev/null +++ b/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) diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile index ce2246e09d5..a3f690fba6f 100644 --- a/tests/bug-reports/Makefile +++ b/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 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst From b88f5f0fafb90fc31a907607b6298772bf73346e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 3 May 2024 08:28:19 -0700 Subject: [PATCH 2/4] Rel: fix bad environment Fixes #3266 --- src/typechecker/FStar.TypeChecker.Rel.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index f7c077c19bc..ebd3511bb21 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/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 From 053dbe4fabd71901733cb07979ab2a662ef53d0d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 3 May 2024 08:28:47 -0700 Subject: [PATCH 3/4] snap --- ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index dca9b326c23..3b92d872542 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -10635,7 +10635,7 @@ and (solve_t' : tprob -> worklist -> solution) = match uu___14 with | (scope, p) -> FStar_TypeChecker_Env.close_forall - wl2.tcenv scope (p_guard p)) + (p_env wl2 orig) scope (p_guard p)) sub_probs1 in FStar_Syntax_Util.mk_conj_l uu___13 in let tx = FStar_Syntax_Unionfind.new_transaction () in From 955d80f8530282acb61966dbaca771cfafbe8254 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 3 May 2024 08:28:42 -0700 Subject: [PATCH 4/4] Add repro for #3266 --- tests/bug-reports/Bug3266.fst | 22 ++++++++++++++++++++++ tests/bug-reports/Makefile | 2 +- 2 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 tests/bug-reports/Bug3266.fst diff --git a/tests/bug-reports/Bug3266.fst b/tests/bug-reports/Bug3266.fst new file mode 100644 index 00000000000..8427972b7e6 --- /dev/null +++ b/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 +} diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile index a3f690fba6f..77dd01b9a70 100644 --- a/tests/bug-reports/Makefile +++ b/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 Bug2172.fst + BugBoxInjectivity.fst BugTypeParamProjector.fst Bug2172.fst Bug3266.fst SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst