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 |