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

On Wed, Jun 5, 2013 at 8:46 AM, Roman Cheplyaka wrote:

* TP [2013-06-05 00:37:36+0200]

...

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?

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. (Sorry for taking so long to reply to this...) Cheers, Pedro

Roman

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Hi, On Wed, Jun 5, 2013 at 11:21 PM, TP wrote:

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

It's an interesting paper, but I'm afraid it won't help you understand what's going on. Typeable is changing in GHC 7.8 to become poly-kinded. You are using Typeable instances for things which are not of kind *, so you need this new poly-kinded variant. The SYB paper says nothing about polykinds (it was written way before polykinds came up). You can find some more information on the new Typeable here: http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/PolyTypeable By the way, you can also get those Typeable instances derived automatically if you use the LANGUAGE pragma AutoDeriveTypeable. This is also documented in the HEAD user's guide. Cheers, Pedro

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