#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, this problem dates even further back than I imagined. Another problematic aspect of this code is that the definition of `C` alone is accepted: {{{#!hs {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# OPTIONS_GHC -ddump-deriv #-} module Bug where import Data.Coerce import Data.Proxy class C a b where c :: Proxy (x :: a) -> b }}} In fact, even GHC 8.0 accepts this! This appears to be a behavioral change from GHC 7.10.3, where this code is rejected: {{{ $ /opt/ghc/7.10.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:10:20: Type variable ‘a’ used in a kind In the kind ‘a’ In the type ‘Proxy (x :: a) -> b’ In the class declaration for ‘C’ }}} (My guess is that commit 6746549772c5cc0ac66c0fce562f297f4d4b80a2, `Add kind equalities to GHC.`, is responsible for this.) Really, defining `C` should require `PolyKinds` (or perhaps even `TypeInType`), as the type variable `a` is also used as a kind variable within the type of `c`. You don't even need type classes for this issue to surface. Here is another problematic definition that uses plain old functions: {{{#!hs {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} module Bug where import Data.Proxy f :: forall a. a -> a f x = const x g where g :: Proxy (x :: a) g = Proxy }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14710#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#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 simonpj): Excellent diagnosis. This can't be too hard to fix, but I'm out of cycles. Happy to advise. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14710#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#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

#14710: GHC 8.4.1-alpha allows the use of kind polymorphism without PolyKinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch 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): Phab:D4554 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D4554 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14710#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#14710: GHC 8.4.1-alpha allows the use of kind polymorphism without PolyKinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch 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): Phab:D4554 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ryan Scott <ryan.gl.scott@…>): In [changeset:"447d1264abcd52bdd98267d109bfc1ff1c96ad27/ghc" 447d1264/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="447d1264abcd52bdd98267d109bfc1ff1c96ad27" Fix #14710 with more validity checks during renaming Summary: #14710 revealed two unfortunate regressions related to kind polymorphism that had crept in in recent GHC releases: 1. While GHC was able to catch illegal uses of kind polymorphism (i.e., if `PolyKinds` wasn't enabled) in limited situations, it wasn't able to catch kind polymorphism of the following form: ```lang=haskell f :: forall a. a -> a f x = const x g where g :: Proxy (x :: a) g = Proxy ``` Note that the variable `a` is being used as a kind variable in the type signature of `g`, but GHC happily accepts it, even without the use of `PolyKinds`. 2. If you have `PolyKinds` (but not `TypeInType`) enabled, then GHC incorrectly accepts the following definition: ```lang=haskell f :: forall k (a :: k). Proxy a f = Proxy ``` Even though `k` is explicitly bound and then later used as a kind variable within the same telescope. This patch fixes these two bugs as follows: 1. Whenever we rename any `HsTyVar`, we check if the following three criteria are met: (a) It's a type variable (b) It's used at the kind level (c) `PolyKinds` is not enabled If so, then we have found an illegal use of kind polymorphism, so throw an error. This check replaces the `checkBadKindBndrs` function, which could only catch illegal uses of kind polymorphism in very limited situations (when the bad kind variable happened to be implicitly quantified in the same type signature). 2. In `extract_hs_tv_bndrs`, we must error if `TypeInType` is not enabled and either of the following criteria are met: (a) An explicitly bound type variable is used in kind position in the body of a `forall` type. (b) An explicitly bound type variable is used in kind position in the kind of a bound type variable in a `forall` type. `extract_hs_tv_bndrs` was checking (a), but not (b). Easily fixed. Test Plan: ./validate Reviewers: goldfire, simonpj, bgamari, hvr Reviewed By: simonpj Subscribers: thomie, carter GHC Trac Issues: #14710 Differential Revision: https://phabricator.haskell.org/D4554 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14710#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler