<div dir="ltr">As a straw man, if we went to a typeclass-driven 'next arg is representational' approach then we could possibly recover 'join' here.<div><br></div><div>e.g.</div><div><br></div><div><font face="courier new, monospace">class Representational f where</font></div>
<div><span style="font-family:'courier new',monospace">  rep :: Coercion f g -> Coercion a b -> Coercion (f a) (g b)</span><br></div><div><font face="courier new, monospace"> </font></div><div><font face="courier new, monospace">class Representational f => Phantom f where</font></div>
<div><font face="courier new, monospace">  phantom :: Coercion f g -> Coercion (f a) (g b)</font></div><div><br></div><div>When we look at for the constraint head <font face="courier new, monospace">Coercible (f a) (g b)</font> we'd then check for <font face="courier new, monospace">Phantom f</font> and if so look for <font face="courier new, monospace">Coercible f g</font>, or fall back to <font face="courier new, monospace">Representational f,</font> and look for <font face="courier new, monospace">Coercible f g</font> and <font face="courier new, monospace">Coercible a b</font>.</div>
<div><br></div><div>Then to derive GND for <font face="courier new, monospace">C m</font> it'd need to check <font face="courier new, monospace">Representational m</font> due to the type of join needing <font face="courier new, monospace">m</font>'s next arg to be representational, find it and move on.</div>
<div><br></div><div>The set of these instances can be left open like any other typeclass and users could supply their own for tricky conversions if need be.</div><div><br></div><div>If you just wrote the existing role annotations, but let them request currently impossible roles you could use the desired role to infer the constraints involved.</div>
<div><br></div><div>e.g.</div><div><br></div><div><font face="courier new, monospace">newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }<br></font></div><div><br></div><div>should be able to derive something like</div>
<div><br></div><div><font face="courier new, monospace">instance Representational (StateT s)<br></font></div><div><font face="courier new, monospace">instance Representational m => Representational (StateT s m)<br></font></div>
<div><font face="courier new, monospace">instance Phantom m => Phantom (StateT s m)</font></div><div><br></div><div>If we put nominal or representational on the m argument </div><div><br></div><div><font face="courier new, monospace">type role StateT nominal nominal nominal</font></div>
<div><br></div><div>then we could just elide the instances for anything lower in the nominal -> representational -> phantom lattice than the named role.</div><div><br></div><div>The positional argument scheme isn't perfect, as in the above it'd fail to let you derive <font face="courier new, monospace">`instance Representational StateT`</font> due to the s occurring under m, an argument later in the argument list, but it does fix most of the problems with Coercible and monad transfomers.</div>
<div><br></div><div>There might be some fancier form that can cover all of the use cases, but I'm not seeing it off hand.</div><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Tue, May 13, 2014 at 12:59 AM, Simon Peyton Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
This looks a bit awkward to me.  Here's a small test case<br>
<br>
class C m where<br>
  ret :: a -> m a<br>
  bind :: m a -> (a -> m b) -> m b<br>
  join :: m (m a) -> m a<br>
<br>
newtype T m a = MkT (m a) deriving( C )<br>
<br>
This is accepted without the 'join' in the class, but rejected with it.<br>
<br>
So *all* uses of GND to do 'deriving( Monad )' will break when 'join' is added to Monad.<br>
<br>
And this is because we don't know that 'm' ranges only over things that have representational arguments; type variables always have nominal arguments.  The paper draws attention to this shortcoming, but now it's becoming important.<br>

<br>
I can't think of an obvious workaround either, except not putting 'join' in Monad.<br>
<span class="HOEnZb"><font color="#888888"><br>
Simon<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
<br>
| -----Original Message-----<br>
| From: ghc-devs [mailto:<a href="mailto:ghc-devs-bounces@haskell.org">ghc-devs-bounces@haskell.org</a>] On Behalf Of Austin<br>
| Seipp<br>
| Sent: 12 May 2014 13:53<br>
| To: <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
| Subject: Question about Roles and the AMP work<br>
|<br>
| Hello all,<br>
|<br>
| While picking the AMP patch back up, it is almost ready to go, but I got<br>
| quite a puzzling error when attempting to build 'haskeline' with the AMP<br>
| changes. I don't seem to remember encountering this error before - but<br>
| maybe my mind is hazy.<br>
|<br>
| The error in question is this:<br>
|<br>
| <a href="https://gist.github.com/thoughtpolice/6df4c70d8a8fb711b282" target="_blank">https://gist.github.com/thoughtpolice/6df4c70d8a8fb711b282</a><br>
|<br>
| The TL;DR is that the move of `join` into base has caused a problem<br>
| here. The error really speaks for itself: GND tries to derive an<br>
| instance of `join` for DumbTerm, which would have the type<br>
|<br>
|   join :: DumbTerm m (DumbTerm m a) -> DumbTerm m a<br>
|<br>
| and be equivalent to join for StateT. But this can't hold: DumbTerm<br>
| should unwrap directly to StateT (by newtype equality) and thus the<br>
| third parameter to StateT in this case is `DumbTerm m a` if you expand<br>
| the types - but because this argument is Nominal, it cannot unify with<br>
| 'PosixT m', which is the actual definition of DumbTerm in the first<br>
| place!<br>
|<br>
| With a little thought, this error actually seems reasonable. But it<br>
| puzzles me as to what we should do now. One thing we could do is just<br>
| write the instances manually, of course. But that's a bit annoying.<br>
|<br>
| Another alternative (and also unfortunate) change is to leave `join` out<br>
| of Monad, in which case the GND mechanism is oblivious to it and does<br>
| not need to worry about deriving these cases.<br>
|<br>
| I am not sure how many packages depend on using GND to derive monads<br>
| like StateT with Nominal arguments, but I imagine it is not totally<br>
| insignificant and will essentially hurt a lot of people who may use it.<br>
|<br>
| Richard, I'm particularly interested to hear what you think. This one<br>
| sort of snuck up!<br>
|<br>
| (NB: despite this, the AMP work is very close to landing in HEAD, at<br>
| which point we can begin cleaning stuff up faster.)<br>
|<br>
| --<br>
| Regards,<br>
|<br>
| Austin Seipp, Haskell Consultant<br>
| Well-Typed LLP, <a href="http://www.well-typed.com/" target="_blank">http://www.well-typed.com/</a><br>
| _______________________________________________<br>
| ghc-devs mailing list<br>
| <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
| <a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
</div></div></blockquote></div><br></div>