PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Simon Peyton-Jones]

Friends

Thanks for this useful conversation, by email and at ICFP.  Here's my summary.  Please tell me if I'm on the right track.  It would be great if someone wanted to create a page on the GHC wiki to capture the issues and outcomes.

Simon

Eta rules
~~~~~~
*   We want to add eta-rules to FC.  Sticking to pairs for now, that would amount to
     adding two new type functions (Fst, Snd), and three new, built-in axioms
	axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
	axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
	axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
     Generalising to arbitrary products looks feasible.

*  Adding these axioms would make FC inconsistent, because 
	axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)
     and that has two different type constructors on each side.
     However, I think is readily solved: see below under "Fixing Any"

* Even in the absence of Any, it's not 100% obvious that adding the above
   eta axioms retains consistency of FC.  I believe that Richard is volunteering
   to check this out.  Right, Richard?

Type inference
~~~~~~~~~
I'm a little unclear about the implications for inference.  One route
might be this.   Suppose we are trying to solve a constraint
     [W]  (a:'(k1,ks)) ~ '( t1, t2 )
where a is an untouchable type variable.  (if it was touchable we'd
simply unify it.)  Then we can replace it with a constraint
    [W]   '(Fst a, Snd a) ~ '( t1, t2)

Is that it?  Or do we need more?  I'm a bit concerned about constraints like
    F a ~ e
where a:'(k1,k2), and we have a type instance like  F '(a,b) = ...

Anything else?

I don't really want to eagerly eta-expand every type variable, because (a) we'll bloat the constraints and (b) we might get silly error messages.  For (b) consider the insoluble constraint
    [W]  a~b
where a and b are both skolems of kind '(k1,k2). If we eta-expand both we'll get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b), and we DEFINITELY don't want to report that as a type error!

Fixing Any
~~~~~~~
* I think we can fix the Any problem readily by making Any into a type family, 
     that has no instances.   We certainly allow equalities with a type
     *family* application on the left and a type constructor on the right.
     I have implemented this change already... it seems like a good plan.
	
* Several people have asked why we need Any at all.  Consider this source program
         reverse []
     At what type should we instantiate 'reverse' and the empty list []?  Any type
     will do, but we must choose one; FC doesn't have unbound type variables.
     So I instantiate it at (Any *):
         reverse (Any *) ([] (Any *))

     Why is Any poly-kinded?  Because the above ambiguity situation sometimes 
     arises at other kinds.

*   I'm betting that making Any into a family will mess up Richard's (entirely separate)
     use of (Any k) as a proxy for a kind argument k; because now (Any k1 ~ Any k2)
     does not entail (k1~k2).   We need Any to be an *injective* type family.  We want
     injective type families anyway, so I guess I should add the internal machinery 
     (which is easy).

     I believe that injective type families are fully decomposable, just like data type families,
     correct?  To make them available at the source level, we'd just need to
       a) add the syntax     injective type family F a :: *
       b) check for injectivity when the user adds type instances
     Richard, would you like to do that part?