[Agda] Absurd catch all pattern

[Nils Anders Danielsson]

On 2010-03-04 21:14, Andreas Abel wrote:
> Is it thinkable to get this accepted?

Perhaps it would even be possible to get the following code accepted:

  _≟_ : (x y : Bool) → Dec (x ≡ y)
  true  ≟ true  = yes refl
  false ≟ false = yes refl
  _     ≟ _     = no (λ ())

If overlapping underscores/variables were sugar for "all the missing
cases", then the code above would be shorthand for the following,
type-correct code:

  _≟_ : (x y : Bool) → Dec (x ≡ y)
  true  ≟ true  = yes refl
  false ≟ false = yes refl
  true  ≟ false = no (λ ())
  false ≟ true  = no (λ ())

Ulf and I have discussed this in the past. There are some issues:

• How, exactly, would "all the missing cases" be defined? Perhaps a
  definition falls out nicely from the algorithm for type checking
  patterns.

• If the original code type checks, then it seems inefficient to expand
  it, so perhaps one should first try to type check the unexpanded code.
  I am not certain that expansion always preserves typability, though
  (it may be easier to instantiate some meta-variable before expansion).

• One would need to make sure that error messages which refer to
  expanded cases are not incomprehensible.

--
/NAD