deriving Typeable and Nat kinds

Gabor Greif ggreif at gmail.com
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
indices.

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

The relevant changes to mainline appear to be
https://github.com/ghc/ghc/commit/b359c886cd7578ed083bcedcea05d315ecaeeb54
https://github.com/ghc/ghc/commit/3a0019e3672097761e7ce09c811018f774febfd2

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,

    Gabor


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