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

[Roman Cheplyaka]

* TP <paratribulations at free.fr> [2013-05-22 18:45:06+0200]
> 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?

You seem to assume that Succ Zero will have type 'Succ 'Zero (i.e. the
promoted type), but it's not the case — it still has type Nat, as
always.

On the other hand, the type 'Succ 'Zero has kind 'Nat and doesn't have
any inhabitants — only types of kind * do.

So, how to fix this depends on what you want. For example, you can
change c2num to accept Proxy c instead of c. Or you can establish the
connection between Succ Zero and 'Succ 'Zero — again, using a (slightly
modified) Sing class. In the latter case, take a look at the
'singletons' package — it can do a lot of work for you.

Roman