Conor,
What happens when I say
newtype Jim = Hide Fred deriving Public
? I tried it. I get
blah :: EQ Jim Fred
Thinking of it; this *does* make sense in System FC. The newtype- declaration gives you as an axiom Hide :: Jim ~ Fred To give an instance of Public for Jim, we have to provide blah :: EQ Jim Fred which, with Refl :: forall (a :: *) (b :: *). (a ~ b) => EQ a b can be given straightforwardly as blah = Refl {Jim, Fred, Hide} So, the problem, if any, is that the System FC-encoding of newtypes renders them into "guarded" type equalities, rather than proper type isomorphisms. (Or, the other way around, reduces ~ to type isomorphism rather than type equality.)
I wonder if there's a potential refinement of the kind system lurking here, distinguishing *, types-up-to-iso, from |*|, types-up-to- identity. That might help us to detect classes for which newtype deriving is inappropriate: GADTs get indexed over |*|, not *; classes of *s are derivable, but classes of |*|s are not. I certainly don't have a clear proposal just now. It looks like an important distinction: recognizing it somehow might buy us something.
That seems a promising approach. We would then have Jim :: * Fred :: * EQ :: |*| -> |*| -> * Hide :: Jim ~ Fred Refl :: forall (a :: |*|) (b :: |*|). (a ~ b) => EQ a b and (I guess) a type-level operation that allows you to lift every type T :: * into |T| :: |*|. Then we have, blahFred = Refl {|Fred|, |Fred|, |Fred|} which make sense, given that |*| :: TY, but both blahJim = Refl {Jim, Fred, Hide} and blahJim' = Refl {|Jim|, |Fred|, Hide} and variations thereof would be ill-kinded, as desired. And, indeed, generalised newtype deriving should then only make sense for *-indexed classes. I think this would work. Cheers, Stefan