[isaac21259]

Dependent type systems don't deal well with non termination. In general you can't prove a program will or won't terminate. The solution is to disallow recursion except through a few eliminators which do recursion in a well founded way that is guaranteed to halt.

The reason they don't work well with recursion is you could have something like: false :: _|_ false = false

Where false is a function we are defining of the uninhabited type.

For more complicated versions stuff like this see Girard's paradox.

[johnbender]

> In general you can't prove a program will or won't terminate.

As a point of clarity for folks who come to this (the commenter clearly knows this) one can’t _automatically_ prove for an arbitrary program whether or not it terminates. It’s definitely possible to prove this manually per program and most dependently typed languages will do the work for you as a matter of sound over approximation as long as one of the arguments is shrinking in an obvious way.