I think it would be ok to expect the constructors to be visible, even though it might need to a lot being needed.

BTW I think you might need S1 visible as well otherwise how would you convert (S1 True :: S Bool Int) into (S1 True :: S Bool Age)?

If you don't derive the role from constructor visibility then I think it should fail-safe and default to the nominal role - valid Haskell 2010 code shouldn't be exposed to an abstraction leak just because it's GHC compiling it.


On 08/10/2013 14:23, Richard Eisenberg wrote:
Pedro is suggesting a way for a Haskell type-level program to gain access to role information. This might indeed be useful, but it doesn't seem terribly related to the problem of defaults / abstraction. The problem has to do with definitions like these:

> module A where
> data S a b = S1 a | S2 b
> data T a b = MkT (S a b)

> module B where
> import A ( {- what goes here? -} )
>
> class C a where
>   mkT :: T Bool a
>
> instance C Int where ...
> newtype Age = MkAge Int deriving C

What constructors do we need in order to convert the (C Int) instance to (C Age) by hand? To me, it looks like we need MkT and S2, but not S1. Yet, this is not obvious and seems to be quite confusing.

I hope this helps understanding the issue!
Richard

On Oct 8, 2013, at 4:01 AM, José Pedro Magalhães <dreixel@gmail.com> wrote:

Hi,

On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg <eir@cis.upenn.edu> wrote:
We considered this for a while, but it led to a strange design -- to do it right, you would have to import all constructors for all datatypes *recursively* out to the leaves, starting at the datatypes mentioned in the class for which you wanted to use GND. This would mean potentially a whole lot of imports for symbols not actually used in the text of a program.

I'm not sure I understand why constructors are involved in this. Wouldn't something like
the following potentially be useful?

data Role = Nominal | Representational | Phantom | Fun Role Role

type family HasRole (t :: k) :: Role

data MyData a b = MyData a
data MyGADT a b where MyGADT :: MyGADT a Int

type instance HasRole MyData      = Fun Representational Phantom
type instance HasRole MyGADT      = Fun Representational Nominal
type instance HasRole Traversable = Nominal


HasRole instances would be automatically given by GHC.


Cheers,
Pedro