[GHC] #15862: Typeable panic with promoted rank-2 kind (initDs)
#15862: Typeable panic with promoted rank-2 kind (initDs) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: Typeable | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following program panics on GHC 8.2 and later: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} module Bug where import Type.Reflection newtype Foo = MkFoo (forall a. a) foo :: TypeRep MkFoo foo = typeRep @MkFoo }}} {{{ $ /opt/ghc/8.6.1/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) GHC error in desugarer lookup in Bug: attempting to use module ‘main:Bug’ (Bug.hs) which is not loaded ghc: panic! (the 'impossible' happened) (GHC version 8.6.1 for x86_64-unknown-linux): initDs }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15862 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15862: Typeable panic with promoted rank-2 kind (initDs) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I was surprised to see this, so I tried {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} module Bug where import Type.Reflection newtype Foo = MkFoo (forall a. a) foo :: TypeRep MkFoo foo = undefined }}} instead. And that program is accepted... but it really shouldn't be. The problem is that the type of `foo` is `TypeRep @((forall a. a) -> Foo) 'MkFoo`, which involves an impredicative instantiation of the kind variable of `TypeRep`. This is not currently allowed. I would fix the missing impredicativity check before worrying about `initDs`. However, with #12045, I suppose we'll want to start allowing impredicative kind instantiations... even then, we won't be able to deal with type representations involving foralls (at least, not without another rewrite of `TypeRep`). So, I suppose tackling the `initDs` bug directly is also a step forward. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15862#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15862: Typeable panic with promoted rank-2 kind (initDs) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:1 goldfire]:
I would fix the missing impredicativity check before worrying about `initDs`.
In case you didn't notice this, I deliberately enabled `ImpredicativeTypes` in this program :) I, too, am surprised that this panics, though. Especially since `typeIsTypeable` appears to [http://git.haskell.org/ghc.git/blob/1a3b9bd0b674ad16a41b942c738b8f34564bcd8d... already answer "no"] when a type contains a nested `forall` like this: {{{#!hs typeIsTypeable (ForAllTy{}) = False }}} It's possible that something else is going wrong, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15862#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15862: Typeable panic with promoted rank-2 kind (initDs) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: Typeable, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: Typeable => Typeable, ImpredicativeTypes -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15862#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15862: Panic with promoted types that Typeable doesn't support -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: Typeable, ImpredicativeTypes => Typeable Comment: It turns out that this problem is more general than just this one example (which happens to use `ImpredicativeTypes`). Here is //another// program which triggers the same panic: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Type.Reflection type family F a type instance F Int = Type data Bar = forall (a :: F Int). MkBar a bar :: TypeRep (MkBar True) bar = typeRep }}} This time, the culprit is likely the fact that `MkBar True` contains a cast/coercion somewhere, which is another thing that `Typeable` doesn't support. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15862#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15862: Panic with promoted types that Typeable doesn't support -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Unboxed sums, too: {{{#!hs {-# LANGUAGE TypeInType #-} {-# LANGUAGE UnboxedSums #-} module Bug where import Type.Reflection data Quux = MkQuux (# Bool | Int #) bar :: TypeRep MkQuux bar = typeRep }}} {{{ $ /opt/ghc/8.6.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) GHC error in desugarer lookup in Bug: attempting to use module ‘main:Bug’ (Bug.hs) which is not loaded ghc: panic! (the 'impossible' happened) (GHC version 8.6.2 for x86_64-unknown-linux): initDs }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15862#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15862: Panic with promoted types that Typeable doesn't support -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): This also fails {{{#!hs data Bar where MkBar :: forall (a :: F Int). a -> Bar }}} but this succeeds {{{#!hs data Bar where MkBar :: (a :: F Int) -> Bar }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15862#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15862: Panic with promoted types that Typeable doesn't support -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: Typeable, | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: Typeable => Typeable, TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15862#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC