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