[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):

 Hold the phone! There is an easier solution to the original problem!

 In my first comment, I wanted a coercion `co :: forall (a :: *). Maybe
 (Maybe a) ~R NTMaybe (NTMaybe a)`, and then I proposed a possible value of
 that type that was ill-roled. But, here is a well-roled value:

 {{{
 co = co1 ; co2

 co1 :: forall (a :: *). Maybe (Maybe a) ~R Maybe (NT a)
 co1 = forall (a :: *). Maybe (sym NTCo <a>_N)

 co2 :: forall (a :: *). Maybe (NT a) ~R NT (NT a)
 co2 = forall (a :: *). sym NTCo <NT a>_N
 }}}

 If we convert the pieces one at a time and then use transitivity, we're
 all OK. I remember battling against this problem over the summer.

 So, now we have a new question: how to get GHC to find this solution?
 Luckily, we happen to have a solver lying around that does just that: the
 `Coercible` mechanism. I imagine we could get the GND code to just call
 the `Coercible` code for each method. In fact, I considered this approach
 when improving the GND mechanism a few weeks ago, but thought it was
 overkill.

 My guess is that this would Just Work, when implemented. It might simplify
 the code a bit, too, but be somewhat less efficient (at compile time) at
 doing GND. I think this is reasonable.

 Taking the idea a bit further, what if the `Coercible` mechanism can't
 derive a coercion for a particular method? It would have to produce
 unsolved `Coercible` constraints... which we could just add to the
 constraints on the GND instance! This would allow more GND's to work than
 we had hoped for, such as this example:

 {{{
 type family F a
 class C a where
   meth :: a -> F a

 type instance F Int = Bool
 class C Int where
   meth = (> 0)

 type instance F Age = Bool
 newtype Age = MkAge Int
   deriving C      -- just works, no extra constraints because F Age = F
 Int

 type instance F [a] = a
 class C [a] where
   meth = head

 type instance F (List a) = Int
 newtype List a = MkL [a]
   deriving C     -- this would create an instance with head "instance
 (Coercible a Int) => C (List a) where ..."
 }}}

 This all seems quite reasonable behavior, though we would want to make
 sure we don't produce constraints like `Coercible Int Bool`.

 Thoughts? Is this a good plan? We could always, as a first pass, implement
 GND in terms of `Coercible` and fail if there are any unsolved
 constraints, working for `C Age` above but not `C (List a)`.

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