[GHC] #8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles

[GHC]

#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type
roles
-------------------------------------+-------------------------------------
              Reporter:  haasn       |            Owner:
                  Type:  feature     |           Status:  new
  request                            |        Milestone:
              Priority:  normal      |          Version:  7.8.1
             Component:  Compiler    |         Keywords:
  (Type checker)                     |     Architecture:  Unknown/Multiple
            Resolution:              |       Difficulty:  Unknown
      Operating System:              |       Blocked By:
  Unknown/Multiple                   |  Related Tickets:
       Type of failure:              |
  None/Unknown                       |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Refactoring in my branch has added a small wrinkle here: my version
 currently ''accepts'' the original code.

 Let's be concrete:

 {{{
 {-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving #-}
 module T8984 where

 class C a where
     app :: a (a Int)

 newtype N cat a b = MkN (cat a b)  deriving( C )
 }}}

 yields an instance

 {{{
 instance (Coercible (cat a (N cat a Int)) (cat a (cat a Int)), C (cat a))
 => C (N cat a)
 }}}

 This is actually perfectly sound: GHC is just choosing to abstract over
 the unprovable `Coercible` constraint. What do we think of this behavior?
 Is it desired or not? This seems to be a free choice here: I don't think
 either option or the other would affect much else.

 Implementation note: This is a direct consequence of changes to
 `TcValidity.validDerivPred`. Previously (that is, in today's HEAD), a
 `Coercible` constraint looked like a class constraint, meaning it was
 checked to make sure that it wasn't too exotic. In my branch, (`wip/rae-
 new-coercible`) `Coercible` constraints are like equalities, which are
 allowed unchecked. Thus, the rather exotic constraint above is allowed.

 This has all gotten me thinking: Why ''do'' we blithely allow equality
 constraints to be in a derived-inferred context? This ability was added in
 response to #6088, where the user wanted to use GND to derive an instance
 based on another instance with an explicit equality in the context. Here
 is the example from #6088:

 {{{
 class C a

 newtype A n = A Int

 type family Pos n
 data True

 instance (Pos n ~ True) => C (A n)


 newtype B n = B (A n)
    deriving (C)
 }}}

 This is now accepted.

 However, here is a very similar case:

 {{{
 class C1 a b
 class C2 a

 instance C1 a a => C2 (Maybe a)

 newtype N a = MkN (Maybe a)
   deriving C2
 }}}

 This second case is rejected. And yet, they're similar in that the exotic
 context that might be inferred is specified by the user. It seems a little
 odd to accept one and reject the other.

 So, I propose the following behavior:
  * Reject equality constraints to be inferred for `deriving`.
  * If `deriving` failed solely because of checks in `validDerivPred`,
 provide the full inferred context in the error message to make it easy for
 users to work around this restriction.

 This would, essentially, break the fix for #6088, and would thus be a
 regression, because 7.8 incorporates the #6088 fix. But, with the enhanced
 error message, the breakage would be easy to fix. What do folks think?

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