PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
simonpj at microsoft.com
Sun Sep 16 17:49:05 CEST 2012
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.
* 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?
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) = ...
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
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!
* 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
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?
More information about the Glasgow-haskell-users