A dependently typed system (or presumably anything else) which allows non-halting definitions is unsound. The classic example is an infinite loop:

loop = loop

What is the type of `loop`? We can infer it by starting with a completely generic type variable, e.g. `forall t. t`:

loop : forall t. t
loop = loop

Then we can look at the type of the body to see which constraints it must satisfy, and perform unification with that and the `t` we have so far. In this case the body is `loop` which has type `forall t. t` (i.e. which is completely unconstrained). Unifying `forall t. t` with `forall t. t` gives (unsurprisingly) `forall t. t`. Hence that is the type of `loop`. Yet this claims to hold for all types `t`, which must include empty types like `Empty`, which should have no values!

data Empty where
-- This page intentionally left blank

loop : forall t. t
loop = loop

myEmptyValue : Empty
myEmptyValue = loop

In particular, this lets us "prove" (in an invalid way) things like the Collatz conjecture. Here's a quick definition of the Collatz sequence, in Agda/Idris notation (untested):

-- Peano arithmetic
data Natural where
Zero : Natural
Succ : Natural -> Natural

one = Succ Zero

halve : Natural -> Natural
halve Zero = Zero
halve (Succ Zero) = Succ Zero -- Should never reach this; included for completeness
halve (Succ (Succ n)) = Succ (halve n)

threeTimes : Natural -> Natural
threeTimes Zero = Zero
threeTimes (Succ n) = Succ (Succ (Succ (threeTimes n)))

data Boolean where
True : Boolean
False : Boolean

not : Boolean -> Boolean
not True = False
not False = True

ifThenElseNat : Boolean -> Natural -> Natural -> Natural
ifThenElseNat True x y = x
ifThenElseNat False x y = y

isEven : Natural -> Boolean
isEven Zero = True
isEven (Succ n) = not (isEven n)

collatzStep : Natural -> Natural
collatzStep Zero = one -- Again, only for completeness
collatzStep (Succ n) = ifThenElseNat (isEven (Succ n))
(halve (Succ n))
(Succ (threeTimes (Succ n)))

-- This won't be allowed by Agda/Idris since it may or may not halt ;)
collatzLoop : Natual -> Natural
collatzLoop Zero = collatzLoop (collatzStep Zero) -- For completeness
collatzLoop (Succ Zero) = Succ Zero -- Halt
collatzLoop (Succ (Succ n)) = collatzLoop (collatzStep (Succ (Succ n)))

We can then define the Collatz conjecture, using a standard encoding of equality:

data Equal : Natural -> Natural -> Type where
reflexivity : (n : Natural) -> Equal n n

CollatzConjecture : Type
CollatzConjecture = (n : Natural) -> Equal (collatzLoop n) one

proofOfCollatzConjecture : CollatzConjecture
proofOfCollatzConjecture = ?

disproofOfCollatzConjecture : CollatzConjecture -> Empty
disproofOfCollatzConjecture purportedProof = ?

The disproof basicallys says "if you give me a proof of `CollatzConjecture`, I can give you a value which doesn't exist"; since that's absurd, the only way it can hold is if there are no proofs of `CollatzConjecture` to give it (this is a form of proof by contradiction: give me a supposed proof, and I'll show you why it must be wrong).

The problem with allowing non-terminating recursion is that we can use `loop` to fill in either of these proofs, or even both of them!

proofOfCollatzConjecture : CollatzConjecture
proofOfCollatzConjecture = loop

disproofOfCollatzConjecture : CollatzConjecture -> Empty
disproofOfCollatzConjecture purportedProof = loop

The type of `loop` is `forall t. t`, which can unify with either of these types, so the language/logic will allow us to use it in these definitions (or anywhere else, for that matter).

For this reason, we have to make sure our language isn't Turing-complete, which we can do using a "totality checker" (a static analyser which checks if our definitions halt: if they definitely do, they're permitted; if they don't or we can't tell, they're forbidden). That stops us from writing things like `loop`, but unfortunately it stops us from writing `collatzLoop` as well.

One way to get around this is to use "corecursion". This lets an infinite loop pass the totality checker, as long as it's definitely producing output data as it goes (e.g. like a stream which is forbidden from getting "stuck"). We can use this to make a `Delayed` type, which is just a stream of dummy data which might or might not end (a polymorphic version of this is described in more detail at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html ):

data Delayed : Type where
Now : Natural -> Delayed
Later : Delayed -> Delayed

collatzLoop : Natural -> Delayed
collatzLoop Zero = Later (collatzLoop (collatzStep Zero)) -- For completeness
collatzLoop (Succ Zero) = Now (Succ Zero) -- Halt
collatzLoop (Succ (Succ n)) = Later (collatzLoop (collatzStep (Succ (Succ n))))

This will pass the totality checker since each step is guaranteed to produce some data (either the `Now` symbol or the `Later` symbol); even though the contents of a `Later` value may be infinite! If we run this version of `collatzLoop` on, say, 6 (ignoring the `Zero`/`Succ` notation for brevity), we get:

collatzLoop 6
Later (collatzLoop 3)
Later (Later (collatzLoop 10))
Later (Later (Later (collatzLoop 5)))
Later (Later (Later (Later (collatzLoop 16))))
Later (Later (Later (Later (Later (collatzLoop 8)))))
Later (Later (Later (Later (Later (Later (collatzLoop 4))))))
Later (Later (Later (Later (Later (Later (Later (collatzLoop 2)))))))
Later (Later (Later (Later (Later (Later (Later (Later (collatzLoop 1))))))))
Later (Later (Later (Later (Later (Later (Later (Later (Now 1))))))))

We can rephrase the Collatz conjecture as saying that the return value of `collatzLoop` will always, eventually, end with `Now one`. This is an existence proof: there exists an `n : Natural` such that after `n` layers of `Later` wrappers there will be a `Now one` value. Since we're dealing with constructive logic, to prove this existence we must construct the number `n` (e.g. using some function, which I'll call `boundFinder`):

unwrap : Natural -> Delayed -> Delayed
wrap Zero x = x
wrap (Succ n) (Now y) = Now y
wrap (Succ n) (Later y) = unwrap n y

data DelayEqual : Delayed -> Delayed -> Type where
delayedReflexivity : (d : Delayed) -> DelayEqual d d

-- The notation `(x : y *** z)` is a dependent pair, where the first element has
-- type `y` and the second element has type `z` which may refer to the first
-- value as `x`
CollatzConjecture : Type
CollatzConjecture = (boundFinder : Natural -> Natural ***
(n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one))

proofOfCollatzConjecture : CollatzConjecture
proofOfCollatzConjecture = ?

disproofOfCollatzConjecture : CollatzConjecture -> Empty
disproofOfCollatzConjecture (boundFinder, purportedProof) = ?

With this definition, a value of type `CollatzConjecture` will be a proof of the Collatz conjecture. Since we can't use tricks like `loop`, we're forced to actually construct a value of the required type. This value will be a pair: the first element of the pair is a function of type `Natural -> Natural`, which we call `boundFinder`. The second element of the pair is also a function, but it has type:

(n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one))

This says that given any `n : Natural`, we can return a proof that:

DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one))

This says that `unwrap (boundFinder n) (collatzLoop n)`, i.e. removing `boundFinder n` layers of `Later` wrappers from `collatzLoop n`, is equal to the value `Now one`.

To disprove this form of the Collatz conjecture, we're given a supposed proof: i.e. we're given some `boundFinder` function and a value supposedly proving the equation described above. We need to find a contradiction to that supposed proof, which might be an `n : Natural` which reduces to `Now x` where `x` is not 1; or which we can show doesn't reduce at all. Either way this would contradict the claim made by `purportedProof`, and we could use that contradiction to prove anything ("ex falso quodlibet") including the `Empty` return value we need (just as if we had `loop`!).

The thing is, even if we set up all of this machinery, there is an unfortunate fact staring us in the face: compare the definition of `Natural` to the definition of `Delayed`. They're almost identical! The only difference is that `Now` takes an argument but `Zero` doesn't. If we think about what `Succ` is doing, it's just adding a wrapper around a `Natural` to represent "one more than" (e.g. `Succ Zero` is 1, `Succ (Succ Zero)` is 2, etc.). If we think about what `Later` is doing, it's just adding a wrapper around a `Delayed` to represent "one more step". In essence we've just traded one form of counting for another! It doesn't actually get us any closer to solving the Collatz conjecture, other than giving us something to plug a proof attempt into, such that it will be verified automatically. It's like setting up a Wordpress blog: it lets us say anything we like to the world, but doesn't help us figure what we want to say ;)