Layered effects work items

[aseemr]

This is a meta-issue to track some remaining work items in layered effects.

• [ ] Enforce that the extra arguments to the combinators are must_erase_for_extraction. They are not maintained in the typechecker (and we pass ( ) as their values when reifying) so it would be unsound to compute with them.

• [x] Enforce the soundness of the if-then-else combinator, essentially ask the user to provide a lemma that if p holds then the if_then_else is a super-comp of c_then and if ~ p then if_then_else is a super-comp of c_else.

• [ ] Extraction of state parametric state effect (see https://github.com/FStarLang/FStar/blob/master/examples/layeredeffects/ParametricStateIssue.fst).

• [x] Kremlin extraction for FlightsStExn.fst (OCaml extraction works fine).

• [ ] In Rel, don't defer the problems that can't be solved because of errors such as free variables mismatch.

• [x] Enable lifts from layered effects.

• [ ] For subcomp combinator, we should add a Meta_monadic node for its application, and reify it properly during extraction. Mostly it's an identity though.

• [x] One step reflect

• [x] Allow programmers to provide the proof of soundness of the if_then_else combinator.

• [ ] Reification of polymonadic binds (see one of the comments below with details).

[aseemr]

Added the soundness check for if_then_else combinators: https://github.com/FStarLang/FStar/commit/8dd449469a24e5259a95d1e8b2c461808545c478

[aseemr]

See https://github.com/FStarLang/FStar/issues/1879 for erasing the index arguments.

[aseemr]

We recently added support for polymonadic binds in the typechecker, see https://github.com/FStarLang/FStar/wiki/Polymonadic-binds. But we haven't yet implemented reification of these. Following note outlines an implementation strategy (as discussed with @nikswamy).

When typechecking effectful code, the typechecker adds Meta_monadic annotations to the terms, which are then used to reify the code (during extraction or user annotated reify e). For example,

let x = e1 in
e2

where G |- e1 : M t1 wp1, and G, x:t1 |- e2 : N t2 wp2, the typechecker will rewrite it to:

Meta_monadic (P, let x = Meta_monadic_lift (M, P, e1) in
                              Meta_monadic_lift (N, P, e2))

where P is the least upper bound of M and N in the effect lattice.

Another place where such rewriting comes up is the monadic applications, where effectful arguments (and head) are explicitly lifted as let bindings and decorated with these monadic annotations.

To support polymonadic binds, we need to extend these meta annotations syntax to add a new case for polymonadic binds. For the let case, it would work as follows:

Meta_polymonadic (M, N, P, let x = e1 in e2)

And then these annotations can be handled in the normalizer when a reification happens.

The function application case is a bit more involved. Currently, given e e1 ... en, only the effectful terms are hoisted and let bound, the pure terms are left as is. In the case of polymonadic binds, to keep the code simple, we would like to hoist (let-bind) all the terms and bind them appropriately.

We would do it only if during the application, some polymonadic bind was used and the final effect is reifiable. For pure and ghost arguments, we could even add inline_let attribute to the let-binding, so that extraction puts them back in place.

Note that always let-binding all the arguments, pure or not, is also correct, but it may lead to exploded terms in the typechecker, so we would start with doing it just for reifiable polymonadic binds.