tactics: ctrl_rewrite: perform rewrite under arrows; fix rewrite under dependent binders

[amosr]

I wanted to perform rewrites on the environment, but when I reverted the environment it wouldn't rewrite. It looks like ctrl_rewrite was missing part of the implementation.

Additionally, I believe that the handling of dependent binders in ctrl_rewrite was incorrect. For a function abstraction fun (a: Type) (x: a) -> x it was taking the binders [a: Type; x: a] and computing a close substitution [a := bv@1; x := bv@0]. But we can't apply that substitution to the binders, because the binder x: a needs to refer to a with de bruijn index 0, not 1.

At least, this is what I think was causing the rewriting problem that I saw. I suspect that this may not have come up often in the past because functions with dependent binders will occur more often in the environment than in the goal.

To rewrite under arrows, I only implemented rewrite for Total and GTotal computations. It wasn't clear to me what to do for effectful computations. (I assume that they won't occur in reverts, anyway.) How often does this case occur - should it perhaps print a warning?

While debugging, I also made some of the "Impossible" errors a little more searchable. (Is there an easier way to track down what threw the impossible?)

[amosr]

@nikswamy hi Nik, I came across this bug the other day where ctrl_rewrite throws an error on dependent binders:

let dependent_binders =
  assert (let id = fun (a: Type) (x: a) -> x in id Type0 True)
    by (FStar.Tactics.pointwise (fun () -> FStar.Tactics.trefl ()))

gives uncaught exception: Failure("Impossible")

I believe this PR fixes the above error. ctrl_rewrite also didn't descend into arrows, so I've implemented that for pure arrows too. I can split them out to separate PRs if rewriting under arrows is iffy?

[mtzguido]

Hi Amos, thank you! This does look correct to me. I'll merge it.

For effectful arrows I think we could still rewrite in the same way in the type and indices.. but it's not a common case and I'd be wary of writing yet another syntactic pass over terms, maybe we could instead reuse FStar.Syntax.Visit.visit_tm, but I don't think it's a pressing concern.

While debugging, I also made some of the "Impossible" errors a little more searchable. (Is there an easier way to track down what threw the impossible?)

--trace_error and --error_contexts true can help here, but the messages being distinct is a definite improvement.