About the relationship between non-termination and inconsistency?

I've been trying to get into Agda and I noticed that it doesn't have recursion, which implies that it isn't Turing-Complete.

From what I could understand, if Agda had recursion, it would make itself an inconsistency from a type theory perspective.

Something stuck to my mind: Is it possible to exist a language that it isn't strongly normalizing but, yet, consistent? Or does the existence of recursion mandatorily implies inconsistency?

Some trivial type systems

Let the set of types be $\bot,\top$ and the sets of terms be $a,b$, with typing rules

$$
\vdash a:\top \qquad \vdash b:\top
$$
and computational rules
$$
a \to b \qquad b \to a
$$

Then, the resulting system has no (weakly/strongly) normalizing terms, yet it is consistent since no term inhabits $\bot$.

We can also allow recursion on $\top$, if we want.

$$
\dfrac{
\Gamma, x:\top \vdash e:\top
}{
\Gamma \vdash {\sf rec}\ x. e\ :\top
}
$$
with the obvious computational rule
$$
{\sf rec}\ x. e \to e\{{\sf rec}\ x. e/x\}
$$

On adding full recursion

Of course, we can't allow unrestricted recursion on $\bot$, otherwise ${\sf rec}\ x.x:\bot$ leads to an inconsistency.

Adapting more serious type systems

If we take any strongly normalizing typed lambda calculus, we can modify the computational rules to add a silly reduction step
$$
t\to t
$$
for any term $t$.

The new calculus has as inhabited types the same inhabited types, so it preserves consistency. The calculus is not even weakly normalizing, though.

StackExchange Computer Science Q#97836, answer score: 4