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

2 Jun 2013

      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...