GHC HEAD regression: cannot instantiate higher-rank kind

The following program typechecks on GHC 8.2.2 and 8.4.2:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Void

infixl 4 :==
-- | Heterogeneous Leibnizian equality.
newtype (a :: j) :== (b :: k)
  = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }

newtype Coerce a = Coerce { uncoerce :: Starify a }
type family Starify (a :: k) :: Type where
  Starify (a :: Type) = a
  Starify _           = Void

coerce :: a :== b -> a -> b
coerce f = uncoerce . hsubst f . Coerce

But GHC HEAD rejects it:

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

Bug.hs:21:34: error:
    • Kind mismatch: cannot unify (c0 :: forall i. i -> *) with:
        Coerce :: forall k. k -> *
      Their kinds differ.
      Expected type: a -> c0 * a
        Actual type: Starify a -> Coerce a
    • In the second argument of ‘(.)’, namely ‘Coerce’
      In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’
      In the expression: uncoerce . hsubst f . Coerce
   |
21 | coerce f = uncoerce . hsubst f . Coerce
   |                                  ^^^^^^

Trac metadata

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