deriving Typeable and Nat kinds

[Gabor Greif]

Here you go: https://ghc.haskell.org/trac/ghc/ticket/10348

Thanks for looking into this!

Cheers,

    Gabor

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