[GHC] #8827: Inferring Safe mode with GeneralizedNewtypeDeriving is wrong

[GHC]

#8827: Inferring Safe mode with GeneralizedNewtypeDeriving is wrong
-------------------------------------+------------------------------------
        Reporter:  goldfire          |            Owner:
            Type:  bug               |           Status:  new
        Priority:  normal            |        Milestone:  7.8.1
       Component:  Compiler          |          Version:  7.8.1-rc2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:  8226, 8745
-------------------------------------+------------------------------------

Comment (by ekmett):

 {{{
 deriving Coercible a b => Coercible (Map k a) (Map k b)
 }}}

 is somewhat in line with what I've been playing around with to try to work
 out how we can lift coercions over complex data types.

 e.g.

 {{{
 class Representational (t :: k1 -> k2) where
   rep :: Coercion a b -> Coercion (t a) (t b)
   default rep :: Phantom t => Coercion a b -> Coercion (t a) (t b)
   rep _ = phantom

 class Representational t => Phantom t where
   phantom :: Coercion (t a) (t b)
   default phantom :: Coercible (t a) (t b) => Coercion (t a) (t b)
   phantom = Coercion
 }}}

 Then easy cases we can already handle work:

 {{{

 instance Representational Proxy
 instance Phantom Proxy

 instance Representational Tagged
 instance Phantom Tagged
 instance Representational (Tagged a) where rep Coercion = Coercion

 instance Representational Const where rep Coercion = Coercion
 instance Representational (Const a)
 instance Phantom (Const a)

 instance Representational Coercion     where rep = unsafeCoerce
 instance Representational (Coercion a) where rep Coercion = Coercion

 instance Representational (->)       where rep Coercion = Coercion
 instance Representational ((->) a)   where rep Coercion = Coercion
 }}}

 But with a few helpers

 {{{
 coerce1 :: Coercible a b => Coercion a c -> Coercion b c
 coerce1 = coerce

 coerce2 :: Coercible b c => Coercion a b -> Coercion a c
 coerce2 = coerce

 -- from Control.Lens as a placeholder
 new :: (Rewrapping s t, Coercible (Unwrapped s) s, Coercible (Unwrapped t)
 t) => Coercion (Unwrapped s) (Unwrapped t) -> Coercion s t
 new = coerce1 . coerce2

 -- I don't see how to implement this one directly
 eta :: forall (f :: x -> y) (g :: x -> y) (a :: x). Coercion f g ->
 Coercion (f a) (g a)
 eta = unsafeCoerce
 }}}

 we can write several hard cases that are currently beyond our reach:

 {{{
 instance (Representational f, Representational g) => Representational
 (Compose f g) where
   rep = new.rep.rep

 instance Representational m => Representational (StateT s m) where
   rep = new.rep.rep.eta.rep

 instance Representational m => Representational (ReaderT e m) where
   rep = new.rep.rep

 instance Representational m => Representational (WriterT w m) where
   rep = new.rep.eta.rep
 }}}

 Then instead of lifting `Coercible a b`  into `Coercible (f a) (f b)`
 based on the role of f's next argument, it'd lift using the
 `Representational` instance.

 I'd been mostly exploring this as a straw man, but if we're throwing 'big
 changes' into the discussion, I felt it worth mentioning as a direction.

 Mind you the code I have above is implementable and implemented with the
 existing `Coercible` machinery.

 It isn't perfect though, e.g. I don't know a better way to implement

 {{{
 instance Representational f => Representational (Compose f) where
   rep = unsafeCoerce
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8827#comment:31>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler