Get the in-scope set right in FamInstEnv.injectiveBranches

There was an assert error, as Gergo pointed out in #21896.

I fixed this by adding an InScopeSet argument to tcUnifyTyWithTFs.
And also to GHC.Core.Unify.niFixTCvSubst.

I also took the opportunity to get a couple more InScopeSets right,
and to change some substTyUnchecked into substTy.

This MR touches a lot of other files, but only because I also took the
opportunity to introduce mkInScopeSetList, and use it.

3 files changed, 34 insertions, 0 deletions

diff --git a/testsuite/tests/indexed-types/should_fail/T21896.hs b/testsuite/tests/indexed-types/should_fail/T21896.hs
new file mode 100644
index 0000000000..64ce18d023
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T21896.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE DataKinds, TypeFamilies, TypeFamilyDependencies, PolyKinds #-}
+module Bug where
+
+data T = Foo | Bar
+
+type family F (ns :: T) (ret :: k) = (r :: k) | r -> ret where
+    F Foo r = r
+    F Bar r = r
diff --git a/testsuite/tests/indexed-types/should_fail/T21896.stderr b/testsuite/tests/indexed-types/should_fail/T21896.stderr
new file mode 100644
index 0000000000..971c220171
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T21896.stderr
@@ -0,0 +1,24 @@
+
+T21896.hs:8:5: error:
+    • Type family equation right-hand sides overlap; this violates
+      the family's injectivity annotation:
+        forall {k} {r :: k}. F 'Foo r = r -- Defined at T21896.hs:8:5
+        forall {k} {r :: k}. F 'Bar r = r -- Defined at T21896.hs:9:5
+    • In the equations for closed type family ‘F’
+      In the type family declaration for ‘F’
+
+T21896.hs:8:5: error:
+    • Type family equation violates the family's injectivity annotation.
+      RHS of injective type family equation is a bare type variable
+      but these LHS type and kind patterns are not bare variables: ‘'Foo’
+        forall {k} {r :: k}. F 'Foo r = r -- Defined at T21896.hs:8:5
+    • In the equations for closed type family ‘F’
+      In the type family declaration for ‘F’
+
+T21896.hs:9:5: error:
+    • Type family equation violates the family's injectivity annotation.
+      RHS of injective type family equation is a bare type variable
+      but these LHS type and kind patterns are not bare variables: ‘'Bar’
+        forall {k} {r :: k}. F 'Bar r = r -- Defined at T21896.hs:9:5
+    • 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 5338a8780f..5a8d0cd88d 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -168,3 +168,4 @@ test('T20466', normal, compile_fail, [''])
 test('ExpandTFs', normal, compile_fail, [''])
 test('T20465', normal, compile_fail, [''])
 test('T20521', normal, compile_fail, [''])
+test('T21896', normal, compile_fail, [''])