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