On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg <eir@cis.upenn.edu> wrote:
Now I think we're on the same page, and I *am* a little worried about the sky falling because of this. (That's not a euphemism -- I'm only a little worried.)
 
=)
 
Wait! I have an idea!
The way I've been describing GND all along has been an abbreviation. GHC does not coerce a dictionary from, say, Ord Int to Ord Age. Instead, GHC mints a fresh dictionary for Ord Age where all the methods are implemented as coerced versions of the methods for Ord Int. (I'm not sure why it's implemented this way, which is why I've elided this detail in just about every conversation on the topic.) With this in mind, I have a proposal:

1) All parameters of all classes have nominal role.
2) Classes also store one extra bit per parameter, saying whether all uses of that parameter are representational. Essentially, this bit says whether that parameter is suitable for GND. (Currently, we could just store for the last parameter, but we can imagine extensions to the GND mechanism for other parameters.)

Because GND is implemented using coercions on each piece instead of wholesale, the nominal roles on classes won't gehingt in the way of proper use of GND. An experiment (see below for details) also confirms that even superclasses work well with this idea -- the superclasses aren't coerced.

Under this proposal, dictionaries can never be coerced, but GND would still seem to work.

Thoughts?

This strikes me as a remarkably straightforward solution. Does it strike you as something implementable in time for 7.8 though?

 
Richard

Experiment:

newtype Age = MkAge Int

instance Eq Age where
  _ == _ = False

deriving instance Ord Age

useOrdInstance :: Ord a => a -> Bool
useOrdInstance x = (x == x)

What does `useOrdInstance (MkAge 5)` yield? It yields `False` (in HEAD). This means that the existing GND mechanism (I didn't change anything around this part of the code) uses superclass instances for the *newtype*, not for the *base type*. So, even with superclasses, class dictionaries don't need to be coerced.

Upon reflection it makes a lot of sense that GND has to mint a new dictionary, because the superclasses may differ, like you showed here.

-Edward