Ltac pattern matching: why does `forall x, ?P x` not match `forall x, x`?

Ltac checkForall H :=
  let T := type of H in
  match T with
  | forall x, ?P x =>
    idtac
  | _ =>
    fail 1 "not a forall"
  end.

Example test : (forall x, x) -> True.
Proof.
  intros H.
  Fail checkForall H. (* not a forall *)
Abort.

I would naively expect checkForall H to succeed, but it doesn't.

In his book Certified Programming with Dependent Types, Adam Chlipala discusses a limitation of pattern matching on dependent types:

The problem is that unification variables may not contain locally bound variables.

Is this the reason for the behaviour I'm seeing here?