[GHC] #10348: HEAD: `KnownNat` does not imply `Typeable` any more
GHC
ghc-devs at haskell.org
Thu Apr 23 17:17:04 UTC 2015
#10348: HEAD: `KnownNat` does not imply `Typeable` any more
-------------------------------------+-------------------------------------
Reporter: heisenbug | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.11
(Type checker) | Operating System: Unknown/Multiple
Keywords: | Type of failure: GHC rejects
Architecture: | valid program
Unknown/Multiple | Blocked By:
Test Case: | Related Tickets:
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
As Iavor confirmed (https://mail.haskell.org/pipermail/ghc-
devs/2015-April/008885.html) there is a regression on HEAD relative to
`ghc-7.11.20150215`. Here is a reproduction snippet:
{{{#!hs
{-# 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 I now see more constraints
{{{
*Main> :t T Hey
T Hey :: (Typeable n, KnownNat n) => T (Foo n)
}}}
OTOH ghci-7.11.20150215 only wanted `KnownNat`:
{{{
*Main> :t T Hey
T Hey :: KnownNat n => T (Foo n)
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10348>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list