在同一索引处使用两个感应类型值匹配的模式

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. 

错误消息：

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

感谢“护航模式”的安东Trunov的提示，我设法让那一个编译版本。

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.