[Haskell-cafe] accessing a type variable in instance declaration

[TP]

Roman Cheplyaka wrote:

> You are confusing type and value variables.
> 
>   c2num order
> 
> means apply the function 'c2num' to the value variable 'order', which is
> not defined.
> 
> To get from a type to a value you can use a type class 'Sing' (for
> 'singleton')
> 
>   class Sing a where
>     sing :: a
> 
>   instance Sing Zero where
>     sing = Zero
> 
>   instance Sing a => Sing (Succ a) where
>     sing = Succ sing
> 
> After adding the appropriate constraint to the instance, you can write
>   
>   show $ c2num $ (sing :: order)

Ok, thanks, I understand. Now, I'm stuck to compile this code (independent 
from my previous post, but related to it):

---------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data Nat = Zero | Succ Nat
type One = Succ Zero
type Two = Succ One

-- class Cardinal c where   -- line 1
class Cardinal (c::Nat) where  -- line 2
    c2num :: c -> Integer
    cpred :: (Succ c) -> c
    cpred = undefined

instance Cardinal Zero where
    c2num _ = 0

instance (Cardinal c) => Cardinal (Succ c) where
    c2num x = 1 + c2num (cpred x)

main = do

print $ show $ c2num (undefined::Succ (Succ Zero))
print $ show $ c2num (undefined::Two)
-----------------

With line 2, I get:

test_nat.hs:11:14:
    Kind mis-match
    Expected kind `OpenKind', but `c' has kind `Nat'
    In the type `c -> Integer'
    In the class declaration for `Cardinal'

With line 1 instead, I get:

    Kind mis-match
    The first argument of `Succ' should have kind `Nat',
    but `c' has kind `*'
    In the type `(Succ c) -> c'
    In the class declaration for `Cardinal'

So, in the first case, c has a too restricted kind, and in the second one, 
it has a too broad kind in the definition of cpred. I have tried several 
things without any success.
How to compile that code?

Thanks,

TP