* TP <paratribulati...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe