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 <[email protected]> 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 <[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
