pattern で ill-typed term が出てくる例

依存型を使っていると destruct が ill-typed term を作って失敗することがあるんですが，その原因が何なのかがよくわからないので似たような現象を起こす小さな例を探しています。

pattern でおそらく同様の原因によるものと思われるエラーが出る例を作りました。

Coq < Section dep_test.

Coq < Variables A B : Set.
A is assumed
B is assumed

Coq < Variables (g : A -> B) (P : B -> Prop) (T : Type) (Q : T -> Prop) (b : forall x, P (g x) -> T).
g is assumed
P is assumed
T is assumed
Q is assumed
b is assumed

Coq < Variables (P1 : B -> Prop) (x : A) (H : forall y : B, P1 y -> P y).
P1 is assumed
x is assumed
H is assumed

Coq < Goal forall (H0 : P1 (g x)), Q (b x (H (g x) H0)).
1 subgoal
  
  A : Set
  B : Set
  g : A -> B
  P : B -> Prop
  T : Type
  Q : T -> Prop
  b : forall x : A, P (g x) -> T
  P1 : B -> Prop
  x : A
  H : forall y : B, P1 y -> P y
  ============================
   forall H0 : P1 (g x), Q (b x (H (g x) H0))

Unnamed_thm < pattern (g x).
Toplevel input, characters 0-13:
> pattern (g x).
> ^^^^^^^^^^^^^
Error: The abstracted term
"fun b0 : B => forall H0 : P1 b0, Q (b x (H b0 H0))"
is not well typed.
Illegal application (Type Error): 
The term "b" of type "forall x : A, P (g x) -> T"
cannot be applied to the terms
 "x" : "A"
 "H b0 H0" : "P b0"
The 2nd term has type "P b0" which should be coercible to 
"P (g x)".

The abstracted term "fun b0 : B => forall H0 : P1 b0, Q (b x (H b0 H0))" を g x に適用したものが，pattern tactic 適用後の goal の候補です。しかし，これには型がつかないというエラーメッセージが出ています。

b x は P (g x) 型の引数をとりますが，abstract する前にその型をもっていた H (g x) H0 はいま H b0 H0 となって，P b0 型をもつようになっています。だから b x に渡されると型が合いません。

サイズはそんなに大きくはありませんが，わかりやすいかというと微妙なところですね。仕組みとしては，b に x が渡されて初めて g x が現れるので (b の型の中では x は束縛変数) pattern で切り出せないまま残る，というふうに見えますが。

もっと具体的でこれくらいの大きさの例があるとわかりやすいのかもしれません。

ちなみに実際にぶつかった例では b は Program Definition が生成した obligation で，equality proof を引数にとるところで型が合わなくなってました。