Aymeric Fromherz

Regarding the data uvars, I think that's fine, and actually useful this way. This will provide better information about what has been solved in the current state, and which implicits...

Posting here several observations from ongoing work: Example 4 is indeed due to the discrepancy between `hide u0` and `v0`. We might be able to apply an slprop canonicalization pass...

More comments about why we currently require a return at the end of each function, and how we might avoid it. Let's consider the following code: ``` let read_write (#a:Type)...

We also discussed how to typecheck the following example: ``` assume val p: slprop let f (#a:Type) (r0:reference a) (v0:erased a) : SteelT unit (p `star` pts_to r0 full_perm v0)...

This fix unfortunately comes with a memory blowup leading to examples/steel/Queue failing for instance with an OOM error on the CI machine

Update on this: generating a uvar for the equality in all cases is a bit too powerful. In particular, a common usecase of `ctrl_rewrite` is through `pointwise`, where a lot...

Trying to debug this further, it seems that lax-checking A.fst from Emacs does indeed succeed, but running `fstar.exe --lax A.fst` from the command-line leads to the same error as when...

I didn't get a chance to look yet, I'll try to inspect the queries and report back.

Yes, we observed something similar. In @cmovcc's initial usecase, this was occuring when if/then/else branches consisted of a single return, he minimized it further to this small snippet.

Note, while ppx_deriving_yojson does not have this opaque feature, it should be possible to emulate it using the override of default derivations. For instance, by annotating a field with ```@to_yojson...