deriving Typeable and Nat kinds

Gabor Greif ggreif at
Thu Apr 23 14:04:31 UTC 2015

Hi devs,

between ghc-7.11.20150215 and ghc-7.11.20150407 I experienced a
strange regression with deriving Typeable for data with Nat-kinded

Something like this used to work (I cannot post the whole thing, unfortunately)

data OTU (p :: Nat) (o :: Nat) = OTU { ...fields... } deriving (Show, Typeable)

With my ghc-7.11.20150407 (and later) strange obligations of the form
`Typeable p` appear, rendering my code uncompilable. But there is no
way I can see how I can convince the type checker that the Nat index
is indeed Typeable. I *do* have a `KnownNat p` constraint around,

The relevant changes to mainline appear to be

both by Iavor.

So now my questions:

1) Is this a regression on mainline? (I surely hope so!) How did this
work before?
2) Should `KnownNat p` imply `Typeable p` for the ability to have my
`Typeable (OTU p o)`
3) if 2) is answered with "NO", how am I supposed to satisfy those constraints?

Thanks and cheers,


PS: Sometimes I feel like a canary doing my research-like programming
with GHC-HEAD, and it is a mostly positive experience, but events like
this make me shiver...

More information about the ghc-devs mailing list