I think I know what to do about the GND + roles question.
First, the problem. Here’s an example:
class Trans t a where
foo :: t a -> t a
newtype N x = MkN x deriving( Trans Maybe )
As things stand, Trans gets roles (representational, nominal). The second
parameter ‘a’ gets a nominal role because we don’t know what ‘t’ will get
instantiated too.
As a result the attempted GND is rejected because of the new role stuff. But
with 7.6.3 we’ll get an instance
instance Trans Maybe a => Trans Maybe (N a)
from the GND mechanism.
Do I have this right?
Second, there is a Good Reason for the problem. Suppose I said
newtype N x = MkN x deriving( Trans D )
where D was a data family. Then the foo method for (D x) might seg-fault if
applied to a (D (N x)) value. So the current GND is treading on very thin ice,
and it is ice that the author (Edward) does not control. His clients control
it.
Do I have this right?
Third, there is an easy solution. As Richard observed in a separate thread
about Coercible, GND does not attempt to build a coercion to witness
Trans Maybe x ~R Trans Maybe (N x)
Rather, it builds a dictionary for (Trans Maybe (N x)) thus
dTransMaybeN :: Trans Maybe x -> Trans Maybe (N x)
dTransMaybeN d = MkTrans (sel_foo d |> co)
where the (sel_foo d) selects the foo method from d. That is, we actually
cast the methods, not the dictionary as a whole. So what we need is a coercion
between
Maybe x ~R Maybe (N x)
Can we get that? Yes of course! Maybe has a representational role.
Bottom line: we should accept or reject a GND attempt not on the basis of the
role of the class, but rather on whether the method types are coercible.
Indeed, this is just what we agreed some days ago
http://www.haskell.org/pipermail/glasgow-haskell-users/2013-October/024386.html
So I think this solves Edward’s problem below.
Moreover, I think this solves the other failures in
http://www.haskell.org/pipermail/ghc-devs/2013-October/002961.html. Here is
one example, in that email. smallcheck has this:
newtype Series m a = Series (ReaderT Depth (LogicT m) a)
deriving
( …, MonadLogic)
where logict defines MonadLogic thus:
class (MonadPlus m) => MonadLogic m where
msplit :: m a -> m (Maybe (a, m a))
So the “bottom line” check above will attempt to find a cocercion betwem
msplit’s type with m=Series m, and with m=ReaderT Depth (LogitT m). Right? So
on the left of msplit’s arrow, we’ll ask can we prove
Series m a ~R ReaderT Depth (LogicT m) a
Can we show that? Yes, of course… that is the very newtype coercion for Series.
In short, I think we are fine, once Richard has implemented the new GND test.
Am I wrong?
Simon
From: ghc-devs [mailto:[email protected]] On Behalf Of Edward Kmett
Sent: 13 October 2013 23:02
To: ghc-devs; Richard Eisenberg
Subject: Re: More GND + role inference woes
I didn't think I was using GND much at all, but apparently I was wrong.
After Ben's initial foray into building linear, I went and looked at the other
applications of GeneralizedNewtypeDeriving in my code and found that in
parsers, all of the derived instances for the supplied parser transformers fail.
This also affects any attempt to use GND to do deriving for any monad
transformer stack that isn't fully instantiated to concrete terms. This is
actually a very common idiom to avoid writing boilerplate on top of
transformers:
newtype T m a = T { runT : StateT MyState (ReaderT MyEnv) m a }
deriving (Functor, Monad, Applicative, MonadState MyState, MonadReader MyEnv,
...)
As I rummage through more of my code, I actually can't find any instances of
GND that do still work that aren't of the form:
newtype Foo a = Foo { runFoo :: a } deriving ...
Literally every other example I have of GND in the code I maintain has
something in it that causes it to run afoul of the new roles machinery.
I'd say the problem is more widespread than we thought.
-Edward
On Sun, Oct 13, 2013 at 5:26 PM, Edward Kmett
<[email protected]<mailto:[email protected]>> wrote:
Ben Gamari was trying to update my linear package to work with GHC HEAD.
Along the way he noted an example of the new GND+role inference machinery
failing rather spectacularly.
http://hackage.haskell.org/package/linear-1.3/docs/src/Linear-Affine.html#Point
Note the number of classes that the current proposal would force us to hand
implement.
=(
-Edward
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
