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

22 May 2013

      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