Use injectiveVarsOfType to catch dodgy type family instance binders (#17008)

Previously, we detected dodgy type family instances binders by
expanding type synonyms (via `exactTyCoVarsOfType`) and looking for
type variables on the RHS that weren't mentioned on the (expanded)
LHS. But this doesn't account for type families (like the example
in #17008), so we instead use `injectiveVarsOfType` to only count
LHS type variables that are in injective positions. That way, the `a`
in `type instance F (x :: T a) = a` will not count if `T` is a type
synonym _or_ a type family.

Along the way, I moved `exactTyCoVarsOfType` to `TyCoFVs` to live
alongside its sibling functions that also compute free variables.

Fixes #17008.

5 files changed, 61 insertions, 0 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/T17008b.hs b/testsuite/tests/indexed-types/should_compile/T17008b.hs
new file mode 100644
index 0000000000..25763684e4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T17008b.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T17008b where
+
+import Data.Kind
+
+type family ConstType1 (a :: Type) :: Type where
+  ConstType1 _ = Type
+
+type family F1 (x :: ConstType1 a) :: Type where
+  F1 @a (x :: ConstType1 a) = a
+type family F2 (x :: ConstType1 a) :: ConstType1 a where
+  F2 @a (x :: ConstType1 a) = x :: ConstType1 a
+type F3 (x :: ConstType1 a) = a
+type F4 (x :: ConstType1 a) = x :: ConstType1 a
+
+type ConstType2 (a :: Type) = Type
+
+type family G1 (x :: ConstType2 a) :: Type where
+  G1 @a (x :: ConstType2 a) = a
+type family G2 (x :: ConstType2 a) :: ConstType2 a where
+  G2 @a (x :: ConstType2 a) = x :: ConstType1 a
+type G3 (x :: ConstType2 a) = a
+type G4 (x :: ConstType2 a) = x :: ConstType2 a
+
+type Id1 (a :: Type) = a
+
+type family H (a :: Type) :: Type where
+  H (Id1 a) = a
+type family I (x :: Id1 a) :: Type where
+  I (x :: Id1 a) = a
+
+type family Id2 (a :: Type) :: Type where
+  Id2 a = a
+
+type family J (x :: Id2 a) :: Type where
+  J (x :: Id2 a) = a
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index f4ecabd83d..7eeeda6d59 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -291,3 +291,4 @@ test('T16356_Compile1', normal, compile, [''])
 test('T16356_Compile2', normal, compile, [''])
 test('T16632', normal, compile, ['-Wunused-type-patterns -fdiagnostics-show-caret'])
 test('T16828', normal, compile, [''])
+test('T17008b', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/T17008a.hs b/testsuite/tests/indexed-types/should_fail/T17008a.hs
new file mode 100644
index 0000000000..53d7f7737c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T17008a.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T17006 where
+
+import Data.Kind
+
+type family ConstType (a :: Type) :: Type where
+  ConstType _ = Type
+
+type family F (x :: ConstType a) :: Type where
+  F (x :: ConstType a) = a
+
+f :: F Int
+f = let x = x in x
diff --git a/testsuite/tests/indexed-types/should_fail/T17008a.stderr b/testsuite/tests/indexed-types/should_fail/T17008a.stderr
new file mode 100644
index 0000000000..8428a279b4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T17008a.stderr
@@ -0,0 +1,7 @@
+
+T17008a.hs:11:21: error:
+    • Type variable ‘a1’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
+        The real LHS (expanding synonyms) is: F @a2 x
+    • In the equations for closed type family ‘F’
+      In the type family declaration for ‘F’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 1ad9aa2504..ca1781b8fd 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -159,3 +159,4 @@ test('T16110_Fail3', normal, compile_fail, [''])
 test('T16356_Fail1', normal, compile_fail, [''])
 test('T16356_Fail2', normal, compile_fail, [''])
 test('T16356_Fail3', normal, compile_fail, [''])
+test('T17008a', normal, compile_fail, ['-fprint-explicit-kinds'])