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 <[email protected]> wrote: > On 4/23/15, Iavor Diatchki <[email protected]> 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 <[email protected]> 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... > >> > > >
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
