Well, if you throw the halting problem at it then all of your static analysis goes away since you can use general recursion to write arbitrarily typed expressio

Well, if you throw the halting problem at it then all of your static analysis goes away since you can use general recursion to write arbitrarily typed expressions. That's why things like Idris have termination checkers.