Benjamin Bonneau

Expose the `unascribe` normalisation step

1

This PR exposes the `unascribe` normalisation step. It can be useful to get more readable terms and it also seems to speed up some normalisations. I have just exposed the...

F* should disallow degenerate effects

4

F* (https://github.com/FStarLang/FStar/commit/5bcd16865e5161ccbc7b2b9ead96ba099618adf8) does not seem to retypecheck the parameters of the effect combinators when they are used. This is probably intentional since it notably avoids rechecking the monotonicity of `pure_wp`...

The type of `/\` and related connectives does not reflect their left-to-right bias (Was: The typechecking of `l_and` as a lazy operator is unsound)

1

In F*, the type-checking of `l_and` (`⋀`) reflects its laziness. That is in `p ⋀ q`, the type-checking of `q` can assume that `p` holds. Hence it is possible to...

Subtyping and unification in the tactics engine requires re-checking solutions (Was: The unification in tactics is unsound)

3

On can prove `⊥` using the unification of uvars in tactics (F* https://github.com/FStarLang/FStar/commit/a46a208c59b502b427e300e7a9e7b7cf9fb58ad7): ```fstar module Main open FStar.Tactics #set-options "--ifuel 0 --fuel 0" let prove_False (pf : squash False) (_...

Steel definition fails in dependency loading

1

The following Steel definition is accepted in normal and in lax mode but not when loaded as a dependency: ```fstar module A open Steel.Effect noeq type fsteel (pre : pre_t)...

Absence of control on the order of resolution of implicits

1

When using `resolve_implicits`, there seems to be no option to control the order in which the different implicits are instantiated. This is needed when interacting with libraries (such as Steel)...

Tactic using anti-quotation for a binder stuck if lax checked

1

The following example verify without any issue when checked in normal mode: ```fstar module Main open FStar.Tactics let dummy_lemma (x : int) goal (pf : goal) : goal = pf...

On a steel example similar to the one given for [PR#2534](https://github.com/FStarLang/FStar/pull/2534), fstar still fails to rewrite a vprop with an `smt_fallback` and raises a typing error: ```fstar module Mem =...