[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:  new
           Priority:  high           |         Milestone:  8.4.1
          Component:  Compiler       |           Version:  8.4.1-alpha1
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 This program:

 {{{#!hs
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# OPTIONS_GHC -ddump-deriv #-}
 module Bug where

 import Data.Coerce
 import Data.Proxy

 class C a b where
   c :: Proxy (x :: a) -> b

 newtype I a = MkI a

 instance C x a => C x (Bug.I a) where
   c = coerce @(forall (z :: x). Proxy z -> a)
              @(forall (z :: x). Proxy z -> I a)
              c
 }}}

 is rightfully rejected by GHC 8.2.2:

 {{{
 $ /opt/ghc/8.2.2/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:20:16: error:
     Unexpected kind variables Perhaps you intended to use PolyKinds
     In a type argument
    |
 20 |   c = coerce @(forall (z :: x). Proxy z -> a)
    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 Bug.hs:21:16: error:
     Unexpected kind variables Perhaps you intended to use PolyKinds
     In a type argument
    |
 21 |              @(forall (z :: x). Proxy z -> I a)
    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 But GHC 8.4.1-alpha2 actually //accepts// this program!

 {{{
 $ /opt/ghc/8.4.1/bin/ghci Bug.hs
 GHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 Ok, one module loaded.
 }}}

 This is almost certainly bogus.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14710>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler