Fix #12369 by being more flexible with data insts

Previously, a data family's kind had to end in `Type`,
and data instances had to list all the type patterns for the
family. However, both of these restrictions were unnecessary:

- A data family's kind can usefully end in a kind variable `k`.
  See examples on #12369.

- A data instance need not list all patterns, much like how a
  GADT-style data declaration need not list all type parameters,
  when a kind signature is in place. This is useful, for example,
  here:

    data family Sing (a :: k)
    data instance Sing :: Bool -> Type where ...

This patch also improved a few error messages, as some error
plumbing had to be moved around.

See new Note [Arity of data families] in FamInstEnv for more
info.

test case: indexed-types/should_compile/T12369

7 files changed, 49 insertions, 26 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/T12369.hs b/testsuite/tests/indexed-types/should_compile/T12369.hs
new file mode 100644
index 0000000000..51cee7df03
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T12369.hs
@@ -0,0 +1,35 @@
+{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies, RankNTypes, TypeInType,
+             TypeOperators, ConstraintKinds #-}
+
+module T12369 where
+
+import Data.Kind
+
+data family Fix :: (k -> *) -> k
+newtype instance Fix f = In { out :: f (Fix f) }
+
+type FREE k = (k -> Constraint) -> (k -> k)
+type f  ~> g = forall a. f a -> g a
+type f ~~> g = forall a b. f a b -> g a b
+
+data    family   Free k :: FREE k
+
+newtype instance Free Type k p where
+  Free0 :: (forall q. k q => (p  -> q) -> q) -> Free Type k p
+
+newtype instance Free (j -> Type) k p a where
+  Free1 :: (forall q. k q => (p  ~> q) -> q a) -> Free (j -> Type) k p a
+
+newtype instance Free (j1 -> j2 -> Type) k p a b where
+  Free2 :: (forall q. k q => (p ~~> q) -> q a b) -> Free (j1 -> j2 -> Type) k p a b
+
+data family Free2 :: FREE k
+
+newtype instance Free2 :: FREE Type where
+  Free20 :: (forall q. k q => (p  -> q) -> q) -> Free2 k p
+
+newtype instance Free2 :: forall k. FREE (k -> Type) where
+  Free21 :: (forall q. k q => (p  ~> q) -> q a) -> Free2 k p a
+
+newtype instance Free2 :: forall k1 k2. FREE (k1 -> k2 -> Type) where
+  Free22 :: (forall q. k q => (p ~~> q) -> q a b) -> Free2 k p a b
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index ec55113e6b..84e23982de 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -265,3 +265,4 @@ test('T13398a', normal, compile, [''])
 test('T13398b', normal, compile, [''])
 test('T13662', normal, compile, [''])
 test('T13705', normal, compile, [''])
+test('T12369', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
index f2ea8b2668..5bc6aca64c 100644
--- a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
@@ -1,12 +1,12 @@
 
 ExtraTcsUntch.hs:23:18: error:
-    • Couldn't match expected type ‘F Int’ with actual type ‘[x]’
+    • Couldn't match expected type ‘F Int’ with actual type ‘[p]’
     • In the first argument of ‘h’, namely ‘[x]’
       In the expression: h [x]
       In an equation for ‘g1’: g1 _ = h [x]
     • Relevant bindings include
-        x :: x (bound at ExtraTcsUntch.hs:21:3)
-        f :: x -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
+        x :: p (bound at ExtraTcsUntch.hs:21:3)
+        f :: p -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
 
 ExtraTcsUntch.hs:25:38: error:
     • Couldn't match expected type ‘F Int’ with actual type ‘[[a0]]’
diff --git a/testsuite/tests/indexed-types/should_fail/Overlap4.stderr b/testsuite/tests/indexed-types/should_fail/Overlap4.stderr
index 937a18d861..53dc8b4ac0 100644
--- a/testsuite/tests/indexed-types/should_fail/Overlap4.stderr
+++ b/testsuite/tests/indexed-types/should_fail/Overlap4.stderr
@@ -1,6 +1,4 @@
 
-Overlap4.hs:7:12: error:
-    • Expecting one more argument to ‘Maybe’
-      Expected a type, but ‘Maybe’ has kind ‘* -> *’
-    • In the type ‘Maybe’
-      In the type family declaration for ‘F’
+Overlap4.hs:7:3: error:
+    • Number of parameters must match family declaration; expected 2
+    • In the type family declaration for ‘F’
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
index e872f115a2..43c72cffb5 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
@@ -1,6 +1,4 @@
 
-SimpleFail1b.hs:4:1:
-    Too many parameters to T1:
-      Char is unexpected;
-      expected only two parameters
-    In the data instance declaration for ‘T1’
+SimpleFail1b.hs:4:1: error:
+    • Number of parameters must match family declaration; expected 2
+    • In the data instance declaration for ‘T1’
diff --git a/testsuite/tests/indexed-types/should_fail/TyFamArity1.stderr b/testsuite/tests/indexed-types/should_fail/TyFamArity1.stderr
index 8b3d5f5910..46521deeba 100644
--- a/testsuite/tests/indexed-types/should_fail/TyFamArity1.stderr
+++ b/testsuite/tests/indexed-types/should_fail/TyFamArity1.stderr
@@ -1,6 +1,4 @@
 
-TyFamArity1.hs:4:23: error:
-    • Expecting one more argument to ‘IO’
-      Expected a type, but ‘IO’ has kind ‘* -> *’
-    • In the type ‘IO’
-      In the type instance declaration for ‘T’
+TyFamArity1.hs:4:15: error:
+    • Number of parameters must match family declaration; expected 2
+    • In the type instance declaration for ‘T’
diff --git a/testsuite/tests/indexed-types/should_fail/TyFamArity2.stderr b/testsuite/tests/indexed-types/should_fail/TyFamArity2.stderr
index 778d8ab9f4..8d48921946 100644
--- a/testsuite/tests/indexed-types/should_fail/TyFamArity2.stderr
+++ b/testsuite/tests/indexed-types/should_fail/TyFamArity2.stderr
@@ -1,11 +1,4 @@
 
 TyFamArity2.hs:4:15: error:
-    • Too many parameters to T:
-        Float is unexpected;
-        expected only one parameter
+    • Number of parameters must match family declaration; expected 1
     • In the type instance declaration for ‘T’
-
-TyFamArity2.hs:4:29: error:
-    • Expected kind ‘* -> *’, but ‘Char’ has kind ‘*’
-    • In the type ‘Char’
-      In the type instance declaration for ‘T’