Non-termination, strict positivity and free monads
Using Free, you can have a HOAS embedding of the untyped lambda calculus. And then write a structurally recursive function firing the top-level redex again and again. Good luck trying to normalise reduce omega.

{-# NO_POSITIVITY_CHECK #-}
data Free (f : Set → Set) (a : Set) : Set where
  Pure : a → Free f a
  Roll : f (Free f a) → Free f a

data LAMF (T : Set) : Set where
  App : T → T → LAMF T
  Lam : (T → T) → LAMF T

LAM : Set → Set
LAM = Free LAMF

pattern `lam b   = Roll (Lam b)
pattern `app f t = Roll (App f t)

data ⊥ : Set where

-- Type of closed term: LAM ⊥

delta : LAM ⊥
delta = `lam λ x → `app x x

omega : LAM ⊥
omega = `app delta delta

reduce : ∀ {A} → LAM A → LAM A
reduce (`app (`lam b) t) = reduce (b t)
reduce t = t