[ssr] "apply:" produces ill-typed terms

[mrhaandi]

Description of the problem

The following ssreflect example uses apply: to incorrectly arrive at No more subgoals for the goal Vector.t unit 0 -> False.
An ill-typed term is produced and detected only at Qed.
Standard Coq apply does not produce such an issue.

Possibly related: #11881 (uses apply /).

Require Vector.
Require Import ssreflect.

Lemma vec_fail (v : Vector.t unit 0) : False.
Proof.
  pattern v.
  apply: (Vector.case0 _ v).
  (* No more subgoals *)
Fail Qed.
(*
  The command has indeed failed with message:
  Illegal application: 
  The term "@Vector.case0" of type
  "forall (A : Type) (P : Vector.t A 0 -> Type),
  P (Vector.nil A) -> forall v : Vector.t A 0, P v"
  cannot be applied to the terms
  "unit" : "Set"
  "fun _ : Vector.t unit 0 => False" : "Vector.t unit 0 -> Prop"
  "v" : "Vector.t unit 0"
  "v" : "Vector.t unit 0"
  The 3rd term has type "Vector.t unit 0" which should be coercible to
  "(fun _ : Vector.t unit 0 => False) (Vector.nil unit)".
*)

Coq Version

The Coq Proof Assistant, version 8.15+rc1
compiled with OCaml 4.13.1

[Alizter]

Also present in master d78e79c.