CODEWITHSUNDEEP
pattern-matchingcoqdependent-type
Li-yao Xia
Li-yao Xia

Reputation: 33569

Pattern matching with two values of inductive type at the same index

Why does the following not type-check (coq-8.5pl3)? Pattern matching seems to forget that u and v have the same type.

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 message:

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".

Upvotes: 1

Views: 90

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33569

Thanks to Anton Trunov's hint of "convoy pattern", I managed to make a version that compiles.

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.

Upvotes: 2

Related Questions