Fix #16391 by using occCheckExpand in TcValidity

The type-variables-escaping-their-scope-via-kinds check in
`TcValidity` was failing to properly expand type synonyms, which led
to #16391. This is easily fixed by using `occCheckExpand` before
performing the validity check.

Along the way, I refactored this check out into its own function,
and sprinkled references to Notes to better explain all of the moving
parts. Many thanks to @simonpj for the suggestions.

Bumps the haddock submodule.

4 files changed, 88 insertions, 26 deletions

diff --git a/compiler/basicTypes/OccName.hs b/compiler/basicTypes/OccName.hs
index b474c64ca6..cb846f74ec 100644
--- a/compiler/basicTypes/OccName.hs
+++ b/compiler/basicTypes/OccName.hs
@@ -806,7 +806,7 @@ starting the search; and we make sure to update the starting point for "a"
 after we allocate a new one.
 
 
-Node [Tidying multiple names at once]
+Note [Tidying multiple names at once]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Consider
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 90c2b5a4a7..e7ca2e2caa 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -689,20 +689,11 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
         ; check_type (ve{ve_tidy_env = env'}) tau
                 -- Allow foralls to right of arrow
 
-        ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
-                   (forAllEscapeErr env' ty tau_kind)
-        }
+        ; checkEscapingKind env' tvbs' theta tau }
   where
-    (tvbs, phi)  = tcSplitForAllVarBndrs ty
-    (theta, tau) = tcSplitPhiTy phi
-
-    tvs          = binderVars tvbs
-    (env', _)    = tidyVarBndrs env tvs
-
-    tau_kind              = tcTypeKind tau
-    phi_kind | null theta = tau_kind
-             | otherwise  = liftedTypeKind
-        -- If there are any constraints, the kind is *. (#11405)
+    (tvbs, phi)   = tcSplitForAllVarBndrs ty
+    (theta, tau)  = tcSplitPhiTy phi
+    (env', tvbs') = tidyTyCoVarBinders env tvbs
 
 check_type (ve@ValidityEnv{ve_rank = rank}) (FunTy _ arg_ty res_ty)
   = do  { check_type (ve{ve_rank = arg_rank}) arg_ty
@@ -877,13 +868,52 @@ forAllTyErr env rank ty
                    MonoType d     -> d
                    _              -> Outputable.empty -- Polytype is always illegal
 
-forAllEscapeErr :: TidyEnv -> Type -> Kind -> (TidyEnv, SDoc)
-forAllEscapeErr env ty tau_kind
+-- | Reject type variables that would escape their escape through a kind.
+-- See @Note [Type variables escaping through kinds]@.
+checkEscapingKind :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> TcM ()
+checkEscapingKind env tvbs theta tau =
+  case occCheckExpand (binderVars tvbs) phi_kind of
+    -- Ensure that none of the tvs occur in the kind of the forall
+    -- /after/ expanding type synonyms.
+    -- See Note [Phantom type variables in kinds] in Type
+    Nothing -> failWithTcM $ forAllEscapeErr env tvbs theta tau tau_kind
+    Just _  -> pure ()
+  where
+    tau_kind              = tcTypeKind tau
+    phi_kind | null theta = tau_kind
+             | otherwise  = liftedTypeKind
+        -- If there are any constraints, the kind is *. (#11405)
+
+forAllEscapeErr :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> Kind
+                -> (TidyEnv, SDoc)
+forAllEscapeErr env tvbs theta tau tau_kind
   = ( env
-    , hang (vcat [ text "Quantified type's kind mentions quantified type variable"
-                 , text "(skolem escape)" ])
-         2 (vcat [ text "   type:" <+> ppr_tidy env ty
-                 , text "of kind:" <+> ppr_tidy env tau_kind ]) )
+    , vcat [ hang (text "Quantified type's kind mentions quantified type variable")
+                2 (text "type:" <+> quotes (ppr (mkSigmaTy tvbs theta tau)))
+                -- NB: Don't tidy this type since the tvbs were already tidied
+                -- previously, and re-tidying them will make the names of type
+                -- variables different from tau_kind.
+           , hang (text "where the body of the forall has this kind:")
+                2 (quotes (ppr_tidy env tau_kind)) ] )
+
+{-
+Note [Type variables escaping through kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider:
+
+  type family T (r :: RuntimeRep) :: TYPE r
+  foo :: forall r. T r
+
+Something smells funny about the type of `foo`. If you spell out the kind
+explicitly, it becomes clearer from where the smell originates:
+
+  foo :: ((forall r. T r) :: TYPE r)
+
+The type variable `r` appears in the result kind, which escapes the scope of
+its binding site! This is not desirable, so we establish a validity check
+(`checkEscapingKind`) to catch any type variables that might escape through
+kinds in this way.
+-}
 
 ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
 ubxArgTyErr env ty
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 86f72b88f2..9ccfaae31d 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -3909,7 +3909,7 @@ tidyVarBndr tidy_env@(occ_env, subst) var
 
 avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
 -- Seed the occ_env with clashes among the names, see
--- Node [Tidying multiple names at once] in OccName
+-- Note [Tidying multiple names at once] in OccName
 avoidNameClashes tvs (occ_env, subst)
   = (avoidClashesOccEnv occ_env occs, subst)
   where
@@ -3939,7 +3939,9 @@ tidyTyCoVarBinder tidy_env (Bndr tv vis)
 
 tidyTyCoVarBinders :: TidyEnv -> [VarBndr TyCoVar vis]
                    -> (TidyEnv, [VarBndr TyCoVar vis])
-tidyTyCoVarBinders = mapAccumL tidyTyCoVarBinder
+tidyTyCoVarBinders tidy_env tvbs
+  = mapAccumL tidyTyCoVarBinder
+              (avoidNameClashes (binderVars tvbs) tidy_env) tvbs
 
 ---------------
 tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 7ff5bb4c84..555e73f390 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -2712,6 +2712,30 @@ In tcTypeKind we consider Constraint and (TYPE LiftedRep) to be distinct:
 Note that:
 * The only way we distinguish '->' from '=>' is by the fact
   that the argument is a PredTy.  Both are FunTys
+
+Note [Phantom type variables in kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  type K (r :: RuntimeRep) = Type   -- Note 'r' is unused
+  data T r :: K r                   -- T :: forall r -> K r
+  foo :: forall r. T r
+
+The body of the forall in foo's type has kind (K r), and
+normally it would make no sense to have
+   forall r. (ty :: K r)
+because the kind of the forall would escape the binding
+of 'r'.  But in this case it's fine because (K r) exapands
+to Type, so we expliclity /permit/ the type
+   forall r. T r
+
+To accommodate such a type, in typeKind (forall a.ty) we use
+occCheckExpand to expand any type synonyms in the kind of 'ty'
+to eliminate 'a'.  See kinding rule (FORALL) in
+Note [Kinding rules for types]
+
+And in TcValidity.checkEscapingKind, we use also use
+occCheckExpand, for the same reason.
 -}
 
 -----------------------------
@@ -2734,8 +2758,11 @@ typeKind (AppTy fun arg)
     go fun             args = piResultTys (typeKind fun) args
 
 typeKind ty@(ForAllTy {})
-  = case occCheckExpand tvs body_kind of   -- We must make sure tv does not occur in kind
-      Just k' -> k'                        -- As it is already out of scope!
+  = case occCheckExpand tvs body_kind of
+      -- We must make sure tv does not occur in kind
+      -- As it is already out of scope!
+      -- See Note [Phantom type variables in kinds]
+      Just k' -> k'
       Nothing -> pprPanic "typeKind"
                   (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
   where
@@ -2772,8 +2799,11 @@ tcTypeKind ty@(ForAllTy {})
   = constraintKind
 
   | otherwise
-  = case occCheckExpand tvs body_kind of   -- We must make sure tv does not occur in kind
-      Just k' -> k'                        -- As it is already out of scope!
+  = case occCheckExpand tvs body_kind of
+      -- We must make sure tv does not occur in kind
+      -- As it is already out of scope!
+      -- See Note [Phantom type variables in kinds]
+      Just k' -> k'
       Nothing -> pprPanic "tcTypeKind"
                   (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
   where