[GHC] #11963: GHC introduces kind equality without TypeInType

[GHC]

#11963: GHC introduces kind equality without TypeInType
-------------------------------------+-------------------------------------
           Reporter:  ezyang         |             Owner:  goldfire
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1-rc2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following program is accepted by GHC 8.0 rc2

 {{{
 {-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
 data Typ k t  where
     Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t
 }}}

 This probably shouldn't be accepted, because this is a circuitous way of
 saying:

 {{{
 {-# LANGUAGE TypeInType #-}
 data Typ k (t :: k) = Typ
 }}}

 which does not work without `TypeInType`. Or perhaps both should be
 accepted without `TypeInType`?

 Printing with explicit kinds makes it clear why the obvious check didn't
 fire:

 {{{
 ezyang at sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds
 GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( B.hs, interpreted )
 Ok, modules loaded: Main.
 *Main> :info Typ
 type role Typ nominal nominal nominal
 data Typ k k1 (t :: k) where
   Typ :: forall k (t :: k).
          (forall (a :: k -> *). a t -> a t) -> Typ k k t
         -- Defined at B.hs:2:1
 }}}

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