Quoting AntC <anthony_clay...@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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
