[GHC] #14441: GHC HEAD regression involving type families in kinds

[GHC]

#14441: GHC HEAD regression involving type families in kinds
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.4.1
          Component:  Compiler       |           Version:  8.3
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypeFamilies                       |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #13790
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 In GHC 8.2.1, this file typechecks:

 {{{#!hs
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind

 type family Demote (k :: Type) :: Type
 type family DemoteX (a :: k) :: Demote k

 data Prox (a :: k) = P

 type instance Demote (Prox (a :: k)) = Prox (DemoteX a)
 $(return [])
 type instance DemoteX P = P
 }}}

 (Note that the `$(return [])` line is essential, as it works around
 #13790.)

 However, on GHC HEAD, this now fails:

 {{{
 $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:15:27: error:
     • Expected kind ‘Demote (Prox a0)’, but ‘P’ has kind ‘Prox a1’
     • In the type ‘P’
       In the type instance declaration for ‘DemoteX’
    |
 15 | type instance DemoteX P = P
    |                           ^
 }}}

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