José Pedro Magalhães wrote: >> Oh, it should probably be simply >> >> deriving instance Typeable 'Zero >> deriving instance Typeable 'Succ >> > > Yes, that's how it should be. Please let me know if that > doesn't work.
Thanks, it works perfectly like that. I don't understand exactly why the previous syntax did not work, but maybe it will be clearer when I finish the paper "Scrap your boilerplate: a practical design pattern for generic programming" (anyway, this paper seems very interesting). Output of the code: --------------------- $ runghc-head test_typeable.hs Box test_typeable.hs: Prelude.undefined --------------------- Maybe the "Box " in front of the line is strange, but it is OK: "one" is undefined, not "Box one". This is the full tested code, for sake of reference: ----------------------- {-# LANGUAGE GADTs #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE StandaloneDeriving #-} import Data.Typeable data Nat = Zero | Succ Nat deriving ( Show, Eq, Ord ) deriving instance Typeable 'Zero deriving instance Typeable 'Succ data Box where Box :: (Typeable s, Show s, Eq s) => s -> Box deriving Typeable data Proxy a = P deriving (Typeable, Show, Eq) 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 ---------------------- Thanks a lot, TP _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe