13.5 When does the expansion strategy fail ?
The strategy works very like in ML languages when treating patterns of non-dependent type. But there are new cases of failure that are due to the presence of dependencies.The error messages of the current implementation may be sometimes confusing. When the tactic fails because patterns are somehow incorrect then error messages refer to the initial expression. But the strategy may succeed to build an expression whose sub-expressions are well typed when the whole expression is not. In this situation the message makes reference to the expanded expression. We encourage users, when they have patterns with the same outer constructor in different equations, to name the variable patterns in the same positions with the same name. E.g. to write (cons n O x) => e1 and (cons n _x) => e2 instead of (cons n O x) => e1 and (cons n' _x') => e2. This helps to maintain certain name correspondence between the generated expression and the original.
Here is a summary of the error messages corresponding to each situation:
-
patterns are incorrect (because constructors are not applied to
the correct number of the arguments, because they are not linear or
they are wrongly typed)
- In pattern term the constructor ident expects num arguments
- The variable ident is bound several times in pattern term
- Constructor pattern: term cannot match values of type term
- the pattern matching is not exhaustive
- This pattern-matching is not exhaustive
- the elimination predicate provided to Cases has not the
expected arity
- The elimination predicate term should be of arity num (for non dependent case) or num (for dependent case)
- the whole expression is wrongly typed, or the synthesis of
implicit arguments fails (for example to find the elimination
predicate or to resolve implicit arguments in the rhs).
There are nested patterns of dependent type, the elimination predicate corresponds to non-dependent case and has the form [x1:T1]...[xn:Tn]T and some xi occurs free in T. Then, the strategy may fail to find out a correct elimination predicate during some step of compilation. In this situation we recommend the user to rewrite the nested dependent patterns into several Cases with simple patterns. In all these cases we have the following error message:
-
Expansion strategy failed to build a well typed case
expression. There is a branch that mismatches the expected
type. The risen
type error on the result of expansion was:
-
Expansion strategy failed to build a well typed case
expression. There is a branch that mismatches the expected
type. The risen
- because of nested patterns, it may happen that even though all
the rhs have the same type, the strategy needs dependent elimination
and so an elimination predicate must be provided. The system warns
about this situation, trying to compile anyway with the
non-dependent strategy. The risen message is:
- Warning: This pattern matching may need dependent elimination to be compiled. I will try, but if fails try again giving dependent elimination predicate.
- there are nested patterns of dependent type and the
strategy builds a term that is well typed but recursive calls in fix
point are reported as illegal:
- Error: Recursive call applied to an illegal term ...
This is because the strategy generates a term that is correct w.r.t. to the initial term but which does not pass the guard condition. In this situation we recommend the user to transform the nested dependent patterns into several Cases of simple patterns. Let us explain this with an example. Consider the following definition of a function that yields the last element of a list and O if it is empty:
Coq < Fixpoint last [n:nat; l:(listn n)] : nat :=
Coq < Cases l of
Coq < (consn _ a niln) => a
Coq < | (consn m _ x) => (last m x) | niln => O
Coq < end.
Error during interpretation of command:
Fixpoint last [n:nat; l:(listn n)] : nat :=
Cases l of
(consn _ a niln) => a
| (consn m _ x) => (last m x) | niln => O
end.
Error: Recursive call applied to an illegal term
The recursive definition
[n:nat]
[l:(listn n)]
<[_:nat]nat>
Cases l of
niln => O
| (consn n0 a a0) =>
<[_:nat]nat>
Cases a0 of
niln => a
| (consn t1 t0 t) => (last (S t1) (consn t1 t0 t))
end
end is not well-formed
It fails because of the priority between patterns, we know that this definition is equivalent to the following more explicit one (which fails too):
Coq < Fixpoint last [n:nat; l:(listn n)] : nat :=
Coq < Cases l of
Coq < (consn _ a niln) => a
Coq < | (consn n _ (consn m b x)) => (last n (consn m b x))
Coq < | niln => O
Coq < end.
Note that the recursive call (last n (consn m b x)) is not guarded. When treating with patterns of dependent types the strategy interprets the first definition of last as the second one(In languages of the ML family the first definition would be translated into a term where the variable x is shared in the expression. When patterns are of non-dependent types, Coq compiles as in ML languages using sharing. When patterns are of dependent types the compilation reconstructs the term as in the second definition of last so to ensure the result of expansion is well typed.). Thus it generates a term where the recursive call is rejected by the guard condition.
You can get rid of this problem by writing the definition with simple patterns:
Coq < Fixpoint last [n:nat; l:(listn n)] : nat :=
Coq < <[_:nat]nat>Cases l of
Coq < (consn m a x) => Cases x of niln => a | _ => (last m x) end
Coq < | niln => O
Coq < end.
last is recursively defined