cbv on undefined evars under binders when the substitution involves cases produces unbound rel

[yannl35133]

Description of the problem

Eval cbv zeta in (fun (a : True) => (?[T] : True),
  let r :=
    let b := I in
    match tt with tt => b end
  in
  ?T@{a := r}).

= (fun a : True => ?T, ?T@{a:=match tt with
                              | tt => _UNBOUND_REL_1
                              end})
: (True -> True) * True
where
?T : [a : True |- True]

this can be turned into something which fails because of it, although the instance I found is contrived.

Require Import Coq.Program.Tactics.

Program Definition a := Eval cbv zeta in (fun (a : True) => (?[A] : nat),
  let r :=
    let b := I in match tt with tt => b end
  in
  ?A@{a := r},
  fun (a : True) => (eq_refl : ?A = _)).

Next Obligation.
  destruct a; exact 0.
Defined.

File "/tmp/foo.v", line 12, characters 0-8:
Error:
Unbound reference: In environment
anonymous' : unit
The reference 3 is free.

Coq Version

8.18.0, master

Fix

coq/pretyping/cbv.ml

Line 374 in f202dcb

(mkCase (ci, u, pms, ty, iv, t,br))

-        (mkCase (ci, u, pms, ty, iv, t,br))
+        (apply_env @@ mkCase (ci, u, pms, ty, iv, t,br))

PR #18195