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

[TP]

Roman Cheplyaka wrote:

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

Thanks Roman.
Unfortunately, I already tried that (without the constraint "Typeable a =>", 
what a fool), but it did not work. The error is the same with the 
constraint:

    Derived typeable instance must be of form (Typeable 'Succ)
    In the stand-alone deriving instance for
      ‛Typeable a => Typeable (Succ a)’

What is the problem?

Is it possible that it is a bug in GHC? Indeed, we had unwanted similar 
error messages recently:

http://hackage.haskell.org/trac/ghc/ticket/7704

Thanks,

TP

PS: the complete program for a test that shows the error:
----------------------
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

import Data.Typeable

data Nat = Zero | Succ Nat
    deriving ( Show, Eq, Ord, Typeable )

deriving instance Typeable 'Zero
deriving instance Typeable a => Typeable ('Succ a)

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