deriving Typeable and Nat kinds

[Iavor Diatchki]

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 at 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...
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20150423/756d4828/attachment.html>