Re: deriving Typeable and Nat kinds

Could you please make a ticket for this, so that we have a reference and it does not get lost? On Thu, Apr 23, 2015 at 9:59 AM, Iavor Diatchki wrote:

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`:

instance KnownNat n => Typeable (n :: Nat) where ...

When I updated the `Typeable` solver, I forgot about that special case---I'll have a go at a fix.

-Iavor

On Thu, Apr 23, 2015 at 8:37 AM, Gabor Greif wrote:

...

On 4/23/15, Iavor Diatchki wrote:

...

Hello,

Hi Iavor,

...

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.

No need to apologize, I chose this way to be able to intervene fast when something breaks :-) The old behaviour might have been unsafe, though I cannot see why.

...

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.

Here is a small example where an additional constraint surfaces:

------------------------------------------------------------------------------ {-# LANGUAGE AutoDeriveTypeable, GADTs, DataKinds, KindSignatures, StandaloneDeriving #-}

import GHC.TypeLits import Data.Typeable

data Foo (n :: Nat) where Hey :: KnownNat n => Foo n

deriving instance Show (Foo n)

data T t where T :: (Show t, Typeable t) => t -> T t

deriving instance Show (T n)

{-

------------------- WITH ghci-7.11.20150407 (and newer) *Main> :t T Hey T Hey :: (Typeable n, KnownNat n) => T (Foo n)

------------------- WITH ghci-7.11.20150215 (old) *Main> :t T Hey T Hey :: KnownNat n => T (Foo n)

-}

------------------------------------------------------------------------------

...

To answer your question about `KnownNat p`---there is no relation

...

it and `Typeable`. You may think if a `KnownNat x` constraint as just

between 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

Yes, this relation I was alluding to.

...

that if you have `KnownNat p`, then you can get `Typeable p`, but this has never worked previosly, so perhaps there is another issue.

Maybe with my example from above it might be easier to debug it.

...

-Iavor

Thanks,

Gabor

...

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