[GHC] #11732: Deriving Generic1 interacts poorly with TypeInType

[GHC]

#11732: Deriving Generic1 interacts poorly with TypeInType
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:  TypeInType,
                                     |  Generics
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Richard's consultation is [https://mail.haskell.org/pipermail/ghc-
 devs/2016-March/011631.html this email thread].

 Just to be clear to everyone else, we are discussing
 {{{
    data P1   (a :: k) = MkP1 deriving Functor
    data P2 k (a :: k) = MkP2 deriving Functor
 }}}
 Here `P2` has an explicit kind arg, which must appear in any use of `P2`;
 thus
 {{{
    f :: P2 * Int -> Bool
 }}}
 The question before the house is whether to reject either or both
 'deriving' clauses, on the grounds that both instantiate 'k'; and ask for
 a stand-alone deriving declaration instead.  Or we could accept either or
 both, getting
 {{{
   instance Functor (P1 (a :: *))
   instance Functor (P2 * (a ::*))
 }}}
 In principle we could say Yes/Yes, Yes/No, or No/No to the two cases.

 As Richard points out, a 'deriving' clause attached to a 'data' decl
 infers some instance context.  That context must be written explicitly in
 a standalone deriving declaration. For example:
 {{{
   data Maybe a = Nothing | Just a deriving( Eq )
 }}}
 we get the derived instance
 {{{
   instance Eq a => Eq (Maybe a ) where
     (==) x y = ...blah...
 }}}
 The `Eq a` context in this instance declaration is magically inferred from
 the form of the data type declaration.  This inference process gets pretty
 tricky for Functor and Traversable. To use the instance declarations you
 have to understand what the inferred instance context is; GHC should
 really provide a way to tell you.

 Richard points out (later in the thread) that "instantiating k" is like
 adding a constraint `k ~ *` to the instance, thus
 {{{
   instance (k ~ *) => Functor (P1 (a :: k))
 }}}
 That's not quite true, because this instance will match for any k, and
 hence overlaps with putative instances for k's other than `*`; whereas
 {{{
   instance Functor P1 (a :: *)
 }}}
 matches only for the `*` case.  And that is a subtle distinction indeed!

 Hmm.   I am rather persuaded by Richard's argument. '''Proposal:''' just
 regard the kind constraints as extra inferred constraints, and hence
 generate
 {{{
   instance (k ~ *) => Functor (P1 (a :: k))
 }}}
 Now the derived instance always has type variables in the head; but those
 type variables may be constrained by the context.  I like that.

 It's not quite what happens now, so there would be a little implementation
 work to do.  It might quite possibly actually be simpler.

 I'm going to dump this email into the ticket.

 Simon

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