[GHC] #8503: New GeneralizedNewtypeDeriving check still isn't permissive enough

[GHC]

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough
-------------------------------------+------------------------------------
        Reporter:  goldfire          |            Owner:  goldfire
            Type:  bug               |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.7
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by goldfire):

 This is subtler than I thought.

 Let's take a simple case:

 {{{
   class C m where
     meth :: m (m a)

   instance C Maybe where
     meth = Nothing

   newtype NT a = MkNT (Maybe a)
     deriving C
 }}}

 In the derived instance for `C NT`, we need this:

 {{{
 $meth_C_NT = $meth_C_Maybe |> co
   where
     co :: forall (a :: *). Maybe (Maybe a) ~R# NT (NT a)
 }}}

 What is `co`? Ideally, it would be

 {{{
 co = forall (a :: *). Sym NTCo:NT[0] (Sym NTCo:NT[0] <a>)
 }}}

 but that doesn't role-check! `NTCo:NT[0]` has type `NT ~R# Maybe`. But, to
 apply that coercion to another requires an `AppCo`, which in turn requires
 its second argument to have a nominal role.  The underlying problem here
 is essentially that eta-reducing the newtype coercion loses information
 about the roles of its parameters. After all, if `Maybe`'s parameter were
 at a nominal role, then this deriving would be bogus. By eta-reducing,
 we're forgetting that `Maybe`'s parameter's role is other than nominal.

 What to do? One possible solution is to allow `AxiomInstCo` to be
 oversaturated, and then role information could be stored in an axiom
 (indeed, role information for all non-eta-reduced parameters is already
 there). This isn't a terrible plan, but perhaps it has further
 ramifications that I'm not currently seeing.

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