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.

7 files changed, 43 insertions, 8 deletions

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: