Re: Kindness of strangers (or strangeness of Kinds)

Quoting AntC :

{-# 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