Kindness of strangers (or strangeness of Kinds)

[AntC]

 <wagnerdm <at> seas.upenn.edu> writes:

> 
> Quoting AntC <anthony_clayden <at> clear.net.nz>:
> 
> > {-# OPTIONS_GHC -XDataKinds -XPolyKinds -XKindSignatures	#-}
> >
> >     data MyNat = Z | S MyNat
> >
> >     class NatToIntN (n :: MyNat)
> >         where natToIntN :: (n :: MyNat) -> Int
> >     instance NatToIntN Z
> >         where natToIntN _ = 0
> >     instance (NatToIntN n) => NatToIntN (S n)
> >         where natToIntN _ = 1 + natToInt (undefined :: n)
> >
> > But GHC rejects the class declaration (method's type):
> >     "Kind mis-match
> >      Expected kind `ArgKind', but `n' has kind `MyNat'"
> > (Taking the Kind signature out of the method's type gives same message.)
> 
> At a guess, (->) :: * -> * -> *, but n :: MyNat, not n :: *, so (->) n  
> is badly kinded. In comparison:
> 
> >     data Proxy a = Proxy
> >
> >     class NatToInt (n :: MyNat)
> >         where natToInt :: Proxy (n :: MyNat) -> Int
> >     instance NatToInt Z
> >         where natToInt _ = 0
> >     instance (NatToInt n) => NatToInt (S n)
> >         where natToInt _ = 1 + natToInt (Proxy :: Proxy n)
> 
> Here Proxy n :: *, even if n :: MyNat, so Proxy n is a fine argument  
> to hand to (->).
> 
> ~d
> 

Thanks for the prompt response, and yes, you're right, so says GHCi:

:k (->) :: * -> * -> *          -- so `ArgKind` in the message means `*'

:k Proxy :: AnyK -> *           -- which answers what is `AnyKind'

So Proxy is a kind-level wormhole: forall k. k -> *
Singleton types are a wormhole from types to values.

For the natToInt method, it's a shame having to insert Proxy's everywhere -- 
it takes away from the parallel to value-level equations.

Perhaps I need promoted GADT's?

Or perhaps PolyKinded (->) :: k1 -> k2 -> k3?

AntC