
#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