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.
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.