Kindness of strangers (or strangeness of Kinds)

[wagnerdm at seas.upenn.edu]

Quoting AntC <anthony_clayden at clear.net.nz>:

> {-# OPTIONS_GHC -XDataKinds -XPolyKinds -XKindSignatures	#-}
>
>     data MyNat = Z | S Nat
>
>     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