Suppose we set $$\mathbb{M} \alpha := r \to \alpha$$, where $$r$$ is some fixed type, and $$\alpha$$ an arbitrary type, of the STLC (Simply-Typed Lambda Calculus)

Suppose we want to define a co-monad, which contains Co-unit and Co-join, with the following types (where $$\mathbb{M}$$ binds more tightly than $$\to$$ and $$\mathbb{M}$$ is as stated above):

1. Co-unit $$\;\;\;\; \mathbb{M} \alpha \to \alpha$$
2. Co-join $$\;\;\;\;\mathbb{M}\mathbb{M} \alpha \to \mathbb{M} \alpha$$

I have been told that this will not work and that we could not create a co-monad in this way, since there is no terminating implementation for the type $$(e \to a) \to a$$.

But in the pure STLC all terms are "terminating"(i.e, reductions always lead to a (unique) normal form). So I don’t understand how this comment can be relevant in the case of the STLC.