13.7 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)
-
The constructor ident expects num arguments
- The variable ident is bound several times
in pattern term
- Found a constructor of inductive type term
while a constructor of term is expected
- the pattern matching is not exhaustive
-
Non exhaustive pattern-matching
- 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
- there is a type mismatch between the different branches
-
Unable to infer a Cases predicate
Either there is a type incompatiblity or the problem involves
dependencies
Then the user should provide an elimination predicate.