Let me start by saying that I'm happy we're trying to fix the GND problem. Thanks for working on that.
That being said: is this ready for mainstream consumption? We're forcing this on everyone without any language pragma or flags to opt-in/out. That is bad if we're not sure we're doing the right thing in some cases or if we're causing spurious failures. At ICFP I got the impression that very few people will be affected, but Bryan's result suggests there are more people than I thought. On Thu, Oct 10, 2013 at 8:26 PM, Richard Eisenberg <e...@cis.upenn.edu>wrote: > In Bryan's recent test of GHC 7.8 against all of Hackage, there were three > spurious errors caused by lack of role abstraction. Here are the class > definitions where a nominal parameter is inferred, probably against the > wishes of the author: > > from logict-0.2.3/Control.Monad.Logic.Class: > > class (MonadPlus m) => MonadLogic m where > > msplit :: m a -> m (Maybe (a, m a)) > > from monadLib-3.5.2/MonadLib: > > class (Monad m) => ReaderM m i | m -> i where > > ask :: m i > > from base/Control.Arrow: > > class Arrow a => ArrowApply a where > > app :: a (a b c, b) c > > In each of these, the last parameter of the class is given a nominal role > because it appears as the parameter of a type variable. However, in each > case, it appears as the parameter of a *class* type variable. This means > that, if we somehow knew that the class author wanted the class to be > usable with GND, we could simply check every instance declaration for that > class to make sure that the relevant concrete instantiation has the right > role. For example, when the user writes, for example > > > instance ArrowApply Foo where … > > we check that Foo's first parameter has a representational role. If it > doesn't, then the instance is rejected. > > An alternative, somewhat heavier idea would be to represent roles as class > constraints. We could have > > > class NextParamNominal (c :: k) > > class NextParamRepresentational (c :: k) > > GHC could "generate" instances for every datatype definition. For example: > > > type role Map nominal representational > > data Map k v = … > > would induce > > > instance NextParamNominal Map > > instance NextParamRepresentational (Map k) > > Users would not be able to write these instances -- they would have to be > generated by GHC. (Alternatively, there could be no instances, just a > little magic in the constraint solver. Somewhat like Coercible.) > > Then, the classes above would just have to add a superclass, like this: > > > class (Arrow a, NextParamRepresentational a) => ArrowApply a where > > app :: a (a b c, b) c > > The role inference mechanism would be made aware of role constraints and > use this one to derive that ArrowApply is OK for GND. > > This "heavier" approach has a similar upshot to the first idea of just > checking at instance declarations, but it is more customizable and > transparent to users (I think). > > > I'm not sure I'm advocating for this change (or volunteering to implement > before the release candidate), but I wanted to document the idea and get > any feedback that is out there. This would fix the breakage we've seen > without totally changing the kind system. > > Thanks, > Richard > > PS: Due credit is to migmit for suggesting the type-class idea on > glasgow-haskell-users. > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://www.haskell.org/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
