Reduction stack overflow when using "coerce"

Here's an interesting program that tries to coerce an operation to operate on a newtype:

module T24315 where

import Data.Coerce

type Heap τ = Int -> Maybe (τ ())
newtype ProcessM τ a = ProcessM (Heap (ProcessM τ) -> τ (a, Heap (ProcessM τ)))

newtype NewProcessM τ a = NewProcessM (ProcessM τ a)

runM :: ProcessM τ a -> τ (a, Heap (ProcessM τ))
runM (ProcessM f) = f (const Nothing)

runM2 :: NewProcessM τ a -> τ (a, Heap (NewProcessM τ))
runM2 = coerce runM

GHC 9.4 and GHC 9.9 report an error on that coerce:

test.hs:14:9: error: [GHC-40404]
    • Reduction stack overflow; size = 201
      When simplifying the following type: ProcessM τ ()
    • In the expression: coerce runM
      In an equation for ‘runM2’: runM2 = coerce runM
    Suggested fix:
      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
   |
14 | runM2 = coerce runM
   |         ^^^^^^

I would not have expected this error message; in fact I would have expected that the coercion Just Works (it does not, for good reason below). Though admittedly, this is a gnarly type.

End of bug report.

---

Further diagnosis:

When I change ProcessM to a datatype, I'm getting a much nicer error:

test.hs:14:9: error: [GHC-18872]
    • Couldn't match representation of type: τ (a, Heap (ProcessM τ))
                               with that of: τ (a, Heap (NewProcessM τ))
        arising from a use of ‘coerce’
      NB: We cannot know what roles the parameters to ‘τ’ have;
        we must assume that the role is nominal
    • In the expression: coerce runM
      In an equation for ‘runM2’: runM2 = coerce runM
    • Relevant bindings include
        runM2 :: NewProcessM τ a -> τ (a, Heap (NewProcessM τ))
          (bound at test.hs:14:1)
   |
14 | runM2 = coerce runM
   |  

Aha, so I need to add a role annotation.

type role ProcessM representational nominal

But this is rejected for a different reason

test.hs:9:1: error: [GHC-29178]
    • Role mismatch on variable τ:
        Annotation says representational but role nominal is required
    • while checking a role annotation for ‘ProcessM’
  |
9 | type role ProcessM representational nominal
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

That is probably due to the Fixpoint; fair enough. I'd still expect the original program to emit a useful error.