Using core typechecker for indexed effects unification solutions #2760
Conversation
| @@ -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]] | |||
There was a problem hiding this comment.
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.
| l_subcomp : (tscheme * tscheme); | ||
| l_if_then_else : (tscheme * tscheme); | ||
|
|
||
| l_bind : (tscheme * tscheme * option indexed_effect_combinator_kind); |
There was a problem hiding this comment.
Indexed effect combinators maintain their kinds (substitutive or ad_hoc) (kinds are inferred in TcEffect at the time of typechecking the indexed effect.
| 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 |
There was a problem hiding this comment.
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.
| @@ -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 | |||
There was a problem hiding this comment.
Combinator kind in polymonadic bind and subcomp as well.
| @@ -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 | |||
There was a problem hiding this comment.
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.
| let to_comb (us, t) = (us, t), dummy_tscheme, None in | ||
|
|
||
|
|
||
| let eff_t, num_effect_params = |
There was a problem hiding this comment.
Setting the number of effect parameters in the effect signature.
| @@ -1814,37 +1816,11 @@ let new_implicit_var_aux reason r env k should_check meta = | |||
|
|
|||
| (***************************************************) | |||
|
|
|||
| (* | |||
There was a problem hiding this comment.
No more tedious explanations about using Allow_untyped here.
| | _ -> 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 () |
There was a problem hiding this comment.
Use Strict unless the compat flag is set.
| (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 |
| // | ||
| // returns the (subcomp guard, new sub problems, worklist) | ||
| // | ||
| let apply_substitutive_indexed_subcomp (env:Env.env) |
There was a problem hiding this comment.
Applying a substitutive indexed effect subcomp. It mainly computes substitutions for the combinator binders.
| * 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) = |
There was a problem hiding this comment.
With proper typechecking of the indexed effect combinator binders, we don't need all this no subtype typechecking and eqtype_as_type business.
| 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 |
There was a problem hiding this comment.
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.
| @@ -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 | |||
There was a problem hiding this comment.
Only changes in TcUtil are for applying the indexed effects combinators (and some rearrangement).
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
LowParsewriter effect inexample/layeredeffectsand also in the EverParse repo. In this effect, the memory invariant index of the effect is treated differently insubcompand other combinators. Insubcomp, 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 makebindsubstitutive, but have a_ : squash (inv_f == inv_g)binder whose proof is dispatched to a tactic, which simply doestrefl. 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
ulibandexamples.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 fromPURE).