Backpack accepts invalid impredicativity in implementation of abstract data

When checking that type T = rhs is a valid implementation of an abstract data declaration data T, backpack fails to check whether rhs contains any nested foralls, which means it accepts e.g.

{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ImpredicativeTypes #-}

unit p where
  module M where
    import Data.Kind

    type C :: Type -> Constraint
    class C a where
      type family F a :: Type

unit q where
  dependency p
  signature H where
    data T
  module N where
    import M ( C(F) )
    import H ( T )

    instance C T where
      type F T = T

unit r where
  dependency p
  module H where
    import Data.Kind

    type S :: Type -> Type
    data S a = MkS

    type T = S (forall (a :: Type). a -> a)

unit s where
  dependency p
  dependency r
  dependency q[H=r:H]

There should be a check that mirrors the check that there are no type family applications in the RHS.