#14710: GHC 8.4.1-alpha allows the use of kind polymorphism without PolyKinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.4.1-alpha1 checker) | Resolution: | Keywords: PolyKinds Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Actually, if we decide to require the use of `TypeInType` (and not just `PolyKinds`) for this featurette, then checking binding sites wouldn't be enough. It turns out the GHC currently accepts this program without `TypeInType`: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} module Bug where import Data.Proxy f :: forall k a. Proxy (a :: k) f = Proxy }}} But it seems like it shouldn't, since `k` is being quantified as a type variable but used as a kind variable. For comparison, if you tried this equivalent program: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} module Bug where import Data.Proxy f :: forall k (a :: k). Proxy a f = Proxy }}} Then GHC will bleat about `TypeInType`: {{{ $ ghci Bug.hs GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:7:21: error: Type variable âkâ used in a kind. Did you mean to use TypeInType? the type signature for âfâ | 7 | f :: forall k (a :: k). Proxy a | ^ }}} So, in short: I'm even less sure about where to put this validity check :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14710#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler