[GHC] #11152: GND accepts ill-roled coercion when manually defining it won't typecheck

1 Dec 2015


      #11152: GND accepts ill-roled coercion when manually defining it won't typecheck
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC accepts
  Unknown/Multiple                   |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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:

 {{{#!hs
 {-# 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:

 {{{#!hs
 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'
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11152
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler