I should probably mention that I ran into this after Peter Morris talked about strictly positive families, i.e. GADTS that cannot encode recursion in this way. I was curious what this recursion encoding would look like, and was pretty startled when GHC didn’t terminate. I would expect them to limit the number of inline steps to avoid this kind of behaviour.

I don’t entirely agree that this is a completely artificial example. Imagine writing a lambda calculus interpreter using higher-order abstract syntax. If you’re not careful, you can’t write the y-combinator without your compiler diverging:

rec f = Lam (\x -> f `apply` (x `apply` x))

y = Lam (\f -> (rec f) `apply` (rec f))

Having a compiler loop is somehow wrong, even if the example is contrived.

Of course, turning off inlining for apply will fix the problem. You can do that with the pragma:
{-# NOINLINE apply #-}

It would be nice if they could detect and avoid problems of this sort, though I doubt that finding a cleverly efficient solution is a terribly high priority on anyone’s list, seeing as such types only seem to occur in programs contrived to make the compiler unhappy. The problem occurs with recursive types which occur contravariantly (i.e. as function parameters) in their own definition — detecting this directly isn’t entirely trivial due to parametric and mutually recursive types.