More GND + role inference woes

[Simon Peyton-Jones]

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:ghc-devs-bounces at haskell.org] 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 <ekmett at gmail.com<mailto:ekmett at gmail.com>> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131016/2f0214a9/attachment-0001.html>