Question about Roles and the AMP work

[Simon Peyton Jones]

This looks a bit awkward to me.  Here's a small test case 

class C m where
  ret :: a -> m a
  bind :: m a -> (a -> m b) -> m b
  join :: m (m a) -> m a

newtype T m a = MkT (m a) deriving( C )

This is accepted without the 'join' in the class, but rejected with it.

So *all* uses of GND to do 'deriving( Monad )' will break when 'join' is added to Monad.

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.

I can't think of an obvious workaround either, except not putting 'join' in Monad.

Simon



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