> My suggestion is to use --sized-types Yes, I'm aware of that possibility, but it feels like a lot of boilerplate to get something other languages offer out-of-the-box. As a user I'd just like to see a better termination checker :-) Janek