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.

12 files changed, 131 insertions, 34 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
diff --git a/testsuite/tests/dependent/should_compile/T16391a.hs b/testsuite/tests/dependent/should_compile/T16391a.hs
new file mode 100644
index 0000000000..d662af10ad
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T16391a.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16391a where
+
+import Data.Kind
+
+type Const (a :: Type) (b :: Type) = a
+type family F :: Const Type a where
+  F = Int
+type TS = (Int :: Const Type a)
+data T1 :: Const Type a where
+  MkT1 :: T1
+data T2 :: Const Type a -> Type where
+  MkT2 :: T2 b
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index e630f1a90a..4ba649ac9d 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -67,3 +67,4 @@ test('T14729', normal, compile, ['-ddump-types -fprint-typechecker-elaboration -
 test('T14729kind', normal, ghci_script, ['T14729kind.script'])
 test('T16326_Compile1', normal, compile, [''])
 test('T16326_Compile2', normal, compile, [''])
+test('T16391a', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/T16391b.hs b/testsuite/tests/dependent/should_fail/T16391b.hs
new file mode 100644
index 0000000000..f7049fb29d
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16391b.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16391b where
+
+import GHC.Exts
+
+type family T (r :: RuntimeRep) :: TYPE r
+
+foo :: T r
+foo = foo
diff --git a/testsuite/tests/dependent/should_fail/T16391b.stderr b/testsuite/tests/dependent/should_fail/T16391b.stderr
new file mode 100644
index 0000000000..35b5448917
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16391b.stderr
@@ -0,0 +1,6 @@
+
+T16391b.hs:10:8: error:
+    • Quantified type's kind mentions quantified type variable
+        type: ‘forall (r :: RuntimeRep). T r’
+      where the body of the forall has this kind: ‘TYPE r’
+    • In the type signature: foo :: T r
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index ca8a50addf..baaddd7442 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -52,3 +52,4 @@ test('T16326_Fail9', normal, compile_fail, [''])
 test('T16326_Fail10', normal, compile_fail, [''])
 test('T16326_Fail11', normal, compile_fail, [''])
 test('T16326_Fail12', normal, compile_fail, [''])
+test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
diff --git a/testsuite/tests/ghci/scripts/T11524a.stdout b/testsuite/tests/ghci/scripts/T11524a.stdout
index ea91ef9cd1..280eaf8d0a 100644
--- a/testsuite/tests/ghci/scripts/T11524a.stdout
+++ b/testsuite/tests/ghci/scripts/T11524a.stdout
@@ -7,7 +7,7 @@ pattern Pue :: a -> a1 -> (a, Ex) 	-- Defined at <interactive>:19:1
 pattern Pur :: (Eq a, Num a) => a -> [a]
   	-- Defined at <interactive>:20:1
 pattern Purp
-  :: (Eq a, Num a) => Show a1 => a -> a1 -> ([a], UnivProv a1)
+  :: (Eq a1, Num a1) => Show a2 => a1 -> a2 -> ([a1], UnivProv a2)
   	-- Defined at <interactive>:21:1
 pattern Pure :: (Eq a, Num a) => a -> a1 -> ([a], Ex)
   	-- Defined at <interactive>:22:1
@@ -32,10 +32,10 @@ pattern Pue :: forall {a}. () => forall {a1}. a -> a1 -> (a, Ex)
 pattern Pur :: forall {a}. (Eq a, Num a) => a -> [a]
   	-- Defined at <interactive>:20:1
 pattern Purp
-  :: forall {a} {a1}.
-     (Eq a, Num a) =>
-     Show a1 =>
-     a -> a1 -> ([a], UnivProv a1)
+  :: forall {a1} {a2}.
+     (Eq a1, Num a1) =>
+     Show a2 =>
+     a1 -> a2 -> ([a1], UnivProv a2)
   	-- Defined at <interactive>:21:1
 pattern Pure
   :: forall {a}. (Eq a, Num a) => forall {a1}. a -> a1 -> ([a], Ex)
diff --git a/testsuite/tests/patsyn/should_compile/T11213.stderr b/testsuite/tests/patsyn/should_compile/T11213.stderr
index ae8f15f4fa..212e3e9334 100644
--- a/testsuite/tests/patsyn/should_compile/T11213.stderr
+++ b/testsuite/tests/patsyn/should_compile/T11213.stderr
@@ -20,9 +20,9 @@ T11213.hs:23:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
 
 T11213.hs:24:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Pattern synonym with no type signature:
-      pattern Purp :: forall a a1.
-                      (Eq a, Num a) =>
-                      Show a1 => a -> a1 -> ([a], UnivProv a1)
+      pattern Purp :: forall a1 a2.
+                      (Eq a1, Num a1) =>
+                      Show a2 => a1 -> a2 -> ([a1], UnivProv a2)
 
 T11213.hs:25:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Pattern synonym with no type signature:
diff --git a/utils/haddock b/utils/haddock
-Subproject 07f2ca98fd4249dc6ebad053bd6aef90c814efe
+Subproject e7586f005aa89a45b0fc4f3564f0f17ab9f79d3