So the problem is that there are too many useful programs which can't be expressed in a practically decidable form, or there's no clear way to get from a form that isn't to a similar-enough form that would be, like knowing what strategies ghc uses to narrow the search space or something?