cbn reduces in the context of the goal's evars

[cpitclaudel]

Description of the problem

The following program does not terminate (it allocates until it crashes):

Goal (0 = 0).
  pose (Nat.pow 2 30).
  etransitivity.
  clear.
  cbn.

This is because cbn reduces the context of the evars that appear in the goal in addition to the goal itself:

Set Printing Existential Instances.
Goal (0 = 0).
  pose (Nat.pow 2 5).
  etransitivity.
(*  n := Nat.pow 2 5 : nat
    ============================
    0 = ?y@{n:=n} *)
  cbn.
(*  n := Nat.pow 2 5 : nat
    ============================
    0 = ?y@{n:=32} *)
  Show Existentials.

Is that on purpose? (simpl doesn't do that) Don't we expect users to run instantiate (1 := ltac:(cbn in * )). for that instead?

I came across this while porting some code from 8.4 to 8.9; I changed some simpls to cbns and everything blew up.

Coq Version

8.9.1.

[SkySkimmer]

Relevant code:

coq/tactics/cbn.ml

Lines 833 to 835 in f81225b

	let rec strongrec env t =
	map_constr_with_full_binders env sigma
	push_rel_check_zeta strongrec env (whd_cbn flags env sigma t) in

[SkySkimmer]

Maybe we could reduce evar arguments with delta of the proof context off? Or maybe it would be enough to reduce only the non-identity parts of the instance?

Don't we expect users to run instantiate (1 := ltac:(cbn in * )). for that instead?

I don't ever expect anyone to use instantiate.