Fix #10815 by kind-checking type patterns against known kinds.

tcFamTyPats now must take information about the instantiation of any
class variables, when checking the instance of an associated type.

Getting this to work out required some unexpected refactoring in
TcDeriv. TcDeriv needs to look at class instances because of the
possibility of associated datatypes with `deriving` specs. TcDeriv
worked over the user-specified instances. But any data family instances
were already processed, and TcDeriv had no way of finding the rep
tycons. Indeed, TcDeriv *re-type-checked* any data family instances
in an attempt to rediscover what GHC already knew. So, this commit
introduces better tracking of compiled data families between TcInstDcls
and TcDeriv to streamline all of this.

5 files changed, 68 insertions, 51 deletions

diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index e1c0055349..e3a330e88e 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -1,110 +1,110 @@
 
-<interactive>:10:15:
+<interactive>:10:15: error:
     Type family equations violate injectivity annotation:
       F Char Bool Int = Int
       F Bool Int Char = Int
 
-<interactive>:16:15:
+<interactive>:16:15: error:
     Type family equations violate injectivity annotation:
       I Int Char Bool = Bool
       I Int Int Int = Bool
 
-<interactive>:26:15:
+<interactive>:26:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       IdProxy a = Id a
 
-<interactive>:34:15:
+<interactive>:34:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘'Z’
       P 'Z m = m
 
-<interactive>:40:15:
+<interactive>:40:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘b’ does not appear on injective position.
     In the RHS of type family equation:
       J Int b c = Char
 
-<interactive>:44:15:
+<interactive>:44:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘n’ does not appear on injective position.
     In the RHS of type family equation:
       K ('S n) m = 'S m
 
-<interactive>:49:15:
+<interactive>:49:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       L a = MaybeSyn a
 
-<interactive>:55:41:
+<interactive>:55:41: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k1’ is not inferable from the RHS type variables.
+    Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
       PolyKindVarsF '[] = '[]
 
-<interactive>:60:15:
+<interactive>:60:15: error:
     Type family equation violates injectivity annotation.
     Injective kind variable ‘k1’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
       PolyKindVars '[] = '[]
 
-<interactive>:64:15:
+<interactive>:64:15: error:
     Type family equation violates injectivity annotation.
     Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Fc a b = Int
 
-<interactive>:68:15:
+<interactive>:68:15: error:
     Type family equation violates injectivity annotation.
     Injective type variables ‘a’, ‘b’ do not appear on injective position.
     Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
 
-<interactive>:81:15:
+<interactive>:81:15: error:
     Type family equations violate injectivity annotation:
       F1 [a] = Maybe (GF1 a)
       F1 (Maybe a) = Maybe (GF2 a)
 
-<interactive>:85:15:
+<interactive>:85:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘[a]’
       W1 [a] = a
 
-<interactive>:88:15:
+<interactive>:88:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       W2 [a] = W2 a
 
-<interactive>:92:15:
+<interactive>:92:15: error:
     Type family equations violate injectivity annotation:
       Z1 [a] = (a, a)
       Z1 (Maybe b) = (b, [b])
 
-<interactive>:96:15:
+<interactive>:96:15: error:
     Type family equations violate injectivity annotation:
       G1 [a] = [a]
       G1 (Maybe b) = [(b, b)]
 
-<interactive>:100:15:
+<interactive>:100:15: error:
     Type family equations violate injectivity annotation:
       G3 a Int = (a, Int)
       G3 a Bool = (Bool, a)
 
-<interactive>:104:15:
+<interactive>:104:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘b’ does not appear on injective position.
     In the RHS of type family equation:
       G4 a b = [a]
 
-<interactive>:107:15:
+<interactive>:107:15: error:
     Type family equations violate injectivity annotation:
       G5 [a] = [GF1 a]
       G5 Int = [Bool]
 
-<interactive>:111:15:
+<interactive>:111:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘a’ does not appear on injective position.
     In the RHS of type family equation:
diff --git a/testsuite/tests/indexed-types/should_compile/T10815.hs b/testsuite/tests/indexed-types/should_compile/T10815.hs
new file mode 100644
index 0000000000..08fcd02026
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T10815.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}
+
+module T10815 where
+
+import Data.Proxy
+
+type family Any :: k
+
+class kproxy ~ 'KProxy => C (kproxy :: KProxy k) where
+  type F (a :: k)
+  type G a :: k
+
+instance C ('KProxy :: KProxy Bool) where
+  type F a = Int
+  type G a = Any
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 5e7e468766..b98f963f61 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -263,3 +263,4 @@ test('T10634', normal, compile, [''])
 test('T10713', normal, compile, [''])
 test('T10753', normal, compile, [''])
 test('T10806', normal, compile_fail, [''])
+test('T10815', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/T9160.stderr b/testsuite/tests/indexed-types/should_fail/T9160.stderr
index e356f80c86..5850257ec4 100644
--- a/testsuite/tests/indexed-types/should_fail/T9160.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9160.stderr
@@ -1,6 +1,7 @@
 
-T9160.hs:18:8:
-    Type indexes must match class instance head
-    Found ‘* -> *’ but expected ‘*’
+T9160.hs:18:12: error:
+    Expecting one more argument to ‘Maybe’
+    Expected kind ‘*’, but ‘Maybe’ has kind ‘* -> *’
+    In the type ‘Maybe’
     In the type instance declaration for ‘F’
     In the instance declaration for ‘C (a :: *)’
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 440ddacd91..2e0267a3b8 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -4,145 +4,145 @@
 [4 of 5] Compiling T6018Afail       ( T6018Afail.hs, T6018Afail.o )
 [5 of 5] Compiling T6018fail        ( T6018fail.hs, T6018fail.o )
 
-T6018Afail.hs:7:15:
+T6018Afail.hs:7:15: error:
     Type family equations violate injectivity annotation:
       G Char Bool Int = Int
       G Bool Int Char = Int
 
-T6018Dfail.hs:7:15:
+T6018Dfail.hs:7:15: error:
     Type family equations violate injectivity annotation:
       T6018Bfail.H Bool Int Char = Int
       T6018Bfail.H Char Bool Int = Int
 
-T6018fail.hs:13:15:
+T6018fail.hs:13:15: error:
     Type family equations violate injectivity annotation:
       F Bool Int Char = Int
       F Char Bool Int = Int
 
-T6018fail.hs:19:15:
+T6018fail.hs:19:15: error:
     Type family equations violate injectivity annotation:
       I Int Int Int = Bool
       I Int Char Bool = Bool
 
-T6018fail.hs:28:15:
+T6018fail.hs:28:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       IdProxy a = Id a
 
-T6018fail.hs:36:15:
+T6018fail.hs:36:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘'Z’
       P 'Z m = m
 
-T6018fail.hs:37:15:
+T6018fail.hs:37:15: error:
     Type family equations violate injectivity annotation:
       P ('S n) m = 'S (P n m)
       P 'Z m = m
 
-T6018fail.hs:42:15:
+T6018fail.hs:42:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘b’ does not appear on injective position.
     In the RHS of type family equation:
       J Int b c = Char
 
-T6018fail.hs:46:15:
+T6018fail.hs:46:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘n’ does not appear on injective position.
     In the RHS of type family equation:
       K ('S n) m = 'S m
 
-T6018fail.hs:51:15:
+T6018fail.hs:51:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       L a = MaybeSyn a
 
-T6018fail.hs:59:10:
+T6018fail.hs:59:10: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k1’ is not inferable from the RHS type variables.
+    Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
       PolyKindVarsF '[] = '[]
 
-T6018fail.hs:62:15:
+T6018fail.hs:62:15: error:
     Type family equation violates injectivity annotation.
     Injective kind variable ‘k1’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
       PolyKindVars '[] = '[]
 
-T6018fail.hs:66:15:
+T6018fail.hs:66:15: error:
     Type family equation violates injectivity annotation.
     Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Fc a b = Int
 
-T6018fail.hs:70:15:
+T6018fail.hs:70:15: error:
     Type family equation violates injectivity annotation.
     Injective type variables ‘a’, ‘b’ do not appear on injective position.
     Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
 
-T6018fail.hs:75:15:
+T6018fail.hs:75:15: error:
     Type family equations violate injectivity annotation:
       F1 (Maybe a) = Maybe (GF2 a)
       F1 [a] = Maybe (GF1 a)
 
-T6018fail.hs:87:15:
+T6018fail.hs:87:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘[a]’
       W1 [a] = a
 
-T6018fail.hs:90:15:
+T6018fail.hs:90:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       W2 [a] = W2 a
 
-T6018fail.hs:95:15:
+T6018fail.hs:95:15: error:
     Type family equations violate injectivity annotation:
       Z1 (Maybe b) = (b, [b])
       Z1 [a] = (a, a)
 
-T6018fail.hs:99:15:
+T6018fail.hs:99:15: error:
     Type family equations violate injectivity annotation:
       G1 (Maybe b) = [(b, b)]
       G1 [a] = [a]
 
-T6018fail.hs:103:15:
+T6018fail.hs:103:15: error:
     Type family equations violate injectivity annotation:
       G3 a Bool = (Bool, a)
       G3 a Int = (a, Int)
 
-T6018fail.hs:106:15:
+T6018fail.hs:106:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘b’ does not appear on injective position.
     In the RHS of type family equation:
       G4 a b = [a]
 
-T6018fail.hs:110:15:
+T6018fail.hs:110:15: error:
     Type family equations violate injectivity annotation:
       G5 Int = [Bool]
       G5 [a] = [GF1 a]
 
-T6018fail.hs:113:15:
+T6018fail.hs:113:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘a’ does not appear on injective position.
     In the RHS of type family equation:
       G6 [a] = [HF1 a]
 
-T6018fail.hs:118:15:
+T6018fail.hs:118:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘c’ does not appear on injective position.
     Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
     forall (k :: BOX) a b (c :: k). G7 a b c = [G7a a b c]
 
-T6018fail.hs:129:1:
+T6018fail.hs:129:1: error:
     Type family equations violate injectivity annotation:
       FC Int Bool = Bool
       FC Int Char = Bool
 
-T6018fail.hs:134:1:
+T6018fail.hs:134:1: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘*’, ‘Char’