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.
```haskell
{-# 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.
issue