[Agda] Pattern matching on irrelevant types with only one constructor?

[Matthew Daggitt]

 In the Agda documentation
<https://agda.readthedocs.io/en/v2.6.0/language/irrelevance.html> it is
pretty clear that the only time you can pattern match against irrelevant
arguments is when the type is empty. My own reasoning for this has always
been that this is to stop decisions being made depending on the result of
the pattern match. This leads me to wonder if there are any theoretical
reasons why it's not possible to also mark a type irrelevant when it only
has a single constructor?

Consider the motivating example below. Clearly the `Acc` argument is never
actually used in the computation of the final value, and no decisions can
be based on its value as it only has a single constructor. It seems like it
should be possible to mark it irrelevant. If this were possible then we
would immediately get rid of a whole bunch of annoying congruence lemmas.
```
gcd : (m n : ℕ) → Acc _<_ m → n < m → ℕ
gcd m zero     _         _   = m
gcd m (suc n) (acc rec) n<m = gcd′ (suc n) (m % suc n) (rec _ n<m) (a%n<n m
n)
```
Many thanks,
Matthew
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190501/ec867ecf/attachment.html>