Type family with dodgy binding site leads to Core Lint error

The following program produces a Core Lint error on GHC 8.0 through HEAD:

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

import Data.Kind

type family ConstType (a :: Type) :: Type where
  ConstType _ = Type

type family F (x :: ConstType a) :: Type where
  F (x :: ConstType a) = a

f :: F Int
f = let x = x in x

$ /opt/ghc/8.6.5/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    In the expression: x_aVX @ a1_aVT
    @ a1_aVT is out of scope
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)

f :: forall a. F (Int |> Sym (D:R:ConstType[0] <a>_N))
[LclIdX]
f = \ (@ a_a17q) ->
      letrec {
        x_aVX :: forall t. t
        [LclId]
        x_aVX
          = \ (@ t_a17t) ->
              letrec {
                x_a17u :: t_a17t
                [LclId]
                x_a17u = x_a17u; } in
              x_a17u; } in
      (x_aVX @ a1_aVT)
      `cast` (Sub (Sym (D:R:F[0] <a1_aVT>_N <a_a17q>_N <Int>_N))
              :: a1_aVT
                 ~R# F (Int |> Sym (D:R:ConstType[0] <a1_aVT>_N) ; (D:R:ConstType[0]
                                                                        <a1_aVT>_N ; Sym (D:R:ConstType[0]
                                                                                              <a_a17q>_N))))
end Rec }

*** End of Offense ***


<no location info>: error: 
Compilation had errors

This is likely due to the way F is defined, since F (x :: ConstType a) = a expands to F (x :: Type) = a, which is ill scoped.

Note that GHC is smart enough to catch this if ConstType is defined as a type synonym. That is to say, GHC will simply error if you instead try feeding it this program:

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

import Data.Kind

type ConstType (a :: Type) = Type

type family F (x :: ConstType a) :: Type where
  F (x :: ConstType a) = a

f :: F Int
f = let x = x in x

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

Bug.hs:10:3: error:
    • Family instance purports to bind type variable ‘a1’
        but the real LHS (expanding synonyms) is: F x = ...
    • In the equations for closed type family ‘F’
      In the type family declaration for ‘F’
   |
10 |   F (x :: ConstType a) = a
   |   ^^^^^^^^^^^^^^^^^^^^^^^^