在同一索引處使用兩個感應類型值匹配的模式

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.