Data family instance with visible forall in return kind is incorrectly rejected

GHC 8.10 and later reject this program:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind

data family   Hm :: forall a -> a -> Type
data instance Hm :: forall a -> a -> Type

$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:11:1: error:
    • Expecting one more argument to ‘Hm’
      Expected kind ‘a -> *’, but ‘Hm’ has kind ‘forall a -> a -> *’
    • In the data instance declaration for ‘Hm’
   |
11 | data instance Hm :: forall a -> a -> Type
   | ^^^^^^^^^^^^^^^^

I claim that this should be accepted, however. This is especially strange since GHC does accept this program if Hm is changed from a data family to a normal data type:

data Hm :: forall a -> a -> Type

The culprit is this code in tcDataFamInstHeader:

    -- See Note [Result kind signature for a data family instance]
    tc_kind_sig (Just hs_kind)
      = do { sig_kind <- tcLHsKindSig data_ctxt hs_kind
           ; let (tvs, inner_kind) = tcSplitForAllTys sig_kind
           ; lvl <- getTcLevel
           ; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
             -- Perhaps surprisingly, we don't need the skolemised tvs themselves
           ; return (substTy subst inner_kind) }

The use of tcSplitForAllTys above incorrectly splits off the forall a in forall a -> a -> Type, but really, we should only be splitting off invisible foralls in the result kind. Changing tcSplitForAllTys to tcSplitForAllTysInvis would fix this issue.

In fact, there are a number of places where we ought to use tcSplitForAllTysInvis instead of tcSplitForAllTys. This was originally noticed in !4417 (comment 311329), but this bug can be understood independently of !4417 (closed).