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

[TP]

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