deriving Typeable and Nat kinds

[Gabor Greif]

On 4/23/15, Iavor Diatchki <iavor.diatchki at gmail.com> 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 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

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 <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...
>>
>