* TP
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