destruct produces an ill-typed term

[mrhaandi]

Description of the problem

The tactic destruct constructs an ill-typed term which closes the goal (using reflexivity) but fails on Qed.
Possibly connected to #16900.

Small Coq file to reproduce the bug

Inductive t : unit -> Type :=
  t_intro : t tt.

Goal forall (v : t tt), v = (t_intro : t tt).
Proof.
  intros v.
  destruct v.
  reflexivity.
  (* Proof finished *)
Fail Qed.
(*
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
"t u0" : "Prop"
"t" : "t u0"
"t_intro" : "t tt"
The 3rd term has type "t tt" which should be a subtype of 
"t u0".
*)

Version of Coq where this bug occurs

8.19.0

[SkySkimmer]

Interesting, destruct fails when there's no cast (eg if you simpl first).

[SkySkimmer]

Since #16182 (8.17)
The problem is the eq_constr at

coq/pretyping/typing.ml

Line 694 in 38d6695

if EConstr.eq_constr sigma good c then sigma, Same, make_judge c (Retyping.get_type_of env sigma c)

eq_constr ignores casts which causes us to assume u := tt, u0 : unit |- (t_intro : t u) (the trusted term) and u := tt, u0 : unit |- (t_intro : t u0) are the same

[SkySkimmer]

A patch like

modified   engine/eConstr.ml
@@ -632,6 +632,21 @@ let eq_constr sigma c1 c2 =
   in
   eq_constr 0 c1 c2
 
+let strong_eq_constr sigma c1 c2 =
+  let kind c = kind sigma c in
+  let eq_inst _ i1 i2 = EInstance.equal sigma i1 i2 in
+  let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
+  let eq_existential eq e1 e2 = eq_existential sigma (eq 0) e1 e2 in
+  let rec eq_constr nargs c1 c2 =
+    match kind c1, kind c2 with
+    | Cast (c1, _, t1), Cast (c2, _, t2) ->
+      eq_constr 0 t1 t2 && eq_constr nargs c1 c2
+    | Cast _, _ | _, Cast _ -> false
+    | _ ->
+      compare_gen kind eq_inst eq_sorts (eq_existential eq_constr) eq_constr nargs c1 c2
+  in
+  eq_constr 0 c1 c2
+
 let eq_constr_nounivs sigma c1 c2 =
   let kind c = kind sigma c in
   let eq_existential eq e1 e2 = eq_existential sigma (eq 0) e1 e2 in
modified   engine/eConstr.mli
@@ -341,6 +341,7 @@ val whd_evar : Evd.evar_map -> constr -> constr
 (** {6 Equality} *)
 
 val eq_constr : Evd.evar_map -> t -> t -> bool
+val strong_eq_constr : Evd.evar_map -> t -> t -> bool
 val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
 val eq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
 val leq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
modified   pretyping/typing.ml
@@ -691,7 +691,7 @@ let judge_of_apply_against env sigma changedf funj argjv =
 
 (* Assuming "env |- good : some type", infer "env |- c : other type" *)
 let rec recheck_against env sigma good c =
-  if EConstr.eq_constr sigma good c then sigma, Same, make_judge c (Retyping.get_type_of env sigma c)
+  if EConstr.strong_eq_constr sigma good c then sigma, Same, make_judge c (Retyping.get_type_of env sigma c)
   else
     let assume_unchanged_type sigma =
       let gt = Retyping.get_type_of env sigma good in

works but IDK if that's the right way to do it.