Gabriel Ebner

This error also appears in pure F*. Apparently type class resolution is (a) run before sending the VCs to Z3 and (b) eagerly discharges VCs itself. ```fstar let bar #k...

A minimized version that might (or might not) be easier to digest: ```fstar module MissingUniv let contradiction : squash False = assert Functions.is_inj (id #Type0); Classical.forall_intro (Cardinality.Universes.no_inj_universes u#0 u#(a+1)) ```

This is fixed now after merging #3699.

> I'm doing an everest run right now. And it finished successfully.

I managed to fix the reduce/reduce conflicts: ``` Warning: 16 states have shift/reduce conflicts. Warning: 33 shift/reduce conflicts were arbitrarily resolved. Warning: 233 end-of-stream conflicts were arbitrarily resolved. ``` However,...

FWIW, I'm also getting these warnings: ``` File "fstar-lib/FStar_Parser_Parse.mly", line 125, characters 60-70: Warning: the token LBRACK_BAR is unused. File "fstar-lib/FStar_Parser_Parse.mly", line 319, characters 0-15: Warning: symbol decoratableDecl is unreachable...

> There are also unnecessary parenthesis in expressions like `p /\ (let x = ... in ...)` and `p /\ (match x with ...)`, similar to the `forall` example! I...

I just did another everest run with the changes to forall/exists, and I can confirm that there are no regressions.

Okay, I tried to make the typings and the associated functions ghost. But to my suprise, there were plenty more functions with a questionable implementation based on the tactic/reflection API...

Options: - extend the attribute `[@@erasable (fun _ -> ())]` - extend the attribute with the arity `[@@erasable 1]` (defaulting to zero) (maybe `let erasable = erasable_at 0` or something)...