GND accepts ill-roled coercion when manually defining it won't typecheck
I wanted to see what error message might result from adding join
to Monad
and trying to derive it via GeneralizedNewtypeDeriving
, so I used this code to simulate it:
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# OPTIONS_GHC -ddump-deriv #-}
module CoerceJoin where
import qualified Control.Monad (join)
import Data.Coerce (coerce)
class MyMonad m where
join :: m (m a) -> m a
instance MyMonad Maybe where
join = Control.Monad.join
newtype MyMaybe a = MyMaybe (Maybe a) deriving MyMonad
To my surprise, this actually compiles:
==================== Derived instances ====================
Derived instances:
instance CoerceJoin.MyMonad CoerceJoin.MyMaybe where
CoerceJoin.join
= GHC.Prim.coerce
(CoerceJoin.join ::
GHC.Base.Maybe (GHC.Base.Maybe a_axs) -> GHC.Base.Maybe a_axs) ::
forall (a_axs :: *).
CoerceJoin.MyMaybe (CoerceJoin.MyMaybe a_axs)
-> CoerceJoin.MyMaybe a_axs
Generic representation:
Generated datatypes for meta-information:
Representation types:
That seemed really odd, given my understanding of roles, so I tried to implement this instance manually:
newtype MyMaybe a = MyMaybe (Maybe a)
instance MyMonad MyMaybe where
join = coerce (join :: Maybe (Maybe a) -> Maybe a) :: MyMaybe (MyMaybe a) -> MyMaybe a
And now GHC will reject it:
CoerceJoin.hs:18:10:
Couldn't match representation of type `a0' with that of `a1'
`a1' is a rigid type variable bound by
an expression type signature: MyMaybe (MyMaybe a1) -> MyMaybe a1
at CoerceJoin.hs:18:10
arising from trying to show that the representations of
`Maybe (Maybe a0) -> Maybe a0' and
`MyMaybe (MyMaybe a1) -> MyMaybe a1' are the same
Relevant role signatures:
type role Maybe representational
type role MyMaybe representational
In the expression:
coerce (join :: Maybe (Maybe a) -> Maybe a) ::
MyMaybe (MyMaybe a) -> MyMaybe a
In an equation for `join':
join
= coerce (join :: Maybe (Maybe a) -> Maybe a) ::
MyMaybe (MyMaybe a) -> MyMaybe a
In the instance declaration for `MyMonad MyMaybe'
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | goldfire |
Operating system | |
Architecture |