refine produces ill-typed term

[mrhaandi]

Description of the problem

In the following example, refine produces an ill-typed term with No more subgoals., which is rejected on Qed.

Axiom f : unit -> Prop.
Axiom f_intro : forall x, f x.
Axiom P : Prop.
Axiom f_P : forall (x : unit), f x -> P.

Goal forall (x : unit), P.
Proof.
  intros x.
  refine (f_P _ (match x as u return (f _) with tt => _ end)).
  refine (f_intro _ : f (match x as u return (f u -> unit) with tt => fun _ => tt end (f_intro x))).
  (* No more subgoals. *)
Fail Qed.
(*
In pattern-matching on term "x" the branch for constructor 
"tt" has type "f x -> unit" which should be "f tt -> unit".
*)

This looks similar to #7726. However, #7726 (possibly already fixed?) with Coq 8.16 does not accept the refine statement in the initial example. Here, refine is accepted and Qed fails.

Coq Version

The Coq Proof Assistant, version 8.16.0 compiled with OCaml 4.14.0

[herbelin]

It seems that a typing constraint is lost (not solved with #16097).