[GHC] #16247: GHC 8.6 Core Lint regression (Kind application error)

[GHC]

#16247: GHC 8.6 Core Lint regression (Kind application error)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.10.1
          Component:  Compiler       |           Version:  8.6.3
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following program produces a Core Lint error on GHC 8.6.3 and HEAD:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind

 data SameKind :: forall k. k -> k -> Type
 data Foo :: forall a k (b :: k). SameKind a b -> Type where
   MkFoo :: Foo sameKind
 }}}

 {{{
 $ /opt/ghc/8.6.3/bin/ghc Bug.hs -dcore-lint
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 *** Core Lint errors : in result of CorePrep ***
 <no location info>: warning:
     In the type ‘forall k (a :: k) k (b :: k) (sameKind :: SameKind
                                                              a b).
                  Foo sameKind’
     Kind application error in type ‘SameKind a_aWE b_aWG’
       Function kind = forall k. k -> k -> *
       Arg kinds = [(k_aWF, *), (a_aWE, k_aWD), (b_aWG, k_aWF)]
     Fun: k_aWF
          (a_aWE, k_aWD)
 *** Offending Program ***

 <elided>

 MkFoo
   :: forall k (a :: k) k (b :: k) (sameKind :: SameKind a b).
      Foo sameKind
 }}}

 (Confusingly, the type of `MkFoo` is rendered as `forall k (a :: k) k (b
 :: k) (sameKind :: SameKind a b). Foo sameKind` in that `-dcore-lint`
 error, but I think it really should be `forall k1 (a :: k1) k2 (b :: k2)
 (sameKind :: SameKind a b). Foo sameKind`.)

 On GHC 8.4.4 and earlier, this simply produces an error message:

 {{{
 $ /opt/ghc/8.4.4/bin/ghc Bug.hs -dcore-lint
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:9:13: error:
     • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
     • In the kind ‘forall a k (b :: k). SameKind a b -> Type’
   |
 9 | data Foo :: forall a k (b :: k). SameKind a b -> Type where
   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

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