Try adding
deriving instance Typeable 'Zero
deriving instance Typeable a => Typeable ('Succ a)
to your module.
(I haven't tested it — you might need to tweak it a bit.)
Roman
* TP
Hi all,
I try to play with the "Typeable" typeclass, and I have some difficulties to make it work in this simple case where I use type-level naturals:
--------------------- {-# LANGUAGE GADTs #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE StandaloneDeriving #-}
import Data.Typeable
data Nat = Zero | Succ Nat deriving ( Show, Eq, Ord, Typeable )
data Box where Box :: (Typeable s, Show s, Eq s) => s -> Box deriving Typeable
data Proxy a = P deriving Typeable
deriving instance Show Box instance Eq Box where
(Box s1) == (Box s2) = Just s1 == cast s2
main = do
let one = undefined :: Main.Proxy ('Succ 'Zero) let foo = Box one print foo ---------------------
I obtain:
--------------------- No instance for (Typeable Nat 'Zero) arising from a use of ‛Box’ In the expression: Box one In an equation for ‛foo’: foo = Box one In the expression: do { let one = ...; let foo = Box one; print foo } ---------------------
Note that it is necessary to use the HEAD version of GHC to obtain this message (I use version 7.7.20130525); with GHC 7.6.2, the message is different because recent improvements in Typeable are not present (1).
What is the problem? I've tried different things without success. Tell me if the "beginners" diffusion list is more suitable than Haskell- Cafe.
Thanks,
TP
(1): http://hauptwerk.blogspot.fr/2012/11/coming-soon-in-ghc-head-poly-kinded.htm...
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe