<div dir="ltr">Hello,<div><br></div><div>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. </div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Apr 23, 2015 at 7:04 AM, Gabor Greif <span dir="ltr"><<a href="mailto:ggreif@gmail.com" target="_blank">ggreif@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi devs,<br>
<br>
between ghc-7.11.20150215 and ghc-7.11.20150407 I experienced a<br>
strange regression with deriving Typeable for data with Nat-kinded<br>
indices.<br>
<br>
Something like this used to work (I cannot post the whole thing, unfortunately)<br>
<br>
{{{<br>
data OTU (p :: Nat) (o :: Nat) = OTU { ...fields... } deriving (Show, Typeable)<br>
}}}<br>
<br>
With my ghc-7.11.20150407 (and later) strange obligations of the form<br>
`Typeable p` appear, rendering my code uncompilable. But there is no<br>
way I can see how I can convince the type checker that the Nat index<br>
is indeed Typeable. I *do* have a `KnownNat p` constraint around,<br>
though.<br>
<br>
The relevant changes to mainline appear to be<br>
<a href="https://github.com/ghc/ghc/commit/b359c886cd7578ed083bcedcea05d315ecaeeb54" target="_blank">https://github.com/ghc/ghc/commit/b359c886cd7578ed083bcedcea05d315ecaeeb54</a><br>
<a href="https://github.com/ghc/ghc/commit/3a0019e3672097761e7ce09c811018f774febfd2" target="_blank">https://github.com/ghc/ghc/commit/3a0019e3672097761e7ce09c811018f774febfd2</a><br>
<br>
both by Iavor.<br>
<br>
So now my questions:<br>
<br>
1) Is this a regression on mainline? (I surely hope so!) How did this<br>
work before?<br>
2) Should `KnownNat p` imply `Typeable p` for the ability to have my<br>
`Typeable (OTU p o)`<br>
3) if 2) is answered with "NO", how am I supposed to satisfy those constraints?<br>
<br>
Thanks and cheers,<br>
<br>
    Gabor<br>
<br>
<br>
PS: Sometimes I feel like a canary doing my research-like programming<br>
with GHC-HEAD, and it is a mostly positive experience, but events like<br>
this make me shiver...<br>
</blockquote></div><br></div></div>