Yuck yuck yuck -- that's what I think. Austin's analysis below agrees with mine. The error *is* reasonable, because if `coerce` worked in this scenario, a particularly dastardly (and very un-Lawful) Monad instance could break type safety.
Furthermore, I think it's absolutely necessary that Monad remain GND'able. It's a common idiom, and I use it myself quite frequently. What to do? Here are some possible ways forward: 1) Implement the second half of roles (as in the original POPL "Generative type abstraction" paper). This would make roles more first-class and allow us to say something like > class Applicative m => Monad (m :: representational -> *) where ... Under this scenario, all Monad instances would need to be over types with a representational argument, and then `coerce`ing join would be sound. (Actually, we would probably put the representational constraint as a superclass of Functor, but you get the idea.) There are two downsides to this: a) implementing the much-more complicated role scenario, and b) a GADT could not be a Monad any more. I do actually think (b) would bite some users. 2) Don't put `join` in Monad. Sorry for asking a perhaps-obvious question, but why put `join` in Monad at all? Are there examples where doing this would increase efficiency? 3) Something along the lines of Edward's suggestion. As he admits, his idea is still incomplete, but I think it would snag a lot of cases. If the current roles machinery works 95% of the time, the current machinery + built-in support for Edward's idea would get 99.5% of real use cases, I would think. It is a little "hackish" and somewhat unprincipled, but I think it would work in practice. I would even have GHC produce the `Representational` instances automatically. Richard On May 12, 2014, at 8:53 AM, Austin Seipp <aus...@well-typed.com> wrote: > 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@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs