同じインデックスの誘導型の2つの値とのパターンマッチング

Question

次のようなタイプチェック（coq-8.5pl3）がないのはなぜですか？パターンマッチングは、uとvが同じタイプであることを忘れているようです。

Inductive X : Type -> Type := 
| XId : forall a, X a -> X a 
| XUnit : X unit. 

Fixpoint f {a : Type} (x : X a) (y : X a) : a := 
    match x, y with 
    | XId _ u, XId _ v => f u v 
    | XUnit, _ => tt 
    | _, XUnit => tt 
    end. 

エラーメッセージ：「船団パターン」のアントンTrunovのヒントに

Error: 
In environment 
f : forall a : Type, X a -> X a -> a 
a : Type 
x : X a 
y : X a 
T : Type 
u : X T 
y0 : X T 
T0 : Type 
v : X T0 
The term "v" has type "X T0" 
while it is expected to have type "X T". 

Answer 1

おかげで、私はコンパイルしたバージョンを作ることができました。 /：

Fixpoint f {a : Type} (x : X a) : X a -> a := 
    match x in X a return X a -> a with 
    | XId b u => fun y => match y in X b return X b -> b with 
         | XId c v => fun u => f u v 
         | XUnit => fun _ => tt 
         end u 
    | XUnit => fun _ => tt 
    end.