#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