Levity polymorphic GADT requires extra type signatures

This does not compile:

data Foo s (a :: TYPE k) where
  FooC :: Foo s Int#

However, this does:

data Foo (s :: Type) (a :: TYPE k) where
  FooC :: Foo s Int#

This also works:

data Foo (s :: j) (a :: TYPE k) where
  FooC :: Foo s Int#

These are all of the language pragmas I have enabled:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE UnboxedSums #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

This is pretty easy to work around, but I think it's an incorrect behavior.

Trac metadata

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