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

Reply via email to