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

[Simon Peyton-Jones]

I think I was a little hasty below, and need a little help.

Making 'Any' an type family, even an injective one, does not work for the use that Richard and Iavor make of it, eg in TypeLits.  Here's an example from TypeLits:

	instance SingE (Any :: Nat) Integer where
where SingE :: forall k. k -> * -> Constraint

Here Iavor is using Any as a proxy kind argument.  He really wants
	SingE :: forall k. * -> Constraint
with kind-indexed instances. But (much as with the Typeable class at the value level) he is giving it a type argument so that he can later say things like
	SingE (Any :: *->*) v
Without this trick we'd need kind application, something like
	SingE {*->*} v

None of this works if Any is a type family, because the type patterns in an instance decl aren't allowed to involve type families (and rightly so; value declarations don't have functions in patterns).

Nor can we fix this by introducing some *other* constant, Proxy :: forall k. k, because that suffers from the inconsistency problem that we started with.  Another way to say this is as follows.  In the value world we have often written
	typeOf (undefined :: a)
using bottom as a proxy type argument. That works in Haskell, but not in a strict, or strongly-normalising language.  And at the type level we are (mostly) strongly normalising.


The technically-straightforward thing to do is to add kind application, but that's a bit complicated notationally.  http://hackage.haskell.org/trac/ghc/wiki/ExplicitTypeApplication   Does anyone have any other ideas?

Simon


| -----Original Message-----
| From: Simon Peyton-Jones
| Sent: 16 September 2012 16:49
| To: Richard Eisenberg; Andrea Vezzosi
| Cc: Adam Gundry; Conor McBride; Stephanie Weirich; glasgow-haskell-
| users at haskell.org; Simon Peyton-Jones
| Subject: RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
| functional dependency?
| 
| 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?