deriving Typeable and Nat kinds

[Iavor Diatchki]

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