[GHC] #15862: Typeable panic with promoted rank-2 kind (initDs)

[GHC]

#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