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.