[Agda] A feature request: typed pattern synonyms.

[Roman]

Thanks for your suggestion, Yorick. It's a great trick to get nice
case splitting, but having two data types (described lists and a view
for them) seems more heavy than two versions of constructors and
requires a lot more code to change. Currently, to type check the
contents of Data.List.Base after replacing the definition of `List`
with its generic counterpart I need only to rename constructors
(that's yet another problem: different patterns can't have the same
name unlike constructors) and then rename again (patterns to typed
functions) when there are unsolved metas.