[GHC] #14710: GHC 8.4.1-alpha allows the use of kind polymorphism without PolyKinds

[GHC]

#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