Hello,

Apologies if my changes caused difficulties with your work---we made the changes to `Typable` to preserve the soundness of the type system, hopefully the new behavior is exactly equivalent to the old in the safe cases. 

Could you post an example of the code where the unwanted `Typeable p` constraint appears?  It seems entirely reasonable that if you want to solve `Typeable (OUT p o)`, you'll have to provide `Typealbe p`, so I am not seeing the whole picture.

To answer your question about `KnownNat p`---there is no relation between it and `Typeable`.   You may think if a `KnownNat x` constraint as just the integer `x`.  As it happens, the integer is closely related to the `Typeable` instance for the number, so I think we *could* make it work so that if you have `KnownNat p`, then you can get `Typeable p`, but this has never worked previosly, so perhaps there is another issue.

-Iavor



On Thu, Apr 23, 2015 at 7:04 AM, Gabor Greif <ggreif@gmail.com> wrote:
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...