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
I'm inclined to go with option 3 as `Functor (Proxy *)` is the only instance that would typecheck. Perhaps with a warning to let the user know the instance is less general than they might expect? I think this is the most user-friendly route: the user can suppress the warning if they don't care, or make it an error if they do care. On Mon, Mar 28, 2016, at 05:55, Richard Eisenberg wrote:
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
I like number option number two. I don't really expect any of the
TypeInType stuff to work with the deriving machinery. I think that, at the
moment, for a normal deriving clause, GHC never adds in constraints (I
might be wrong on this). Whenever constraints, I feel like
StandaloneDeriving is the right choice. I don't know if StandaloneDeriving
works with DeriveFunctor or not, but if it does, then this is what I would
expect:
REJECTED
data Proxy k (a :: k) = P
deriving Functor
ACCEPTED
data Proxy k (a :: k) = P
deriving instance (k ~ *) => Functor Proxy k
But if the second code snippet involving StandaloneDeriving can't be made
to work, I would still prefer for the first snippet to be rejected as well.
Just my two cents.
-Andrew Thaddeus Martin
On Mon, Mar 28, 2016 at 8:55 AM, Richard Eisenberg
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
-- -Andrew Thaddeus Martin
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@haskell.org] On Behalf Of
| Richard Eisenberg
| Sent: 28 March 2016 13:55
| To: GHC developers
participants (4)
-
Andrew Martin -
Eric Seidel -
Richard Eisenberg -
Simon Peyton Jones