[Haskell-cafe] Typeable typeclass and type-level naturals

Roman Cheplyaka roma at ro-che.info
Mon Jun 3 00:35:37 CEST 2013


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 <paratribulations at free.fr> [2013-06-02 18:08:02+0200]
> 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.html
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe



More information about the Haskell-Cafe mailing list