[GHC] #11520: GHC falls into a hole if given incorrect kind signature (was: GHC falls into a hole)

[GHC]

#11520: GHC falls into a hole if given incorrect kind signature
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  8.0.1-rc1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by bgamari:

@@ -1,1 +1,2 @@
- This non-sense,
+ If one provides an incorrect kind signature GHC throws up. For instance,
+ this non-sense,
@@ -11,2 +12,0 @@
- data TyCon (a :: k) = TyCon
-
@@ -14,1 +13,1 @@
-     TypeCon :: forall (a :: k). TyCon a -> TypeRep k -> TypeRep a
+     TypeCon :: forall (a :: k). String -> TypeRep k -> TypeRep a
@@ -25,3 +24,1 @@
- composeTyCon :: TyCon Compose
- composeTyCon = TyCon Fingerprint "Compose"
-
+ -- Note how the kind signature on g is incorrect
@@ -30,2 +27,1 @@
-     typeRep = TypeApp (TypeApp (TypeCon composeTyCon typeRep) typeRep)
- typeRep
+     typeRep = undefined
@@ -33,4 +29,0 @@
- instance (Typeable f, Typeable g, Typeable a) => Typeable (Compose f g a)
- where
-     typeRep = TypeApp (TypeApp (TypeApp (TypeCon composeTyCon typeRep)
- typeRep) typeRep) typeRep

New description:

 If one provides an incorrect kind signature GHC throws up. For instance,
 this non-sense,

 {{{#!hs
 {-# LANGUAGE RankNTypes, PolyKinds, TypeInType, GADTs,
 UndecidableSuperClasses #-}

 module Play where

 import GHC.Types hiding (TyCon)

 data TypeRep (a :: k) where
     TypeCon :: forall (a :: k). String -> TypeRep k -> TypeRep a
     TypeApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
                TypeRep a
             -> TypeRep b
             -> TypeRep (a b)

 class Typeable k => Typeable (a :: k) where
     typeRep :: TypeRep a

 data Compose (f :: k1 -> *) (g :: k2 -> k1) (a :: k2) = Compose (f (g a))

 -- Note how the kind signature on g is incorrect
 instance (Typeable f, Typeable (g :: k), Typeable k) => Typeable (Compose
 f g) where
     typeRep = undefined

 }}}
 fails with
 {{{
 λ> :load Bug.hs
 [1 of 1] Compiling Play             ( Bug.hs, interpreted )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.1.20160122 for x86_64-unknown-linux):
         fvProv falls into a hole {abet}

 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 }}}

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11520#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler