<div dir="ltr">Could you please make a ticket for this, so that we have a reference and it does not get lost?</div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Apr 23, 2015 at 9:59 AM, Iavor Diatchki <span dir="ltr"><<a href="mailto:iavor.diatchki@gmail.com" target="_blank">iavor.diatchki@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Aha, I see what happened. What I said before was wrong---indeed the `Typeable` instance for type-nats (and symbols) used to be implemented in terms of `KnownNat` and `KnownSymbol`:</div><div><br></div><div>instance KnownNat n => Typeable (n :: Nat) where ...<br></div><div><br></div><div>When I updated the `Typeable` solver, I forgot about that special case---I'll have a go at a fix.</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>-Iavor<br></div><div><br></div><div><br></div><div><br></div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Apr 23, 2015 at 8:37 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">On 4/23/15, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank">iavor.diatchki@gmail.com</a>> wrote:<br>
> Hello,<br>
><br>
<br>
Hi Iavor,<br>
<span><br>
> Apologies if my changes caused difficulties with your work---we made the<br>
> changes to `Typable` to preserve the soundness of the type system,<br>
> hopefully the new behavior is exactly equivalent to the old in the safe<br>
> cases.<br>
<br>
</span>No need to apologize, I chose this way to be able to intervene fast<br>
when something breaks :-) The old behaviour might have been unsafe,<br>
though I cannot see why.<br>
<span><br>
><br>
> Could you post an example of the code where the unwanted `Typeable p`<br>
> constraint appears? It seems entirely reasonable that if you want to solve<br>
> `Typeable (OUT p o)`, you'll have to provide `Typealbe p`, so I am not<br>
> seeing the whole picture.<br>
<br>
</span>Here is a small example where an additional constraint surfaces:<br>
<br>
------------------------------------------------------------------------------<br>
{-# LANGUAGE AutoDeriveTypeable, GADTs, DataKinds, KindSignatures,<br>
StandaloneDeriving #-}<br>
<br>
import GHC.TypeLits<br>
import Data.Typeable<br>
<br>
data Foo (n :: Nat) where<br>
Hey :: KnownNat n => Foo n<br>
<br>
deriving instance Show (Foo n)<br>
<br>
data T t where<br>
T :: (Show t, Typeable t) => t -> T t<br>
<br>
deriving instance Show (T n)<br>
<br>
{-<br>
<br>
------------------- WITH ghci-7.11.20150407 (and newer)<br>
*Main> :t T Hey<br>
T Hey :: (Typeable n, KnownNat n) => T (Foo n)<br>
<br>
------------------- WITH ghci-7.11.20150215 (old)<br>
*Main> :t T Hey<br>
T Hey :: KnownNat n => T (Foo n)<br>
<br>
-}<br>
------------------------------------------------------------------------------<br>
<span><br>
<br>
><br>
> To answer your question about `KnownNat p`---there is no relation between<br>
> it and `Typeable`. You may think if a `KnownNat x` constraint as just the<br>
> integer `x`. As it happens, the integer is closely related to the<br>
> `Typeable` instance for the number, so I think we *could* make it work so<br>
<br>
</span>Yes, this relation I was alluding to.<br>
<span><br>
> that if you have `KnownNat p`, then you can get `Typeable p`, but this has<br>
> never worked previosly, so perhaps there is another issue.<br>
<br>
</span>Maybe with my example from above it might be easier to debug it.<br>
<br>
><br>
> -Iavor<br>
<br>
Thanks,<br>
<br>
Gabor<br>
<div><div><br>
><br>
><br>
><br>
> On Thu, Apr 23, 2015 at 7:04 AM, Gabor Greif <<a href="mailto:ggreif@gmail.com" target="_blank">ggreif@gmail.com</a>> wrote:<br>
><br>
>> 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,<br>
>> unfortunately)<br>
>><br>
>> {{{<br>
>> data OTU (p :: Nat) (o :: Nat) = OTU { ...fields... } deriving (Show,<br>
>> 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<br>
>> 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>
>><br>
><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>