More GND + role inference woes

Wed Oct 16 16:46:04 UTC 2013

> On Oct 16, 2013, at 9:28 AM, Simon Peyton-Jones <simonpj at microsoft.com> 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.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?

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 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> 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/830a1637/attachment-0001.html>