GHC internal error with dubious TLKS scoping

Here's a suspicious program:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

type T :: forall a. a -> Maybe a
type T = Just @a :: forall a. a -> Maybe a

GHC reacts by throwing an internal error:

[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:9:16: error:
    • GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [rpQ :-> ATcTyCon T :: forall a.
                                                     a -> Maybe a]
    • In the first argument of ‘Just’, namely ‘a’
      In the type ‘Just @a :: forall a. a -> Maybe a’
      In the type declaration for ‘T’
  |
9 | type T = Just @a :: forall a. a -> Maybe a
  |                ^

I think this program should ultimately be rejected. This program was inspired by various examples from #16635 (closed).