Using core typechecker for indexed effects unification solutions #2760

aseemr · 2022-11-16T10:01:31Z

Overview

This PR fixes the "lax" typechecking of implicits introduced for applying indexed effects combinators. As with all the other implicits solved in the unifier, these implicits are core typechecked now. This has been a longstanding known issue in the typechecker.

The PR also introduces a notion of substitutive indexed effects. The combinators for these effects are applied plainly by substitution, no unification, and hence, no additional typing and smt obligations from checking unification solutions.

See https://github.com/FStarLang/FStar/wiki/Indexed-effects for more details.

Impact on the client code

In general, the client code that uses indexed effects is subject to more typechecking with this PR.

However, we found that most of the effects (in ulib, examples/layeredeffects, etc.) can be made substitutive, and hence, don't need to pay this extra typechecking cost. If anything, they don't need to use unification now, which should be good for performance.

One tricky effect was the LowParse writer effect in example/layeredeffects and also in the EverParse repo. In this effect, the memory invariant index of the effect is treated differently in subcomp and other combinators. In subcomp, the index is allowed to vary between the two computations, whereas in all other combinators, the two computations are required to have the same invariant. The fix is to roughly make bind substitutive, but have a _ : squash (inv_f == inv_g) binder whose proof is dispatched to a tactic, which simply does trefl. See the example for more details.

There is no impact on the code that does not use indexed effects.

Backward compatibility

To maintain backward compatibility, the PR adds a new flag --compat_pre_typed_indexed_effects. If this flag is specified, then the implicits for applying indexed effects combinators are "lax" as before.

We are using this flag for the Steel code in ulib and examples.

Relation to #2659

This PR partially fixes #2659. There is a testcase in the PR (in tests/bug-reports/) that adapts the example in the bug report.

What remains to completely fix the bug, is a way for F* to reject degenerate effects (e.g. the effects in #2659 have their representation just as unit, which means, they are able to drop all the guards when lifting from PURE).

aseemr · 2022-11-17T12:15:44Z

examples/layeredeffects/ID1.fst

@@ -226,7 +203,6 @@ let tot_i #a (f : unit -> Tot a) : I a =
 let i_tot #a (f : unit -> I a) : Tot a =
  reify (f ()) (fun _ -> True) ()

-[@@expect_failure [19]]


This used to fail earlier due to unifier generating smt guards when applying indexed effects combinators. E.g. f #t e =?= f #(x:t{phi}) e, which resulted in a forall (x:t). phi guard that was unprovable. With substitutive indexed effects, all of this doesn't come up.

There are many such instances where I could remove the expected_failure attribute.

examples/steel/Makefile

aseemr · 2022-11-17T15:43:17Z

src/syntax/FStar.Syntax.Syntax.fsti

-  l_subcomp      : (tscheme * tscheme);
-  l_if_then_else : (tscheme * tscheme);
-
+  l_bind         : (tscheme * tscheme * option indexed_effect_combinator_kind);


Indexed effect combinators maintain their kinds (substitutive or ad_hoc) (kinds are inferred in TcEffect at the time of typechecking the indexed effect.

aseemr · 2022-11-17T15:44:45Z

src/syntax/FStar.Syntax.Syntax.fsti

 type eff_combinators =
  | Primitive_eff of wp_eff_combinators
  | DM4F_eff of wp_eff_combinators
  | Layered_eff of layered_eff_combinators

+type effect_signature =
+  | Layered_eff_sig of int & tscheme  // (n, ts) where n is the number of effect parameters (all upfront) in the effect signature


Indexed effect signature also maintains the number of binders in the signature that are effect parameters. This is determined by an attribute effect_param marked in the effect signature definition. ToSyntax fills in this int in the AST, and strips off the effect_param attribute, so it is not used in the rest of the typechecker afterwards.

aseemr · 2022-11-17T15:45:05Z

src/syntax/FStar.Syntax.Syntax.fsti

@@ -533,8 +555,8 @@ type sigelt' =
  | Sig_pragma            of pragma
  | Sig_splice            of list lident * term

-  | Sig_polymonadic_bind  of lident * lident * lident * tscheme * tscheme  //(m, n) |> p, the polymonadic term, and its type
-  | Sig_polymonadic_subcomp of lident * lident * tscheme * tscheme  //m <: n, the polymonadic subcomp term, and its type
+  | Sig_polymonadic_bind  of lident * lident * lident * tscheme * tscheme * option indexed_effect_combinator_kind  //(m, n) |> p, the polymonadic term, and its type


Combinator kind in polymonadic bind and subcomp as well.

aseemr · 2022-11-17T15:47:35Z

src/tactics/FStar.Tactics.Basic.fst

@@ -585,6 +584,7 @@ let __tc_ghost (e : env) (t : term) : tac (term * typ * guard_t) =
    bind get (fun ps ->
    mlog (fun () -> BU.print1 "Tac> __tc_ghost(%s)\n" (Print.term_to_string t)) (fun () ->
    let e = {e with uvar_subtyping=false} in
+    let e = {e with letrecs=[]} in


In some examples, the tactic was invoked in the context of a recursive function and had env.letrecs set, and then tactic called back into the typechecker with the same env, resulting in letrecs is set but missing type annotations error.

aseemr · 2022-11-17T15:47:59Z

src/tosyntax/FStar.ToSyntax.ToSyntax.fst

+        let to_comb (us, t) = (us, t), dummy_tscheme, None in
+
+
+        let eff_t, num_effect_params =


Setting the number of effect parameters in the effect signature.

aseemr · 2022-11-17T15:49:56Z

src/typechecker/FStar.TypeChecker.Env.fst

@@ -1814,37 +1816,11 @@ let new_implicit_var_aux reason r env k should_check meta =

 (***************************************************)

-(*


No more tedious explanations about using Allow_untyped here.

aseemr · 2022-11-17T15:50:16Z

src/typechecker/FStar.TypeChecker.Env.fst

      | _ -> None in

    let t, l_ctx_uvars, g_t = new_implicit_var_aux
-      (reason b) r env sort (Allow_untyped "layered effects binder") ctx_uvar_meta_t in
+      (reason b) r env sort
+      (if Options.compat_pre_typed_indexed_effects ()


Use Strict unless the compat flag is set.

aseemr · 2022-11-17T15:51:21Z

src/typechecker/FStar.TypeChecker.Rel.fst

-             (Env.all_binders env) t
-             (U.ctx_uvar_should_check u)
-             u.ctx_uvar_meta
+  let env = {wl.tcenv with gamma = u.ctx_uvar_gamma } in


Only formatting.

aseemr · 2022-11-17T15:52:20Z

src/typechecker/FStar.TypeChecker.Rel.fst

+//
+// returns the (subcomp guard, new sub problems, worklist)
+//
+let apply_substitutive_indexed_subcomp (env:Env.env)


Applying a substitutive indexed effect subcomp. It mainly computes substitutions for the combinator binders.

aseemr · 2022-11-17T15:54:38Z

src/typechecker/FStar.TypeChecker.TcEffect.fst

- * Essentially we want to ensure that uvars are not introduces at a type different than
- *   what they are used at
- *)
-let check_no_subtyping_for_layered_combinator env (t:term) (k:option typ) =


With proper typechecking of the indexed effect combinator binders, we don't need all this no subtype typechecking and eqtype_as_type business.

aseemr · 2022-11-17T15:58:29Z

src/typechecker/FStar.TypeChecker.TcTerm.fst

+                  then Env.conj_guard (Rel.discharge_guard env g_env)
+                                      (Rel.discharge_guard envbody guard_body)
+                  else
+                    let g_env, g_env_logical = TcComm.split_guard g_env in


This is a minor modification to the code that was discharging g_env and g_body separately. Since the implicits in g_env and g_body may depend on each other, we get better mileage if we solve their implicits together and then discharge the two guards.

Note that the env of the two guards are different, but we can still solve their implicits together, since env doesn't matter for them.

aseemr · 2022-11-17T16:00:38Z

src/typechecker/FStar.TypeChecker.Util.fst

@@ -51,7 +51,7 @@ let report env errs =
 (* Unification variables *)
 (************************************************************************)
 let new_implicit_var reason r env k =
-  new_implicit_var_aux reason r env k Strict None


Only changes in TcUtil are for applying the indexed effects combinators (and some rearrangement).

examples/layeredeffects/GT.fst

…to remain same

aseemr added 30 commits October 7, 2022 17:53

wip, uvar kinds

fb4c558

merge with master

f9a4291

snap

fc33397

don't create guard uvar when weakening or strengthening

0ad14a9

snap

41bdd9d

solve guard uvars in rel

df01d3b

snap

de0c0d0

some debug logs

4858bd8

one guard uvar per uvar, setting in a helper function in Rel

172fc1b

propagation of guard uvar

4384560

cp

ecaa8f3

set guard uvar even if no guard in core check

a802b54

handle a Tm_delayed in the UF graph in push_subst

b96bd7c

some more tweaks

22169a3

snap

e5c8b6a

merge with nik_memoize_tc

d06b1f1

snap

9300f6a

undo syntax subst

0eeac0e

split guard API

e7b81b7

resolve implicits of tc abs guards before discharging smt guard

b89ba36

snap

e0b4dff

use propositional and for incorporating guard uvars in vc

5709d4e

merge

ac5a64e

if guard uvars are not allowed, use allow untyped

72580e7

snap

17e60ef

strengthen lift vc with guards, rather than returning them

9871fef

don't restrict guard uvars, more cases of strengthening with guard uvars

6df0654

snap

2a08115

don't core check allow untyped uvars

906dbe0

adding a meta core guard + some annotations in prims

2bfa4aa

aseemr commented Nov 17, 2022

View reviewed changes

examples/steel/Makefile Show resolved Hide resolved

aseemr commented Nov 17, 2022

View reviewed changes

suppress 352 for ulib/steel

36a4e7e

nikswamy reviewed Nov 17, 2022

View reviewed changes

examples/layeredeffects/GT.fst Show resolved Hide resolved

nikswamy and others added 11 commits November 17, 2022 18:39

tweak subcomp in Sec2.IFC to resolve a warning

352dd51

Merge branch 'master' into _aseem_substitutive_indexed_effects

f9449e2

set range of autogenerated subcomp and ite combinators

7db7e26

another kind of substitutive subcomp that allows for f and g indices …

08c7d7e

…to remain same

classifying and applying substitutive invariant subcomp

8ae7d09

snap

3203555

support for substitutive invariant ite

996542c

nit to Sec1.GST

2976f3e

comment in syntax

97e38d2

nits

e1c1a18

Merge branch 'master' into _aseem_substitutive_indexed_effects

be5fa34

aseemr merged commit 0085786 into master Nov 22, 2022

aseemr deleted the _aseem_substitutive_indexed_effects branch November 22, 2022 05:58

aseemr mentioned this pull request Nov 22, 2022

F* should disallow degenerate effects #2659

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Using core typechecker for indexed effects unification solutions #2760

Using core typechecker for indexed effects unification solutions #2760

aseemr commented Nov 16, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

aseemr Nov 17, 2022

		let to_comb (us, t) = (us, t), dummy_tscheme, None in


		let eff_t, num_effect_params =

		@@ -1814,37 +1816,11 @@ let new_implicit_var_aux reason r env k should_check meta =

		(***************************************************)

		(*

Using core typechecker for indexed effects unification solutions #2760

Using core typechecker for indexed effects unification solutions #2760

Conversation

aseemr commented Nov 16, 2022

Overview

Impact on the client code

Backward compatibility

Relation to #2659

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment