General recursion for non-coinductive types

Hello,

I'm working on a translation from the calculus of constructions to static single assignment form (then I'll move further to typed assembly). As of now, all SSA programs halt (as expected, since all CoC programs halt).

Though I've got some insight from [this paper](http://lmcs.episciences.org/2265/pdf), I'm still not sure how I'll properly model general recursion (then I assume I'll need one single intrinsic function `iter` which loops over a coinductive type forever, or until it halts). I'm still confused with that, though.

I'd like to ask how you picture implementing that. Let's assume a Haskell to Morte compiler. A simple recursive function:

```haskell
fib :: Int -> Int
fib n = if n < 2 then
return 1
else
fib (n - 1) + fib (n - 2)
````

Or even a mutually recursive function (also assume it's taken from source code, and we can't know if it halts):

```haskell
is_even :: Int -> Bool
is_even n = if n == 0 then
True
else
is_odd (n - 1)

is_odd :: Int -> Bool
is_odd n = if n == 0 then
False
else
is_even (n - 1)
```

So, neither Int nor Bool are coinductive types... Do you have any insight on that?
(The article claims partiality with coinductive types is a monad. I'm not sure I understood how; I don't know category theory. 😢)