# Arbitrary types in Dependent Pattern Matching

Consider the following example of length indexed list, taken from CPDT

``````Section ilist.
Variable A : Set.

Inductive ilist : nat -> Set :=
| Nil : ilist O
| Cons : forall n, A -> ilist n -> ilist (S n).

Definition hd n (ls: ilist (S n)): A :=
match ls in (ilist n') return match n' with
| O => unit
| S n'' => A
end with
| Nil => tt
| Cons h hs => h
end.
``````

In the case for `hd` Nil it’s type is unit, and `unit` is not `A`, so why does Coq accept this definition? I know Nil is unreachable in this case, but what exactly is going under the hood for Coq to allow a branch to have an arbitrary type?

So you know that `ls: ilist (S n)` and the `in (ilist n')` annotation just binds `S n` to the identifier `n'`. This means that

``````return match n' with
| O => unit
| S n'' => A
end
``````

is the same as

``````return match S n with
| O => unit
| S n'' => A
end
``````

which in its turn is the same as just `return A`. Hence the type `A` we required as the output type of `hd` is still `A`.

Then why go through all that trouble of expanding the return type? This is needed because Coq will substitute the index `n'` with `O` and `S n0` in the `Nil` and `Cons` branches of the `match ls ...`-expression. And in the case of `Nil` branch `n'` is `O`, so the return type inside the `Nil` branch is going to be

``````return match O with
| O => unit
| S n'' => A
end
``````

i.e. `unit`.

Had we not mentioned `n'` anywhere in the return type, the substitution would be vacuous and the return type would stay the same in both branches, leading to impossible to solve `Nil` branch.

1 Like

So basically if we are type checking `Definition t x : A := match x return T with ...` it first normalize `T` and then check if it matches `A`?

More precisely, Coq first substitutes the parameters of the inductive type of `x` into `T`. Then, it checks if types `A` and `T` are convertible. Normalization is one way of checking convertibility, but it is kind of a last resort, if all the other heuristics failed.

2 Likes

Can you give me a list of heuristics applied in this case?

Since `A` is an atomic term, no heuristic applies in this case. So, Coq just computes the weak head normal form of `match S n' with ... end`, which is `A`.

Heuristics matter when Coq is comparing definitions or applications. For example, if Coq is comparing the applications `a b` and `c d`, it will first check whether `a` and `c` (resp. `b` and `d`) are convertible. If they are, no need to normalize anything.

1 Like

What about when `T` is a product `forall foo: bar, T'`? Does it first perform a beta reduction on any application after the match?

For example:

``````Definition hd' n (ls: ilist (S n)): A :=
match ls in (ilist n') return (n' = S n) -> A with
| Nil => fun eq => False_rect A (PeanoNat.Nat.neq_succ_0 n (eq_sym eq))
| Cons h hs => fun _ => h
end eq_refl.
``````

Never mind, I just noticed that in this case the type checker will consider the whole body of the function, and in this case it is an application.

Just my personal opinion, but; on complicated cases of dependent pattern matching, i think it’s simpler to understand what’s going on with eliminators instead. Don’t get me wrong, i like “match” as a construct, but dependent matching mixes too much stuff, i feel. For example, an earlier reply was talking about how “Coq first substitutes the parameters of the inductive type of x into T”: using an eliminator makes it clear this isn’t some sort of specific mechanism to pattern matching, it’s just regular function application.

Take the " hd’ " function you posted, for instance. With an eliminator, its definition looks like :

``````  Definition hd'_alt (n:nat) (ls : ilist (S n)) : A :=
@ilist_rec (fun n' _ => n' = S n -> A)
(fun eq => False_rect A (PeanoNat.Nat.neq_succ_0 n (eq_sym eq)))
(fun m h hs _ => (fun _ => h))
(S n) ls eq_refl.
``````

At first glance, this is a mouthful no one would be advised to write, but: you can define it partially. For example, you can check that

``````Definition hd'_start (n:nat) :
((0 = S n) -> A) ->
(forall m (h:A) hs, ((m = S n) -> A) -> (S m = S n) -> A) ->
forall i, ilist i -> i = S n -> A
:= @ilist_rec (fun n' _ => n' = S n -> A).
``````

…and from there it’s a matter of filling holes. Proof mode makes this task simpler, of course.

I agree, dependent pattern matching is still something I don’t think we got quite right yet. This makes me excited about the Equations plugin, for example. My only complaint is that I believe match expressions are superior to equations because they live in the expression level, meaning that you have a much higher freedom to make a case analysis anywhere in your code.