Failure of tactic in --lax

[mtzguido]

trafficstars

module P

open FStar.Tactics.V2

#push-options "--lax"

let aux2 (p:Type0)
: Lemma True
= calc (==>) {
    squash p;
    ==> { _ by (apply (`Squash.join_squash); hyp (nth_var (-1))) }
    p;
  }

Gives:

* Error 217 at FStar.Calc.fsti(91,52-91,62):
  - Tactic left uninstantiated unification variable ?87 of type Type0 (reason = "flex-flex quasi:      lhs=Instantiating implicit argument in application     rhs=apply arg")

Blocking #3174

[mtzguido]

Partly caused by the special handling of ==> in calc, which uses FStar.Calc.push_impl to obtain the antecedent in scope for the justification of the step. If one makes calc not use that, then this works better. But the problem seems to be that the tactic runs in an environment with unresolved uvars.

let (==>>) = (==>)

let aux2 (p:Type0)
: Lemma True
= calc (==>>) {
    squash p;
    ==>> { _ by (let b = implies_intro () in apply (`Squash.join_squash); hyp b) }
    p;
  }