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

[Richard Eisenberg]

Please see my responses inline.

On Sep 16, 2012, at 11:49 AM, Simon Peyton-Jones wrote:

> 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.

The last two axioms are the straightforward compilations of the type families Fst and Snd -- nothing new is needed to create these. The first is the challenge and will require some type inference magic.

> 
> *  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?

I'll be going through the consistency proof shortly for some other work I'm doing, so I'll throw this into the mix while it's all paged in. This might be tricky, though.

> 
> 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)

I don't think that's the right replacement. The next natural step would be decomposition, leading to (Fst a ~ t1) and (Snd a ~ t2), which would then get stuck, because Fst and Snd  aren't injective. So, I would say we need

  a1, a2 fresh
  [G] a ~ '(a1, a2)
  [W] '(a1, a2) ~ '(t1, t2)

which would then decompose correctly. As I write this, I'm worried about that freshness condition… what if 'a' appears multiple times in the type? We would either need to guarantee that a1 and a2 are the same each time, or create new [W] constraints that a1 ~ a1', etc. But, maybe this is easier in practice than it seems. Type inference experts?

> 
> 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) = …

Here, the proper eta-expansion (a ~ '(Fst a, Snd a)) works great, no?

> 
> 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!

Could this be handled using mechanisms already in place to report errors about unexpanded type synonyms? If so, we could eagerly expand, and I think that would ease the implementation. However, I defer to those more expert than I in such issues.

> 
> 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 don't think injectivity is the key here. As I understand it, any equality t1 ~ t2 entails k1 ~ k2, where t1:k1 and t2:k2. When trying to unify Any k1 ~ Any k2, GHC will already (I think) unify k1 and k2, just based on the kinds, not on injectivity. Is there something here I'm missing?

> 
>     I believe that injective type families are fully decomposable, just like data type families,
>     correct?

No, I don't think so. Data families are generative, which is a stronger condition than injective. Consider (D a ~ b c), where D is a data family (or a constructor, for that matter). Then, we can surely decompose to (D ~ b, a ~ c). However, the same is not true for type families. If we have (F a ~ b c), we can't go further, even if F is injective. If we have (F a ~ F b), where we know F is injective, then we can decompose to (a ~ b), but that's the only gain we get.

>  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?
> 

A long, long time ago, I volunteered to look at injectivity of type functions. That task it quite literally on my todo list, but it feels like I'm getting through a long season of putting out fires, and injectivity hasn't been burning brightly enough. I think the last of the brightly-burning ones will either be extinguished or go out on its own on October 8 (PLPV deadline). After that date, I'll have more of a chance to look at this. 

Simon, if you add the internal machinery, I'm happy to do the external stuff -- shouldn't be hard.

> 
> 

As for recovering "kind classes" and such once Any is made into a type family: I'm in favor of finding some way to do explicit kind instantiation, making the Any trick obsolete. I'm happy to leave it to others to decide the best concrete syntax.

Richard