Fail to `destruct` due to ill-typedness and even cannot give an exact term in Coq

I tried to implement the following Coq code:

Set Implicit Arguments.

Inductive fun_eq A B (f : A -> B) : forall C D, (C -> D) -> Prop :=
  fun_eqrefl : forall g : A -> B, f = g -> fun_eq f g.

Lemma fun_eq0 A B (f g : A -> B) : fun_eq f g -> f = g.
Proof. intros H. destruct H.

But destruct H. fails with an error message:

Abstracting over the terms "A", "B" and "g" leads to a term
fun (A0 B0 : Type) (g0 : A0 -> B0) => f = g0 which is ill-typed.
Reason is: Illegal application: 
The term "@eq" of type "forall A : Type, A -> A -> Prop" cannot be applied to the terms
 "A0 -> B0" : "Type"
"f" : "A -> B"
"g0" : "A0 -> B0"
The 2nd term has type "A -> B" which should be coercible to
 "A0 -> B0".

I think there would be two workarounds for this kind of error, neither of which worked in this case.

• One is to admit the proof_irrelevance. However, it is impossible to construct an alternating proof for fun_eq f g because the argument of fun_eqrefl is what we want.

• Another way is to provide an exact term using refine, but I couldn't come up with such a term. Also, if there were such a term (it would involve match statement), I suspect my previous question could be solved in a similar way.

Is it possible to prove fun_eq0? If so, how can it be done?

You can prove it using UIP (special case of proof irrelevance for eq).

The trick is to rewrite one side of the equality f to cast eq_refl f, where cast : A = B -> A -> B, and use UIP/proof irrelevance to replace eq_refl with an equality proof obtained from the H : fun_eq f g assumption. That way, when you destruct H, the type of the LHS changes simultaneously with the type of the RHS.

Set Implicit Arguments.
From Coq Require Import ProofIrrelevance.

Inductive fun_eq A B (f : A -> B) : forall C D, (C -> D) -> Prop :=
  fun_eqrefl : forall g : A -> B, f = g -> fun_eq f g.

(* Extract the equality on types *)
Definition fun_eq_tyeq {A B C D} (f : A -> B) (g : C -> D) (H : fun_eq f g) : (A -> B) = (C -> D) :=
  match H with
  | fun_eqrefl _ => eq_refl
  end.

Definition cast A B (e : A = B) (x : A) : B := eq_rect A (fun T => T) x B e.

Lemma fun_eq0 A B (f g : A -> B) : fun_eq f g -> f = g.
Proof.
  intros H.
  change (cast eq_refl f = g).
  replace eq_refl with (fun_eq_tyeq H) by apply UIP.
  destruct H.
  cbn.
  auto.
Qed.