`destruct` does not work as well in 9.2 as it does in 9.1

[JasonGross]

Description of the problem

This code succeeds in 9.1 but fails in 9.2

Small Rocq / Coq file to reproduce the bug

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-R" "." "IsomorphismChecker" "-top" "IsomorphismChecker.EqualityLemmas") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1889 lines to 24 lines, then from 38 lines to 192 lines, then from 199 lines to 46 lines, then from 61 lines to 46 lines, then from 61 lines to 37 lines, then from 52 lines to 37 lines *)
(* coqc version 9.2+rc2 compiled with OCaml 4.14.2
   coqtop version 9.2+rc2
   Expected coqc runtime on this file: 3.272 sec
   Expected coqc peak memory usage on this file: 181856.0 kb *)
#[export]
Set Universe Polymorphism.
#[local] Set Primitive Projections.
Inductive eq@{s|u|} {α:Type@{s|u}} (a:α) : α -> SProp
  := eq_refl : eq a a.

#[local] Notation "x = y" := (eq x y) : type_scope.
Arguments eq_refl {α a} , [α] a.
#[export]
Set Implicit Arguments.
Record Iso@{s s'|u u'|} (A : Type@{s|u}) (B : Type@{s'|u'}) := {
    to :> A -> B;
    from : B -> A;
    to_from : forall x, to (from x) = x;
    from_to : forall x, from (to x) = x;
}.
Record > rel_iso@{s s'|u u'|} {A B} (i : Iso@{s s'|u u'} A B) (x : A) (y : B) : SProp := { proj_rel_iso :> i.(to) x = y }.
Axiom functional_extensionality_dep@{s s'|u u' u''|u<=u'',u'<=u''}
  : forall {A : Type@{s|u}} {B : A -> Type@{s'|u'}} (f g : forall x : A, B x), (forall x : A, f x = g x) -> eq@{s'|u''} f g.

Definition IsoForall@{s0 s1 s2 s3|u0 u1 u2 u3 u4 u5|u0 <= u4,u1 <= u5,u2 <= u4,u3 <= u5}
  {A A'} (isoA : Iso@{s0 s1|u0 u1} A A') (B : A -> Type@{s2|u2}) (B' : A' -> Type@{s3|u3})
  : (forall a a' (He : rel_iso isoA a a'), Iso (B a) (B' a'))
    -> Iso@{s2 s3|u4 u5} (forall a, B a) (forall a', B' a').
Proof.
  intro H; unshelve esplit; [ intros f a .. | intro x; shelve | intro x; shelve ].
  all: first [ specialize (H a) | specialize (fun a' => H a' a) ].
  all: first [ specialize (H (isoA.(to) a)) | specialize (H (isoA.(from) a)) ].
  all: first [ specialize (H eq_refl) | specialize (H (isoA.(to_from) a)) ].
  all: [ > first [ apply H.(to) | apply H.(from) ]; auto .. ].
  Unshelve.
  all: cbn.
  all: apply functional_extensionality_dep; intro.
  {
 destruct to_from. (* Error: Unable to find an instance for the variables A, B, i, x. *)

Version of Rocq / Coq where this bug occurs

9.2.0

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

9.1.0

[JasonGross]

Sorry, I think this is with #21773

[SkySkimmer]

5f1a2fa is the first bad commit

[SkySkimmer]

I guess this is intended behaviour. Before Iso was non primitive

Warning:
The record Iso could not be defined as a primitive record because it is not in SProp but all
projections may be irrelevant. [non-primitive-record,records,default]

after it is primitive without eta, so no dependent elimination and destruct cannot change the goal.

Maybe we could have a better error message on destruct?