Use tcSplitForAllInvisTyVars (not tcSplitForAllTyVars) in more places

The use of `tcSplitForAllTyVars` in `tcDataFamInstHeader` was the immediate
cause of #18939, and replacing it with a new `tcSplitForAllInvisTyVars`
function (which behaves like `tcSplitForAllTyVars` but only splits invisible
type variables) fixes the issue. However, this led me to realize that _most_
uses of `tcSplitForAllTyVars` in GHC really ought to be
`tcSplitForAllInvisTyVars` instead. While I was in town, I opted to replace
most uses of `tcSplitForAllTys` with `tcSplitForAllTysInvis` to reduce the
likelihood of such bugs in the future.

I say "most uses" above since there is one notable place where we _do_ want
to use `tcSplitForAllTyVars`: in `GHC.Tc.Validity.forAllTyErr`, which produces
the "`Illegal polymorphic type`" error message if you try to use a higher-rank
`forall` without having `RankNTypes` enabled. Here, we really do want to split
all `forall`s, not just invisible ones, or we run the risk of giving an
inaccurate error message in the newly added `T18939_Fail` test case.

I debated at some length whether I wanted to name the new function
`tcSplitForAllInvisTyVars` or `tcSplitForAllTyVarsInvisible`, but in the end,
I decided that I liked the former better. For consistency's sake, I opted to
rename the existing `splitPiTysInvisible` and `splitPiTysInvisibleN` functions
to `splitInvisPiTys` and `splitPiTysInvisN`, respectively, so that they use the
same naming convention. As a consequence, this ended up requiring a `haddock`
submodule bump.

Fixes #18939.

15 files changed, 59 insertions, 29 deletions

diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index bf5fe081d8..b983671d11 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -76,7 +76,7 @@ module GHC.Core.Type (
         coAxNthLHS,
         stripCoercionTy,
 
-        splitPiTysInvisible, splitPiTysInvisibleN,
+        splitInvisPiTys, splitInvisPiTysN,
         invisibleTyBndrCount,
         filterOutInvisibleTypes, filterOutInferredTypes,
         partitionInvisibleTypes, partitionInvisibles,
@@ -1559,7 +1559,7 @@ splitForAllTyCoVars ty = split ty ty []
     split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
     split orig_ty _                            tvs = (reverse tvs, orig_ty)
 
--- | Splits the longest initial sequence of ForAllTys' that satisfy
+-- | Splits the longest initial sequence of 'ForAllTy's that satisfy
 -- @argf_pred@, returning the binders transformed by @argf_pred@
 splitSomeForAllTyCoVarBndrs :: (ArgFlag -> Maybe af) -> Type -> ([VarBndr TyCoVar af], Type)
 splitSomeForAllTyCoVarBndrs argf_pred ty = split ty ty []
@@ -1716,12 +1716,12 @@ invisibleTyBndrCount :: Type -> Int
 -- Includes invisible predicate arguments; e.g. for
 --    e.g.  forall {k}. (k ~ *) => k -> k
 -- returns 2 not 1
-invisibleTyBndrCount ty = length (fst (splitPiTysInvisible ty))
+invisibleTyBndrCount ty = length (fst (splitInvisPiTys ty))
 
--- Like splitPiTys, but returns only *invisible* binders, including constraints
--- Stops at the first visible binder
-splitPiTysInvisible :: Type -> ([TyCoBinder], Type)
-splitPiTysInvisible ty = split ty ty []
+-- | Like 'splitPiTys', but returns only *invisible* binders, including constraints.
+-- Stops at the first visible binder.
+splitInvisPiTys :: Type -> ([TyCoBinder], Type)
+splitInvisPiTys ty = split ty ty []
    where
     split _ (ForAllTy b res) bs
       | Bndr _ vis <- b
@@ -1732,11 +1732,11 @@ splitPiTysInvisible ty = split ty ty []
       | Just ty' <- coreView ty  = split orig_ty ty' bs
     split orig_ty _          bs  = (reverse bs, orig_ty)
 
-splitPiTysInvisibleN :: Int -> Type -> ([TyCoBinder], Type)
--- Same as splitPiTysInvisible, but stop when
---   - you have found 'n' TyCoBinders,
+splitInvisPiTysN :: Int -> Type -> ([TyCoBinder], Type)
+-- ^ Same as 'splitInvisPiTys', but stop when
+--   - you have found @n@ 'TyCoBinder's,
 --   - or you run out of invisible binders
-splitPiTysInvisibleN n ty = split n ty ty []
+splitInvisPiTysN n ty = split n ty ty []
    where
     split n orig_ty ty bs
       | n == 0                  = (reverse bs, orig_ty)
diff --git a/compiler/GHC/HsToCore/Foreign/Decl.hs b/compiler/GHC/HsToCore/Foreign/Decl.hs
index c7907682ae..cae1d3f115 100644
--- a/compiler/GHC/HsToCore/Foreign/Decl.hs
+++ b/compiler/GHC/HsToCore/Foreign/Decl.hs
@@ -316,7 +316,7 @@ dsPrimCall :: Id -> Coercion -> ForeignCall
 dsPrimCall fn_id co fcall = do
     let
         ty                   = coercionLKind co
-        (tvs, fun_ty)        = tcSplitForAllTyVars ty
+        (tvs, fun_ty)        = tcSplitForAllInvisTyVars ty
         (arg_tys, io_res_ty) = tcSplitFunTys fun_ty
 
     args <- newSysLocalsDs arg_tys  -- no FFI levity-polymorphism
@@ -489,7 +489,7 @@ dsFExportDynamic id co0 cconv = do
 
  where
   ty                       = coercionLKind co0
-  (tvs,sans_foralls)       = tcSplitForAllTyVars ty
+  (tvs,sans_foralls)       = tcSplitForAllInvisTyVars ty
   ([Scaled arg_mult arg_ty], fn_res_ty)    = tcSplitFunTys sans_foralls
   Just (io_tc, res_ty)     = tcSplitIOType_maybe fn_res_ty
         -- Must have an IO type; hence Just
diff --git a/compiler/GHC/Runtime/Heap/Inspect.hs b/compiler/GHC/Runtime/Heap/Inspect.hs
index ff2bb50fa9..1b912339e5 100644
--- a/compiler/GHC/Runtime/Heap/Inspect.hs
+++ b/compiler/GHC/Runtime/Heap/Inspect.hs
@@ -1389,4 +1389,4 @@ quantifyType ty = ( filter isTyVar $
                     tyCoVarsOfTypeWellScoped rho
                   , rho)
   where
-    (_tvs, rho) = tcSplitForAllTyVars ty
+    (_tvs, rho) = tcSplitForAllInvisTyVars ty
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 5e5ffd41ad..6e42b9e21e 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2568,13 +2568,13 @@ kcCheckDeclHeader_sig kisig name flav
     split_invis :: Kind -> Maybe Kind -> ([TyCoBinder], Kind)
     split_invis sig_ki Nothing =
       -- instantiate all invisible binders
-      splitPiTysInvisible sig_ki
+      splitInvisPiTys sig_ki
     split_invis sig_ki (Just res_ki) =
       -- subtraction a la checkExpectedKind
       let n_res_invis_bndrs = invisibleTyBndrCount res_ki
           n_sig_invis_bndrs = invisibleTyBndrCount sig_ki
           n_inst = n_sig_invis_bndrs - n_res_invis_bndrs
-      in splitPiTysInvisibleN n_inst sig_ki
+      in splitInvisPiTysN n_inst sig_ki
 
 -- A quantifier from a kind signature zipped with a user-written binder for it.
 data ZippedBinder =
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 5ff7308f80..e3e1b7aa16 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -950,7 +950,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
     tc_kind_sig (Just hs_kind)
       = do { sig_kind <- tcLHsKindSig data_ctxt hs_kind
            ; lvl <- getTcLevel
-           ; let (tvs, inner_kind) = tcSplitForAllTyVars sig_kind
+           ; let (tvs, inner_kind) = tcSplitForAllInvisTyVars sig_kind
            ; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
              -- Perhaps surprisingly, we don't need the skolemised tvs themselves
            ; return (substTy subst inner_kind) }
diff --git a/compiler/GHC/Tc/Utils/Backpack.hs b/compiler/GHC/Tc/Utils/Backpack.hs
index de114c3817..6214434fce 100644
--- a/compiler/GHC/Tc/Utils/Backpack.hs
+++ b/compiler/GHC/Tc/Utils/Backpack.hs
@@ -223,8 +223,8 @@ check_inst sig_inst = do
         skol_info = InstSkol
         -- Based off of tcSplitDFunTy
         (tvs, theta, pred) =
-           case tcSplitForAllTyVars ty of { (tvs, rho)    ->
-           case splitFunTys rho        of { (theta, pred) ->
+           case tcSplitForAllInvisTyVars ty of { (tvs, rho)    ->
+           case splitFunTys rho             of { (theta, pred) ->
            (tvs, theta, pred) }}
         origin = InstProvidedOrigin (tcg_semantic_mod tcg_env) sig_inst
     (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index 9bb0675f6c..27d01a5c4d 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -464,7 +464,7 @@ tcInstType inst_tyvars id
              subst'  = extendTCvInScopeSet subst (tyCoVarsOfType rho)
        ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
   where
-    (tyvars, rho) = tcSplitForAllTyVars (idType id)
+    (tyvars, rho) = tcSplitForAllInvisTyVars (idType id)
     (theta, tau)  = tcSplitPhiTy rho
 
 tcInstTypeBndrs :: Id -> TcM ([(Name, InvisTVBinder)], TcThetaType, TcType)
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index f355a016ae..c408ffb54c 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -60,7 +60,7 @@ module GHC.Tc.Utils.TcType (
   -- These are important because they do not look through newtypes
   getTyVar,
   tcSplitForAllTyVarBinder_maybe,
-  tcSplitForAllTyVars, tcSplitSomeForAllTyVars,
+  tcSplitForAllTyVars, tcSplitForAllInvisTyVars, tcSplitSomeForAllTyVars,
   tcSplitForAllReqTVBinders, tcSplitForAllInvisTVBinders,
   tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllTyVarBinders,
   tcSplitPhiTy, tcSplitPredFunTy_maybe,
@@ -1223,12 +1223,17 @@ tcSplitForAllTyVarBinder_maybe (ForAllTy tv ty) = ASSERT( isTyVarBinder tv ) Jus
 tcSplitForAllTyVarBinder_maybe _                = Nothing
 
 -- | Like 'tcSplitPiTys', but splits off only named binders,
--- returning just the tycovars.
+-- returning just the tyvars.
 tcSplitForAllTyVars :: Type -> ([TyVar], Type)
 tcSplitForAllTyVars ty
   = ASSERT( all isTyVar (fst sty) ) sty
   where sty = splitForAllTyCoVars ty
 
+-- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Invisible'
+-- type variable binders.
+tcSplitForAllInvisTyVars :: Type -> ([TyVar], Type)
+tcSplitForAllInvisTyVars ty = tcSplitSomeForAllTyVars isInvisibleArgFlag ty
+
 -- | Like 'tcSplitForAllTyVars', but only splits a 'ForAllTy' if @argf_pred argf@
 -- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and
 -- @argf_pred@ is a predicate over visibilities provided as an argument to this
@@ -1284,9 +1289,11 @@ tcSplitPhiTy ty
           Just (pred, ty) -> split ty (pred:ts)
           Nothing         -> (reverse ts, ty)
 
--- | Split a sigma type into its parts.
+-- | Split a sigma type into its parts. This only splits /invisible/ type
+-- variable binders, as these are the only forms of binder that the typechecker
+-- will implicitly instantiate.
 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
-tcSplitSigmaTy ty = case tcSplitForAllTyVars ty of
+tcSplitSigmaTy ty = case tcSplitForAllInvisTyVars ty of
                         (tvs, rho) -> case tcSplitPhiTy rho of
                                         (theta, tau) -> (tvs, theta, tau)
 
@@ -1469,9 +1476,9 @@ tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
 -- the latter specifically stops at PredTy arguments,
 -- and we don't want to do that here
 tcSplitDFunTy ty
-  = case tcSplitForAllTyVars ty of { (tvs, rho)    ->
-    case splitFunTys rho        of { (theta, tau)  ->
-    case tcSplitDFunHead tau    of { (clas, tys)   ->
+  = case tcSplitForAllInvisTyVars ty of { (tvs, rho)    ->
+    case splitFunTys rho             of { (theta, tau)  ->
+    case tcSplitDFunHead tau         of { (clas, tys)   ->
     (tvs, map scaledThing theta, clas, tys) }}}
 
 tcSplitDFunHead :: Type -> (Class, [Type])
@@ -1489,7 +1496,7 @@ tcSplitMethodTy :: Type -> ([TyVar], PredType, Type)
 -- tcSplitMethodTy just peels off the outer forall and
 -- that first predicate
 tcSplitMethodTy ty
-  | (sel_tyvars,sel_rho) <- tcSplitForAllTyVars ty
+  | (sel_tyvars,sel_rho) <- tcSplitForAllInvisTyVars ty
   , Just (first_pred, local_meth_ty) <- tcSplitPredFunTy_maybe sel_rho
   = (sel_tyvars, first_pred, local_meth_ty)
   | otherwise
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 87be216d9b..6f290cb7ab 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -924,7 +924,7 @@ forAllTyErr env rank ty
      , vcat [ hang herald 2 (ppr_tidy env ty)
             , suggestion ] )
   where
-    (tvs, _theta, _tau) = tcSplitSigmaTy ty
+    (tvs, _rho) = tcSplitForAllTyVars ty
     herald | null tvs  = text "Illegal qualified type:"
            | otherwise = text "Illegal polymorphic type:"
     suggestion = case rank of
diff --git a/testsuite/tests/typecheck/should_compile/T18939_Compile.hs b/testsuite/tests/typecheck/should_compile/T18939_Compile.hs
new file mode 100644
index 0000000000..8c2123f111
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18939_Compile.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+module T18939_Compile where
+
+import Data.Kind
+
+data family   Hm :: forall a -> a -> Type
+data instance Hm :: forall a -> a -> Type
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 263ff97ba1..4482e3fdc4 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -726,6 +726,7 @@ test('T18323', normal, compile, [''])
 test('T18585', normal, compile, [''])
 test('T18831', normal, compile, [''])
 test('T18920', normal, compile, [''])
+test('T18939_Compile', normal, compile, [''])
 test('T15942', normal, compile, [''])
 test('ClassDefaultInHsBoot', [extra_files(['ClassDefaultInHsBootA1.hs','ClassDefaultInHsBootA2.hs','ClassDefaultInHsBootA2.hs-boot','ClassDefaultInHsBootA3.hs'])], multimod_compile, ['ClassDefaultInHsBoot', '-v0'])
 test('T17186', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T18939_Fail.hs b/testsuite/tests/typecheck/should_fail/T18939_Fail.hs
new file mode 100644
index 0000000000..c2faade865
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18939_Fail.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE PolyKinds #-}
+module T18939_Fail where
+
+data F (f :: forall a -> a)
diff --git a/testsuite/tests/typecheck/should_fail/T18939_Fail.stderr b/testsuite/tests/typecheck/should_fail/T18939_Fail.stderr
new file mode 100644
index 0000000000..2cdbab4bb3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18939_Fail.stderr
@@ -0,0 +1,5 @@
+
+T18939_Fail.hs:5:1: error:
+    • Illegal polymorphic type: forall a -> a
+      Perhaps you intended to use RankNTypes
+    • In the data type declaration for ‘F’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 1a260c5dc4..5ce09273a2 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -583,6 +583,7 @@ test('T18714', normal, compile_fail, [''])
 test('T18723a', normal, compile_fail, [''])
 test('T18723b', normal, compile_fail, [''])
 test('T18723c', normal, compile_fail, [''])
+test('T18939_Fail', normal, compile_fail, [''])
 test('too-many', normal, compile_fail, [''])
 test('T18640a', normal, compile_fail, [''])
 test('T18640b', normal, compile_fail, [''])
diff --git a/utils/haddock b/utils/haddock
-Subproject ad9cbad7312a64e6757c32bd9488c55ba4f2fec
+Subproject 4d0498d503bd51b7d7626497580232685a2691a