Def is used for both defined and undefined constants.
Assume there is a type declaration and a definition for
every constant, even if the definition is an empty
list of clauses.
A clause is a list of patterns and the clause body should Bind or
NoBind in the order the variables occur in the patterns. The NoBind
constructor is an optimisation to avoid substituting for variables that
aren't used.
The telescope contains the types of the pattern variables and the
permutation is how to get from the order the variables occur in the
patterns to the order they occur in the telescope. For the purpose of the
permutation dot patterns counts as variables.
TODO: change this!
Patterns are variables, constructors, or wildcards.
QName is used in ConP rather than Name since
a constructor might come from a particular namespace.
This also meshes well with the fact that values (i.e.
the arguments we are matching with) use QName.