FYI this build failed because of:

[STDERR]/home/everest/hacl-star/lib/Lib.LoopCombinators.fst(102,4-102,10): (Error 228) user tactic failed: `t_trefl: cannot unify (i: a{p i}) and (i: a{q i})` (see also /home/everest/hacl-star/lib/Lib.LoopCombinators.fst(103,45-103,54))
[STDERR]1 error was reported (see above)
[STDERR]make[1]: *** [Makefile:405: obj/Lib.LoopCombinators.fst.checked] Error 1

but I assume this will start working once the F* change lands?

Hi Jonathan, yes that eta expansion is related. The way the precondition is written in C.Loops is fun h -> inv h and here it was written h. To prove these two equal, we earlier had eta equality but not anymore. So I had to expand it here too. I would say no special guidelines as such ... most of the times the preconditions are more than simple inv.

The failure is because the proof requires some changes that Nik did in F* nik_remove_eta. So we discussed that we will first merge F*, get a green here, and then merge it.

Thanks... so if the function requires test: ... Stack (fun h -> inv h) and you pass it an argument of type .. -> Stack inv, it's now a typing error, correct?

Will it always be a typing error from here on, or just in certain cases? (If it's the former, it's a surprising enough change that I should send a heads-up to other HACL folks who may not be following such F* changes closely.)

That particular proof is quite technical. It does require a tactic to rewrite with propositional extensionality, then refinement-type equality, at depth. SMT-based proofs cannot do that. This kind of thing shouldn't come up very often.

It also has to do with the $ on the argument of C.Loops.while ... if that $ was not there subtyping would kick in and this would work. But with $, we try to prove equal which is not possible now in the absence of eta.

Ah I see. Barely anyone uses $ (@tahina-pro was the one who introduced the $ here if I recall correctly) so I don't expect this will be a problem for day-to-day uses of HACL*. Thanks for the clarification!

I was using $ to empirically help in second-order unification of the pre and postconditions of the while loop test, but I certainly do not claim any expertise on that.

Weird, I'm seeing failures now in Hacl.Impl.Exponentiation that I wasn't seeing before. Will take a look later this evening.