More GND + role inference woes

newer
Common Context transformation for...

older
whats our timeline for 7.8 release?

Edward Kmett

13 Oct 2013 13 Oct '13

9:26 p.m.

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#Po... Note the number of classes that the current proposal would force us to hand implement. =( -Edward

Attachments:

attachment.html (text/html — 610 bytes)

Show replies by date

Edward Kmett

13 Oct 13 Oct

10:01 p.m.

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 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#Po...

Note the number of classes that the current proposal would force us to hand implement.

=(

-Edward

Richard Eisenberg

15 Oct 15 Oct

4:22 a.m.

Yuck. But, many, many thanks for discovering this now instead of later. For various silly reasons, I didn't have a platform (i.e. a recent enough HEAD in the right state, etc.) for me to explore this today (Monday). But, I should have the time and ability to look closer on Tuesday. If it's really as bad as you say, we'll need to think carefully about how to proceed. I have various thoughts about how to fix the problem, but none would be ready for 7.8 by a long shot. So, do we issue warnings (that a GND, or perhaps a use of `coerce` might not be safe) in 7.8? How would a user disable these warnings? Anyway, more tomorrow. Richard On Oct 13, 2013, at 6:01 PM, Edward Kmett wrote:

...

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 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#Po...

Note the number of classes that the current proposal would force us to hand implement.

=(

-Edward

Simon Peyton-Jones

16 Oct 16 Oct

1:28 p.m.

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.h... 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@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 mailto:ekmett@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#Po... Note the number of classes that the current proposal would force us to hand implement. =( -Edward

Edward Kmett

4:46 p.m.

...

On Oct 16, 2013, at 9:28 AM, Simon Peyton-Jones wrote:

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

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?

I have no counter examples for GND based on coercing dictionaries rather than parameters at this time and I do agree that this does strike me as sufficient to plug the obvious holes in the current approach. I'll keep looking and see if I can't find a way to subvert the system, but this sounds promising for roles. In light of this, the NPR approach that Richard suggested strikes me as more relevant to fixing up Coercible than GND and as you mentioned we can very well spend another release cycle to get Coercible right. Assuming the dictionary casts work the way we expect, I'm think I'm sold. The main thing I don't want to do is wake up after 7.8 is cut and personally have to write 4000 lines of previously derived instances that are provably safe, because of an overly restrictive role scheme. I'm cautiously optimistic that this will be sufficient to keep me out of that scenario. ;) -Edward

...

Simon

From: ghc-devs [mailto:ghc-devs-bounces@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 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#Po...

Note the number of classes that the current proposal would force us to hand implement.

=(

-Edward

Richard Eisenberg

5:30 p.m.

It seems like we may be on the same page now. Do you agree with my previous email that the change to the GND check will not solve *all* your problems? That is, there will be some derived instances you will have to hand-write, but (I think) for good reason. Richard On Oct 16, 2013, at 12:46 PM, Edward Kmett wrote:

...

On Oct 16, 2013, at 9:28 AM, Simon Peyton-Jones wrote:

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

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?

I have no counter examples for GND based on coercing dictionaries rather than parameters at this time and I do agree that this does strike me as sufficient to plug the obvious holes in the current approach.

I'll keep looking and see if I can't find a way to subvert the system, but this sounds promising for roles.

In light of this, the NPR approach that Richard suggested strikes me as more relevant to fixing up Coercible than GND and as you mentioned we can very well spend another release cycle to get Coercible right.

Assuming the dictionary casts work the way we expect, I'm think I'm sold. The main thing I don't want to do is wake up after 7.8 is cut and personally have to write 4000 lines of previously derived instances that are provably safe, because of an overly restrictive role scheme. I'm cautiously optimistic that this will be sufficient to keep me out of that scenario. ;)

-Edward

...
Simon

From: ghc-devs [mailto:ghc-devs-bounces@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 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#Po...

Note the number of classes that the current proposal would force us to hand implement.

=(

-Edward

Edward Kmett

5:50 p.m.

I think we're basically in agreement. I'm more than happy to write those 5-6 instances that legitimately aren't safe to derive. -Edward

...

On Oct 16, 2013, at 1:30 PM, Richard Eisenberg wrote:

It seems like we may be on the same page now. Do you agree with my previous email that the change to the GND check will not solve *all* your problems? That is, there will be some derived instances you will have to hand-write, but (I think) for good reason.

Richard

...
On Oct 16, 2013, at 12:46 PM, Edward Kmett wrote:

...
On Oct 16, 2013, at 9:28 AM, Simon Peyton-Jones wrote:

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

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?

I have no counter examples for GND based on coercing dictionaries rather than parameters at this time and I do agree that this does strike me as sufficient to plug the obvious holes in the current approach.

I'll keep looking and see if I can't find a way to subvert the system, but this sounds promising for roles.

In light of this, the NPR approach that Richard suggested strikes me as more relevant to fixing up Coercible than GND and as you mentioned we can very well spend another release cycle to get Coercible right.

Assuming the dictionary casts work the way we expect, I'm think I'm sold. The main thing I don't want to do is wake up after 7.8 is cut and personally have to write 4000 lines of previously derived instances that are provably safe, because of an overly restrictive role scheme. I'm cautiously optimistic that this will be sufficient to keep me out of that scenario. ;)

-Edward

...
Simon

From: ghc-devs [mailto:ghc-devs-bounces@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 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#Po...

Note the number of classes that the current proposal would force us to hand implement.

=(

-Edward

Richard Eisenberg

5:28 p.m.

Please see my responses below. (Note: this was written before Edward's most recent post, which will be addressed shortly.) Executive summary: Edward's problem is more general than the one that Simon solves, but what Edward wants is actually not type safe. On Oct 16, 2013, at 9:28 AM, Simon Peyton-Jones wrote:

...

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?

This is a more specific instance of the problem. Yes, the case with `Trans` does appear, but also cases like this:

...

class Functor f => Core f where core :: ((forall g x. Functor g => (x -> g x) -> f x -> g (f x)) -> a) -> f a

That's a nasty-looking type, but note the `g (f x)` that appears. Here, `f` is used as a parameter to a type variable that *is not a class variable*. The problem Simon describes is only the case where the applied type variable is a class variable, and thus is known at `deriving` time. To handle things like Core, we would need to have more proper role abstraction, where we can assert that `g` has a parameter with a representational role in order to infer `f` as a representational parameter for Core. In Edward's `linear` package, the Linear.Affine module has this definition:

...

newtype Point f a = P (f a) deriving ( Eq, Ord, Show, Read, Monad, Functor, Applicative, Foldable , Traversable, Apply, Bind, Additive, Metric, Core, R1, R2, R3, R4 , Fractional , Num, Ix, Storable, Epsilon )

Of these derivings, the following currently fail: Traversable, Bind, Core, R1, R2, R3, and R4. It is straightforward to fix Traversable with DeriveTraversable (and a standalone instance). Bind will fixed by the change in the GND check. But, Core and the Rs won't be and would have to be written by hand.

...

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?

Yes.

...

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

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?

Yes.

...

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.

Well, it's the right-hand side of the arrow that's more troublesome, but that works out in this case, too.

...

In short, I think we are fine, once Richard has implemented the new GND test.

Am I wrong?

It depends on what "fine" is. The new GND check will allow more deriving, but not all that Edward wants. BUT, the ones that (the new) GND doesn't allow aren't actually safe! In the Point example, using GND on Core and the Rs might actually lead to a type error, depending on the instantiation of local type variables within the methods in those classes. For example, if the `g` variable in Core's `core` method is instantiated with a type with a nominal parameter, there could be trouble. So, I disagree with Edward's original claim at the top of this thread that roles cause havoc here: they don't cause havoc, they catch latent type errors! On the other hand, I agree that with more machinery (that is, a constraint on `g` about its parameter's role) we could potentially allow all the derived instances that Edward wants. What I'm worried about is the user experience like the following: - 7.8 comes out: A bunch of deriving clauses have to be expanded to hand-written instances. Annoying, and with runtime cost. - 7.10 comes out: A bunch of those expanded instances now can be rolled back into derived ones, with some extra, not-backward-compatible annotations (that is, the constraints on variables like `g`). Annoying, and a real maintenance headache. What it would mean is that, if we do decide to generalize roles further, users would have one release that allows noticeably fewer uses of GND than the one before or the one after it. On the other hand, if we're confident that we're not going to tinker with roles more, then I see much stronger reasons for releasing with 7.8. Richard

Edward Kmett

5:46 p.m.

If this forced me to write those instances by hand, I could accept that as a tax for correctness. It means you can't GND any of the HasFoo dictionaries that lens builds, but meh. My original objection was for the existing solution with type classes themselves having their arguments be representational. Now that we've changed the problem, the fact that things like this are being caught does a lot to reassure me of the vastly improved correctness of the new scheme. Off the top of your head do things like the following work under the new scheme? newtype T m a = T { runT :: StateT MyState m a } deriving (Monad, MonadState MyState, MonadTrans) I don't have a good enough mental model of the desugaring of the fundep in MonadState. -Edward

...

On Oct 16, 2013, at 1:28 PM, Richard Eisenberg wrote:

Please see my responses below. (Note: this was written before Edward's most recent post, which will be addressed shortly.) Executive summary: Edward's problem is more general than the one that Simon solves, but what Edward wants is actually not type safe.

...
On Oct 16, 2013, at 9:28 AM, Simon Peyton-Jones wrote:

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?

This is a more specific instance of the problem. Yes, the case with `Trans` does appear, but also cases like this:

...
class Functor f => Core f where core :: ((forall g x. Functor g => (x -> g x) -> f x -> g (f x)) -> a) -> f a

That's a nasty-looking type, but note the `g (f x)` that appears. Here, `f` is used as a parameter to a type variable that *is not a class variable*. The problem Simon describes is only the case where the applied type variable is a class variable, and thus is known at `deriving` time.

To handle things like Core, we would need to have more proper role abstraction, where we can assert that `g` has a parameter with a representational role in order to infer `f` as a representational parameter for Core. In Edward's `linear` package, the Linear.Affine module has this definition:

...
newtype Point f a = P (f a) deriving ( Eq, Ord, Show, Read, Monad, Functor, Applicative, Foldable , Traversable, Apply, Bind, Additive, Metric, Core, R1, R2, R3, R4 , Fractional , Num, Ix, Storable, Epsilon )

Of these derivings, the following currently fail: Traversable, Bind, Core, R1, R2, R3, and R4. It is straightforward to fix Traversable with DeriveTraversable (and a standalone instance). Bind will fixed by the change in the GND check. But, Core and the Rs won't be and would have to be written by hand.

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

Yes.

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

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?

Yes.

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

Well, it's the right-hand side of the arrow that's more troublesome, but that works out in this case, too.

...
In short, I think we are fine, once Richard has implemented the new GND test.

Am I wrong?

It depends on what "fine" is.

The new GND check will allow more deriving, but not all that Edward wants. BUT, the ones that (the new) GND doesn't allow aren't actually safe! In the Point example, using GND on Core and the Rs might actually lead to a type error, depending on the instantiation of local type variables within the methods in those classes. For example, if the `g` variable in Core's `core` method is instantiated with a type with a nominal parameter, there could be trouble.

So, I disagree with Edward's original claim at the top of this thread that roles cause havoc here: they don't cause havoc, they catch latent type errors!

On the other hand, I agree that with more machinery (that is, a constraint on `g` about its parameter's role) we could potentially allow all the derived instances that Edward wants.

What I'm worried about is the user experience like the following: - 7.8 comes out: A bunch of deriving clauses have to be expanded to hand-written instances. Annoying, and with runtime cost. - 7.10 comes out: A bunch of those expanded instances now can be rolled back into derived ones, with some extra, not-backward-compatible annotations (that is, the constraints on variables like `g`). Annoying, and a real maintenance headache.

What it would mean is that, if we do decide to generalize roles further, users would have one release that allows noticeably fewer uses of GND than the one before or the one after it. On the other hand, if we're confident that we're not going to tinker with roles more, then I see much stronger reasons for releasing with 7.8.

Richard

Richard Eisenberg

6 p.m.

On Oct 16, 2013, at 1:46 PM, Edward Kmett wrote:

...

Off the top of your head do things like the following work under the new scheme?

newtype T m a = T { runT :: StateT MyState m a } deriving (Monad, MonadState MyState, MonadTrans)

Yes, I believe that will work. The only "hard" part is for the `get` method of MonadState, but when we know the specific parameters, all should be OK. Richard

Ben Gamari

14 Dec 14 Dec

9:52 p.m.

Edward Kmett writes:

...

If this forced me to write those instances by hand, I could accept that as a tax for correctness. It means you can't GND any of the HasFoo dictionaries that lens builds, but meh.

Am I correct in assuming that Bind, R1, R2, R3, and R4 are the problematic instances in linear? With recent GHC I get the errors below. Cheers, - Ben src/Linear/Affine.hs:112:34: Could not coerce from ‛f (f a)’ to ‛f (Point f a)’ because ‛f (f a)’ and ‛f (Point f a)’ are different types. arising from the coercion of the method ‛join’ from type ‛forall a. f (f a) -> f a’ to type ‛forall a. Point f (Point f a) -> Point f a’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (Bind (Point f)) src/Linear/Affine.hs:112:58: Could not coerce from ‛g (f x)’ to ‛g (Point f x)’ because ‛g (f x)’ and ‛g (Point f x)’ are different types. arising from the coercion of the method ‛core’ from type ‛forall a. ((forall (g :: * -> *) x. Functor g => (x -> g x) -> f x -> g (f x)) -> a) -> f a’ to type ‛forall a. ((forall (g :: * -> *) x. Functor g => (x -> g x) -> Point f x -> g (Point f x)) -> a) -> Point f a’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (Core (Point f)) src/Linear/Affine.hs:112:64: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_x’ from type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R1 (Point f)) src/Linear/Affine.hs:112:68: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_xy’ from type ‛forall a (f :: * -> *). Functor f => (V2 a -> f (V2 a)) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (V2 a -> f (V2 a)) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R2 (Point f)) src/Linear/Affine.hs:112:68: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_y’ from type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R2 (Point f)) src/Linear/Affine.hs:112:72: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_xyz’ from type ‛forall a (f :: * -> *). Functor f => (V3 a -> f (V3 a)) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (V3 a -> f (V3 a)) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R3 (Point f)) src/Linear/Affine.hs:112:72: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_z’ from type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R3 (Point f)) src/Linear/Affine.hs:112:76: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_xyzw’ from type ‛forall a (f :: * -> *). Functor f => (V4 a -> f (V4 a)) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (V4 a -> f (V4 a)) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R4 (Point f)) src/Linear/Affine.hs:112:76: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_w’ from type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R4 (Point f))

Richard Eisenberg

15 Dec 15 Dec

12:53 a.m.

Yes, I believe that's right. As far as I can figure out, these classes really *are* problematic, in that if we allowed GeneralizedNewtypeDeriving for them, there would be a way to subvert the type system. To make these derivable, we would need to be able to restrict various type parameters from taking on values that take a nominal argument. Without the ability to restrict the values in this way, there could be trouble. Richard On Dec 14, 2013, at 4:52 PM, Ben Gamari wrote:

...

Edward Kmett writes:

...
If this forced me to write those instances by hand, I could accept that as a tax for correctness. It means you can't GND any of the HasFoo dictionaries that lens builds, but meh.

Am I correct in assuming that Bind, R1, R2, R3, and R4 are the problematic instances in linear? With recent GHC I get the errors below.

Cheers,

- Ben

src/Linear/Affine.hs:112:34: Could not coerce from ‛f (f a)’ to ‛f (Point f a)’ because ‛f (f a)’ and ‛f (Point f a)’ are different types. arising from the coercion of the method ‛join’ from type ‛forall a. f (f a) -> f a’ to type ‛forall a. Point f (Point f a) -> Point f a’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (Bind (Point f))

src/Linear/Affine.hs:112:58: Could not coerce from ‛g (f x)’ to ‛g (Point f x)’ because ‛g (f x)’ and ‛g (Point f x)’ are different types. arising from the coercion of the method ‛core’ from type ‛forall a. ((forall (g :: * -> *) x. Functor g => (x -> g x) -> f x -> g (f x)) -> a) -> f a’ to type ‛forall a. ((forall (g :: * -> *) x. Functor g => (x -> g x) -> Point f x -> g (Point f x)) -> a) -> Point f a’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (Core (Point f))

src/Linear/Affine.hs:112:64: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_x’ from type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R1 (Point f))

src/Linear/Affine.hs:112:68: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_xy’ from type ‛forall a (f :: * -> *). Functor f => (V2 a -> f (V2 a)) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (V2 a -> f (V2 a)) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R2 (Point f))

src/Linear/Affine.hs:112:68: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_y’ from type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R2 (Point f))

src/Linear/Affine.hs:112:72: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_xyz’ from type ‛forall a (f :: * -> *). Functor f => (V3 a -> f (V3 a)) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (V3 a -> f (V3 a)) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R3 (Point f))

src/Linear/Affine.hs:112:72: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_z’ from type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R3 (Point f))

src/Linear/Affine.hs:112:76: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_xyzw’ from type ‛forall a (f :: * -> *). Functor f => (V4 a -> f (V4 a)) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (V4 a -> f (V4 a)) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R4 (Point f))

src/Linear/Affine.hs:112:76: Could not coerce from ‛f1 (f a)’ to ‛f1 (Point f a)’ because ‛f1 (f a)’ and ‛f1 (Point f a)’ are different types. arising from the coercion of the method ‛_w’ from type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)’ to type ‛forall a (f :: * -> *). Functor f => (a -> f a) -> Point f a -> f (Point f a)’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (R4 (Point f))

Ben Gamari

12:59 a.m.

Richard Eisenberg writes:

...

Yes, I believe that's right. As far as I can figure out, these classes really *are* problematic, in that if we allowed GeneralizedNewtypeDeriving for them, there would be a way to subvert the type system. To make these derivable, we would need to be able to restrict various type parameters from taking on values that take a nominal argument. Without the ability to restrict the values in this way, there could be trouble.

I suppose it's unlikely that the roles mechanism will be extended to allow for such restriction? Cheers, - Ben

Richard Eisenberg

1:06 a.m.

On Dec 14, 2013, at 7:59 PM, Ben Gamari wrote:

...

I suppose it's unlikely that the roles mechanism will be extended to allow for such restriction?

Very unlikely in the short term. As more use cases for such a feature filter in and the community demands the feature, there's no strong technical reason it can't be done. We believe that doing this would add quite a bit more complexity within GHC and doesn't have the right payoff-to-complexity ratio, for now. Richard

Edward Kmett

9:27 a.m.

Correct. With 7.8 we'll need to hand-implement those instances rather than derive them. On Sat, Dec 14, 2013 at 7:59 PM, Ben Gamari wrote:

...

Richard Eisenberg writes:

...
Yes, I believe that's right. As far as I can figure out, these classes really *are* problematic, in that if we allowed GeneralizedNewtypeDeriving for them, there would be a way to subvert the type system. To make these derivable, we would need to be able to restrict various type parameters from taking on values that take a nominal argument. Without the ability to restrict the values in this way, there could be trouble.

I suppose it's unlikely that the roles mechanism will be extended to allow for such restriction?

Cheers,

- Ben

Simon Peyton-Jones

31 Dec 31 Dec

10:07 a.m.

So I think we are agreed that what is currently implemented is the right thing; and that it’s expressive enough for now. There’s a lot of interesting stuff in this thread that it would be a shame to lose. It would be great if the wiki page on roles could cover this stuff: https://ghc.haskell.org/trac/ghc/wiki/Roles Specifically, · the way that GND is implemented (as described in the attached email) by looking at the method types, is manifestly non-obvious (since we missed it for ages) · Richard’s observations about the things it still doesn’t do are interesting · Some poster-child examples for where the simple roles we have are insufficiently expressive and a sketch of how it could be extended if necessary (I agree with Richard’s assessment that it’s not worth it right now). Richard, you are the obvious person to do this, if you have time. Maybe just pointers to the right places would do. Simon From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Edward Kmett Sent: 15 December 2013 09:28 To: Ben Gamari Cc: ghc-devs Subject: Re: More GND + role inference woes Correct. With 7.8 we'll need to hand-implement those instances rather than derive them. On Sat, Dec 14, 2013 at 7:59 PM, Ben Gamari mailto:bgamari.foss@gmail.com> wrote: Richard Eisenberg mailto:eir@cis.upenn.edu> writes:

...

Yes, I believe that's right. As far as I can figure out, these classes really *are* problematic, in that if we allowed GeneralizedNewtypeDeriving for them, there would be a way to subvert the type system. To make these derivable, we would need to be able to restrict various type parameters from taking on values that take a nominal argument. Without the ability to restrict the values in this way, there could be trouble.

I suppose it's unlikely that the roles mechanism will be extended to allow for such restriction? Cheers, - Ben

Simon Peyton-Jones

16 Oct 16 Oct

8:23 p.m.

What it would mean is that, if we do decide to generalize roles further, users would have one release that allows noticeably fewer uses of GND than the one before or the one after it. On the other hand, if we're confident that we're not going to tinker with roles more, then I see much stronger reasons for releasing with 7.8. I don't think we know for sure. But the way to find out is to release it. If we don't have a compiler that supports roles, no one will explore or use them. We do this all the time, and yes, Haskell is a bit less smoothly-upgradable as a result. But I think it's worth it, otherwise we'd be stuck in treacle. Remember this is fixing a current unsoundness that can lead to un-caught segmentation faults in user code. That is a Jolly Good thing to fix, it not just a snazzy feature that two people want. Richard, how are you fixed at the moment? Are you able to implement the new GND check soon? Or not? Simon From: Richard Eisenberg [mailto:eir@cis.upenn.edu] Sent: 16 October 2013 18:29 To: Simon Peyton-Jones Cc: Edward Kmett; ghc-devs Subject: Re: More GND + role inference woes Please see my responses below. (Note: this was written before Edward's most recent post, which will be addressed shortly.) Executive summary: Edward's problem is more general than the one that Simon solves, but what Edward wants is actually not type safe. On Oct 16, 2013, at 9:28 AM, Simon Peyton-Jones wrote: 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? This is a more specific instance of the problem. Yes, the case with `Trans` does appear, but also cases like this: class Functor f => Core f where core :: ((forall g x. Functor g => (x -> g x) -> f x -> g (f x)) -> a) -> f a That's a nasty-looking type, but note the `g (f x)` that appears. Here, `f` is used as a parameter to a type variable that *is not a class variable*. The problem Simon describes is only the case where the applied type variable is a class variable, and thus is known at `deriving` time. To handle things like Core, we would need to have more proper role abstraction, where we can assert that `g` has a parameter with a representational role in order to infer `f` as a representational parameter for Core. In Edward's `linear` package, the Linear.Affine module has this definition: newtype Point f a = P (f a) deriving ( Eq, Ord, Show, Read, Monad, Functor, Applicative, Foldable , Traversable, Apply, Bind, Additive, Metric, Core, R1, R2, R3, R4 , Fractional , Num, Ix, Storable, Epsilon ) Of these derivings, the following currently fail: Traversable, Bind, Core, R1, R2, R3, and R4. It is straightforward to fix Traversable with DeriveTraversable (and a standalone instance). Bind will fixed by the change in the GND check. But, Core and the Rs won't be and would have to be written by hand. 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? Yes. 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.h... 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? Yes. 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. Well, it's the right-hand side of the arrow that's more troublesome, but that works out in this case, too. In short, I think we are fine, once Richard has implemented the new GND test. Am I wrong? It depends on what "fine" is. The new GND check will allow more deriving, but not all that Edward wants. BUT, the ones that (the new) GND doesn't allow aren't actually safe! In the Point example, using GND on Core and the Rs might actually lead to a type error, depending on the instantiation of local type variables within the methods in those classes. For example, if the `g` variable in Core's `core` method is instantiated with a type with a nominal parameter, there could be trouble. So, I disagree with Edward's original claim at the top of this thread that roles cause havoc here: they don't cause havoc, they catch latent type errors! On the other hand, I agree that with more machinery (that is, a constraint on `g` about its parameter's role) we could potentially allow all the derived instances that Edward wants. What I'm worried about is the user experience like the following: - 7.8 comes out: A bunch of deriving clauses have to be expanded to hand-written instances. Annoying, and with runtime cost. - 7.10 comes out: A bunch of those expanded instances now can be rolled back into derived ones, with some extra, not-backward-compatible annotations (that is, the constraints on variables like `g`). Annoying, and a real maintenance headache. What it would mean is that, if we do decide to generalize roles further, users would have one release that allows noticeably fewer uses of GND than the one before or the one after it. On the other hand, if we're confident that we're not going to tinker with roles more, then I see much stronger reasons for releasing with 7.8. Richard

Richard Eisenberg

8:38 p.m.

On Oct 16, 2013, at 4:23 PM, Simon Peyton-Jones wrote:

...

What it would mean is that, if we do decide to generalize roles further, users would have one release that allows noticeably fewer uses of GND than the one before or the one after it. On the other hand, if we're confident that we're not going to tinker with roles more, then I see much stronger reasons for releasing with 7.8.

I don’t think we know for sure. But the way to find out is to release it. If we don’t have a compiler that supports roles, no one will explore or use them. We do this all the time, and yes, Haskell is a bit less smoothly-upgradable as a result. But I think it’s worth it, otherwise we’d be stuck in treacle.

Remember this is fixing a current unsoundness that can lead to un-caught segmentation faults in user code. That is a Jolly Good thing to fix, it not just a snazzy feature that two people want.

Richard, how are you fixed at the moment? Are you able to implement the new GND check soon? Or not?

OK. It sounds like we're all pushing forward here. I should be able to implement within the next week, probably starting tomorrow, and possibly ending tomorrow, too. Not sure exactly how hard it will be. Richard

...

Simon

From: Richard Eisenberg [mailto:eir@cis.upenn.edu] Sent: 16 October 2013 18:29 To: Simon Peyton-Jones Cc: Edward Kmett; ghc-devs Subject: Re: More GND + role inference woes

Please see my responses below. (Note: this was written before Edward's most recent post, which will be addressed shortly.) Executive summary: Edward's problem is more general than the one that Simon solves, but what Edward wants is actually not type safe.

On Oct 16, 2013, at 9:28 AM, Simon Peyton-Jones wrote:

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?

This is a more specific instance of the problem. Yes, the case with `Trans` does appear, but also cases like this:

class Functor f => Core f where core :: ((forall g x. Functor g => (x -> g x) -> f x -> g (f x)) -> a) -> f a

That's a nasty-looking type, but note the `g (f x)` that appears. Here, `f` is used as a parameter to a type variable that *is not a class variable*. The problem Simon describes is only the case where the applied type variable is a class variable, and thus is known at `deriving` time.

To handle things like Core, we would need to have more proper role abstraction, where we can assert that `g` has a parameter with a representational role in order to infer `f` as a representational parameter for Core. In Edward's `linear` package, the Linear.Affine module has this definition:

newtype Point f a = P (f a) deriving ( Eq, Ord, Show, Read, Monad, Functor, Applicative, Foldable , Traversable, Apply, Bind, Additive, Metric, Core, R1, R2, R3, R4 , Fractional , Num, Ix, Storable, Epsilon )

Of these derivings, the following currently fail: Traversable, Bind, Core, R1, R2, R3, and R4. It is straightforward to fix Traversable with DeriveTraversable (and a standalone instance). Bind will fixed by the change in the GND check. But, Core and the Rs won't be and would have to be written by hand.

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?

Yes.

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

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?

Yes.

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.

Well, it's the right-hand side of the arrow that's more troublesome, but that works out in this case, too.

In short, I think we are fine, once Richard has implemented the new GND test.

Am I wrong?

It depends on what "fine" is.

The new GND check will allow more deriving, but not all that Edward wants. BUT, the ones that (the new) GND doesn't allow aren't actually safe! In the Point example, using GND on Core and the Rs might actually lead to a type error, depending on the instantiation of local type variables within the methods in those classes. For example, if the `g` variable in Core's `core` method is instantiated with a type with a nominal parameter, there could be trouble.

So, I disagree with Edward's original claim at the top of this thread that roles cause havoc here: they don't cause havoc, they catch latent type errors!

On the other hand, I agree that with more machinery (that is, a constraint on `g` about its parameter's role) we could potentially allow all the derived instances that Edward wants.

What I'm worried about is the user experience like the following: - 7.8 comes out: A bunch of deriving clauses have to be expanded to hand-written instances. Annoying, and with runtime cost. - 7.10 comes out: A bunch of those expanded instances now can be rolled back into derived ones, with some extra, not-backward-compatible annotations (that is, the constraints on variables like `g`). Annoying, and a real maintenance headache.

What it would mean is that, if we do decide to generalize roles further, users would have one release that allows noticeably fewer uses of GND than the one before or the one after it. On the other hand, if we're confident that we're not going to tinker with roles more, then I see much stronger reasons for releasing with 7.8.

Richard

Roman Cheplyaka

4 Nov 4 Nov

3:37 p.m.

* Richard Eisenberg [2013-10-16 13:28:54-0400]

...

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

Yes.

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

Well, it's the right-hand side of the arrow that's more troublesome, but that works out in this case, too.

I just tried compiling smallcheck with GHC HEAD, and it didn't work out: Test/SmallCheck/SeriesMonad.hs:41:7: Can't make a derived instance of ‛MonadLogic (Series m)’ (even with cunning newtype deriving): it is not type-safe to use GeneralizedNewtypeDeriving on this class; ‛msplit’, at type ‛forall a. m a -> m (Maybe (a, m a))’, cannot be converted safely In the newtype declaration for ‛Series’ So GHC now looks at the methods, but the problem is still there. What do you guys think? I would agree that msplit's type is problematic (due to the nested m's), but Simon and Richard previously said that it should work, so I'm confused. Roman

Richard Eisenberg

4:02 p.m.

Bah. This is a bug. I will fix. Thanks for pointing it out! Richard On Nov 4, 2013, at 10:37 AM, Roman Cheplyaka wrote:

...

* Richard Eisenberg [2013-10-16 13:28:54-0400]

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

Yes.

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

Well, it's the right-hand side of the arrow that's more troublesome, but that works out in this case, too.

I just tried compiling smallcheck with GHC HEAD, and it didn't work out:

Test/SmallCheck/SeriesMonad.hs:41:7: Can't make a derived instance of ‛MonadLogic (Series m)’ (even with cunning newtype deriving): it is not type-safe to use GeneralizedNewtypeDeriving on this class; ‛msplit’, at type ‛forall a. m a -> m (Maybe (a, m a))’, cannot be converted safely In the newtype declaration for ‛Series’

So GHC now looks at the methods, but the problem is still there.

What do you guys think?

I would agree that msplit's type is problematic (due to the nested m's), but Simon and Richard previously said that it should work, so I'm confused.

Roman

Richard Eisenberg

6:52 p.m.

Bah^2. This is subtler than I thought. See the ticket commentary here: http://ghc.haskell.org/trac/ghc/ticket/8503 Richard On Nov 4, 2013, at 11:02 AM, Richard Eisenberg wrote:

...

Bah. This is a bug. I will fix.

Thanks for pointing it out! Richard

On Nov 4, 2013, at 10:37 AM, Roman Cheplyaka wrote:

...
* Richard Eisenberg [2013-10-16 13:28:54-0400]

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

Yes.

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

Well, it's the right-hand side of the arrow that's more troublesome, but that works out in this case, too.

I just tried compiling smallcheck with GHC HEAD, and it didn't work out:

Test/SmallCheck/SeriesMonad.hs:41:7: Can't make a derived instance of ‛MonadLogic (Series m)’ (even with cunning newtype deriving): it is not type-safe to use GeneralizedNewtypeDeriving on this class; ‛msplit’, at type ‛forall a. m a -> m (Maybe (a, m a))’, cannot be converted safely In the newtype declaration for ‛Series’

So GHC now looks at the methods, but the problem is still there.

What do you guys think?

I would agree that msplit's type is problematic (due to the nested m's), but Simon and Richard previously said that it should work, so I'm confused.

Roman

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

4205

Age (days ago)

4284

Last active (days ago)

List overview

Download

20 comments

5 participants

participants (5)

Ben Gamari
Edward Kmett
Richard Eisenberg
Roman Cheplyaka
Simon Peyton-Jones