Post #1810079

@zwarich@hachyderm.io This is the classic exemplar, and there's many more: https://github.com/agda/agda/issues/1201#issuecomment-438741785 My point here is that sized types were inspired by a desire to allow reason about termination of Haskell-style code, where you just have to add some annotations to the types but you shouldn't have to change the code itself very much. The issue is that this is actually a very hard problem, and the designers bit off more than they were equipped to chew — and then went and wrote tons of code using the broken version, and have been stonewalling its removal since forever as a result.