instantiating visible parameters in when deriving instances

[Simon Peyton Jones]

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

Now the question is: what derived instances do we get?  We could get

  instance Functor (P1 (a :: *))
  instance Functor (P2 * (a ::*))

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.  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!

Humph.  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

|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
|  Richard Eisenberg
|  Sent: 28 March 2016 13:55
|  To: GHC developers <ghc-devs at haskell.org>
|  Subject: instantiating visible parameters in when deriving instances
|  
|  Hi devs,
|  
|  Consider the following:
|  
|  > data Proxy k (a :: k) = P
|  >   deriving Functor
|  
|  What should happen when this is compiled?
|   1. Issue an error saying that `deriving` cannot instantiate visible
|  parameters.
|   2. Type error: cannot match `k` with `*`.
|   3. Successfully produce `instance (Proxy *)`.
|  
|  Currently, GHC does #3. But this ends up choosing a value for a visible
|  (i.e. explicit) parameter to Proxy. Is this a good idea? I myself have
|  flip-flopped on this issue; see
|  https://ghc.haskell.org/trac/ghc/ticket/11732, comments 4 and 9.
|  
|  I'd love to get feedback on this point.
|  
|  Thanks!
|  Richard
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at haskell.org
|  https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.ha
|  skell.org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
|  devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c175b7c5afb594993
|  14e708d357083e9e%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=d6dNjZWCi
|  IeqDBNFVSL13b6ZUG0QREf9UcqrVrqbpEA%3d