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

[Nicolas Frisby]

On Wed, Sep 19, 2012 at 1:51 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> 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.

I'll admit I haven't parsed this entire email thread, but I read
enough of it early on that I wanted to avoid Any recently. Returning
to find this quote from Richard, perhaps the trick I came up is the
one you're after.

(Also — what's the general status on this initiative? Has much
happened in about a month?)

The to my trick key is to use the promotion of this data type.

> data KindProxy (k :: *) = KindProxy

I needed it in order to define this family, which counts the number of
arguments a kind has.

> type family CountArgs (kp :: KindProxy k) :: Nat
> type instance CountArgs (kp :: *) = Z
> type instance CountArgs (kp :: kD -> kR) = S (CountArgs ('KindProxy :: KindProxy kR))

The proxy is necessary on the RHS of the second instance, in which I
need a type of kind kR, but I wouldn't have any means to build one
(without Any) were CountArgs simply of kind (k -> Nat).

This usage is comparable to Richard's usage in the singletons library,
insomuch as I understand from the Haskell 2012 paper.

I'm less familiar with the usage in GHC.TypeLits. At a quick glance, I
believe I'd change SingE like so

> class SingE (kparam :: KindProxy k) rep | kparam -> rep where
>   fromSing :: Sing (a :: k) -> rep

> instance SingE (kparam :: KindProxy Nat) Integer where
>   fromSing (SNat n) = n

> instance SingE (kparam :: KindProxy Symbol) String where
>   fromSing (SSym s) = s

However, looking through the rest of that module, I see no point where
a proxy is actually required (as it is required in the second case of
CountArgs). Maybe I'm just missing it, or maybe Iavor is just
interested in *enforcing* the fact that the type is not of
consequence?

Along those same lines… Iavor had SingE instances declared for (Any ::
KindProxy Nat) and (Any :: KindProxy Symbol). I'm not sure why he
didn't leave the type polymorphic, as I have. Perhaps it matters for
various uses of SingE? I haven't tried using my code with examples, so
maybe that's where issues would show up. If it were necessary, the
instances could instead be as follows.

> instance SingE ('KindProxy :: KindProxy Nat) Integer where
>   fromSing (SNat n) = n

> instance SingE ('KindProxy :: KindProxy Symbol) String where
>   fromSing (SSym s) = s

Is this the kind of trick you were after, Richard? It might pollute
the code base and interface a bit with KindProxy wrappers, but I've
not found that insurmountable. Hopefully that isn't a show stopper for
you.

HTH