Generate absurd clauses

At the moment, a case that is later detected to be absurd by a match on later arguments, triggers an exhaustiveness error when splitting on former arguments. For an example, consider the following definition of a countdown stream:

negative family CStream : Type where
  case head : (this : CStream) → Natural
  case tail : (this : CStream) -> { m : Natural } -> (eq : Equality (head this) (successor m)) -> CStream

When we now consider the pattern match on the first argument of countdown, we can observe that the case for n = Zero is missing. This is, however, not because n = Zero itself is impossible at this point. For this reason, elaboration reports an error that the match on n is not exhaustive. Although, in practice, this case cannot happen, because we later match on the equality that is part of the tail projection, we have to add it in order to silent the error message.

define countdown : (n : Natural) -> CStream where
  case CStream.head (countdown             n)                      => n
  case CStream.tail (countdown (successor p)) Equality.reflexivity => countdown p

With the missing case for n = Zero added, the error does not show up and since the third clause is absurd now, its body is not elaborated and hence this is absurd is neither resolved nor not type checked.

define countdown : (n : Natural) -> CStream where
  case CStream.head (countdown             n)                      => n
  case CStream.tail (countdown (successor p)) Equality.reflexivity => countdown p
  case CStream.tail (countdown          Zero) Equality.reflexivity => this is absurd

While this is logically consistent (i.e., we may conclude anything under wrong premises), it is inconvenient as the user has to provide a case that can never match. The best solution would be to generate an absurd clause for each case (i.e., constructor) at the end of the user definition. When the user pattern is exhaustive, we never reach these clauses. Otherwise, if the user left out some cases (as in the example above), we would reach such an absurd clause and must check if it is really absurd. Only if there is a synthesized absurd clause that is not really absurd, we report an exhaustiveness error.

Technically, we can generate such clauses by copying the existing clauses when performing a split (with all their remaining constraints) and marking them as absurd.