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