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.