[GHC] #10348: HEAD: `KnownNat` does not imply `Typeable` any more
#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
#10348: HEAD: `KnownNat` does not imply `Typeable` any more -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: diatchki Type: bug | Status: new Priority: highest | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => diatchki * priority: normal => highest * milestone: => 7.12.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10348#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10348: HEAD: `KnownNat` does not imply `Typeable` any more -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: diatchki Type: bug | Status: new Priority: highest | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by heisenbug): Ping. Any chance to fix this, so that I can swim with GHC master again? ''Iavor, if you are buried in other stuff I could look into this myself.'' -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10348#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10348: HEAD: `KnownNat` does not imply `Typeable` any more
-------------------------------------+-------------------------------------
Reporter: heisenbug | Owner: diatchki
Type: bug | Status: new
Priority: highest | Milestone: 7.12.1
Component: Compiler (Type | Version: 7.11
checker) | Keywords:
Resolution: | Architecture:
Operating System: Unknown/Multiple | Unknown/Multiple
Type of failure: GHC rejects | Test Case:
valid program | Blocking:
Blocked By: | Differential Revisions:
Related Tickets: |
-------------------------------------+-------------------------------------
Comment (by Gabor Greif
#10348: HEAD: `KnownNat` does not imply `Typeable` any more
-------------------------------------+-------------------------------------
Reporter: heisenbug | Owner: diatchki
Type: bug | Status: new
Priority: highest | Milestone: 7.12.1
Component: Compiler (Type | Version: 7.11
checker) | Keywords:
Resolution: | Architecture:
Operating System: Unknown/Multiple | Unknown/Multiple
Type of failure: GHC rejects | Test Case:
valid program | Blocking:
Blocked By: | Differential Revisions:
Related Tickets: |
-------------------------------------+-------------------------------------
Comment (by Gabor Greif
#10348: HEAD: `KnownNat` does not imply `Typeable` any more -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: diatchki Type: bug | Status: new Priority: highest | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by heisenbug): I changed the test case thus: {{{ diff --git a/testsuite/tests/typecheck/should_compile/T10348.hs b/testsuite/tests/typecheck/should_compile/T10348.hs index 213079b..14fc085 100644 --- a/testsuite/tests/typecheck/should_compile/T10348.hs +++ b/testsuite/tests/typecheck/should_compile/T10348.hs @@ -15,8 +15,7 @@ data T t where deriving instance Show (T n) -hey :: (Typeable n, KnownNat n) => T (Foo n) --- SHOULD BE: hey :: KnownNat n => T (Foo n) +hey :: KnownNat n => T (Foo n) hey = T Hey ho :: T (Foo 42) }}} Then this code (I just added a panic for visibility) is triggered: {{{ diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 01b0ba1..bf5f237 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -48,6 +48,7 @@ import Pair (Pair(..)) import Unique( hasKey ) import DynFlags import Util +import TypeRep( Type(..) ) {- ********************************************************************** @@ -1852,6 +1853,8 @@ matchTypeableClass clas _k t | Just (f,kt) <- splitAppTy_maybe t = doTyApp f kt | Just _ <- isNumLitTy t = mkSimpEv (EvTypeableTyLit t) | Just _ <- isStrLitTy t = mkSimpEv (EvTypeableTyLit t) + | TyConApp con [] <- _k + , Just tcon <- isPromotedTyCon_maybe con = pprPanic "matchTypeableClass" $ ppr tcon | otherwise = return NoInstance where }}} I guess code must be generated that creates the Typeable hash on the fly (at runtime) by appealing to the KnownNat's method. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10348#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10348: HEAD: `KnownNat` does not imply `Typeable` any more -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: diatchki Type: bug | Status: new Priority: highest | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by simonpj): Iavor says he'll do this over the weekend. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10348#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10348: HEAD: `KnownNat` does not imply `Typeable` any more -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: diatchki Type: bug | Status: new Priority: highest | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by heisenbug): Replying to [comment:6 simonpj]:
Iavor says he'll do this over the weekend.
Simon
Thanks, that sounds good :-) These are presumably part of the future solution: {{{ $ git grep typeLitTypeRep compiler/deSugar/DsBinds.hs: ctr <- dsLookupGlobalId typeLitTypeRepName compiler/prelude/PrelNames.hs: typeLitTypeRepName, compiler/prelude/PrelNames.hs: , typeLitTypeRepName compiler/prelude/PrelNames.hs:typeLitTypeRepName = varQual tYPEABLE_INTERNAL (fsLit "typeLitTypeRep") typeLitTypeRepKey compiler/prelude/PrelNames.hs: , typeLitTypeRepKey compiler/prelude/PrelNames.hs:typeLitTypeRepKey = mkPreludeMiscIdUnique 506 libraries/base/Data/Typeable/Internal.hs: typeLitTypeRep libraries/base/Data/Typeable/Internal.hs:typeLitTypeRep :: String -> TypeRep libraries/base/Data/Typeable/Internal.hs:typeLitTypeRep nm = rep }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10348#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10348: HEAD: `KnownNat` does not imply `Typeable` any more -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: diatchki Type: bug | Status: new Priority: highest | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by diatchki): I pushed a fix this morning, 4854fcea4f73897bbdcdfede382c826da7b64b97. Give it a go and let me know if you find a problems. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10348#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10348: HEAD: `KnownNat` does not imply `Typeable` any more -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: diatchki Type: bug | Status: closed Priority: highest | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: Resolution: fixed | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Changes (by heisenbug): * status: new => closed * resolution: => fixed Comment: Replying to [comment:8 diatchki]:
I pushed a fix this morning, 4854fcea4f73897bbdcdfede382c826da7b64b97. Give it a go and let me know if you find a problems.
Your fix solves my compilation problems, thanks! It will take some days to have my testing done, but I anticipate no problems. I'll close this PR for now, possibly reopening it of some related issues remain. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10348#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10348: HEAD: `KnownNat` does not imply `Typeable` any more
-------------------------------------+-------------------------------------
Reporter: heisenbug | Owner: diatchki
Type: bug | Status: closed
Priority: highest | Milestone: 7.12.1
Component: Compiler (Type | Version: 7.11
checker) | Keywords:
Resolution: fixed | Architecture:
Operating System: Unknown/Multiple | Unknown/Multiple
Type of failure: GHC rejects | Test Case:
valid program | Blocking:
Blocked By: | Differential Revisions:
Related Tickets: |
-------------------------------------+-------------------------------------
Comment (by Gabor Greif
participants (1)
-
GHC