As allways, I forgot to forward the message to the list, but the Conor
response makes it irrelevant:
---------- Forwarded message ----------
From: Alberto G. Corona
Seriously, I love undecidable instances, but there's gotta be a way to make type-level programming less painful. GHC team: please give us type-level integers that don't suck! If I ever have to see S (S (S (S Z))) again it's too soon.
I´m starting to read about dependent types and it´s very promising. Maybe my suggestion makes sense: is to "compress" recursive types such are S(S(S(S Z))) into internal compiler representations S <n> Z. This would type match faster and will generate much more clear and compact compilation errors.