GHC introduces kind equality without TypeInType

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@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

Trac metadata

Trac field	Value
Version	8.0.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture