GHC HEAD regression involving type families in kinds

In GHC 8.2.1, this file typechecks:

{-# 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 (closed).)

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
   |                           ^

Trac metadata

Trac field	Value
Version	8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture