Tighten checking for associated type instances

This patch finishes off Trac #11450.  Following debate on that ticket,
the patch tightens up the rules for what the instances of an
associated type can look like.  Now they must match the instance
header exactly. Eg

   class C a b where
    type T a x b

With this class decl, if we have an instance decl
  instance C ty1 ty2 where ...
then the type instance must look like
     type T ty1 v ty2 = ...
with exactly
  - 'ty1' for 'a'
  -  'ty2' for 'b', and
  - a variable for 'x'

For example:

  instance C [p] Int
    type T [p] y Int = (p,y,y)

Previously we allowed multiple instance equations and now, in effect,
we don't since they would all overlap.  If you want multiple cases,
use an auxiliary type family.

This is consistent with the treatment of generic-default instances,
and the user manual always said "WARNING: this facility (multiple
instance equations may be withdrawn in the future".

I also improved error messages, and did other minor refactoring.

3 files changed, 66 insertions, 64 deletions

diff --git a/testsuite/tests/ghci/scripts/T4175.hs b/testsuite/tests/ghci/scripts/T4175.hs
index 0fc53e76e9..0b7b554062 100644
--- a/testsuite/tests/ghci/scripts/T4175.hs
+++ b/testsuite/tests/ghci/scripts/T4175.hs
@@ -16,10 +16,10 @@ class C a where
     type D a b
 
 instance C Int where
-    type D Int () = String
+    type D Int b = String
 
 instance C () where
-    type D () () = Bool
+    type D () a = Bool
 
 type family E a where
     E ()  = Bool
diff --git a/testsuite/tests/ghci/scripts/T4175.stdout b/testsuite/tests/ghci/scripts/T4175.stdout
index e1ef925bea..d319bd630e 100644
--- a/testsuite/tests/ghci/scripts/T4175.stdout
+++ b/testsuite/tests/ghci/scripts/T4175.stdout
@@ -1,57 +1,56 @@
-type family A a b :: * 	-- Defined at T4175.hs:7:1
-type instance A (B a) b = () 	-- Defined at T4175.hs:10:15
-type instance A (Maybe a) a = a 	-- Defined at T4175.hs:9:15
-type instance A Int Int = () 	-- Defined at T4175.hs:8:15
-data family B a 	-- Defined at T4175.hs:12:1
-instance G B -- Defined at T4175.hs:34:10
-data instance B () = MkB 	-- Defined at T4175.hs:13:15
-type instance A (B a) b = () 	-- Defined at T4175.hs:10:15
-class C a where
-  type family D a b :: *
-  	-- Defined at T4175.hs:16:5
-type instance D () () = Bool 	-- Defined at T4175.hs:22:10
-type instance D Int () = String 	-- Defined at T4175.hs:19:10
-type family E a :: *
-  where
-      E () = Bool
-      E Int = String
-  	-- Defined at T4175.hs:24:1
-data () = () 	-- Defined in ‘GHC.Tuple’
-instance C () -- Defined at T4175.hs:21:10
-instance Bounded () -- Defined in ‘GHC.Enum’
-instance Enum () -- Defined in ‘GHC.Enum’
-instance Eq () -- Defined in ‘GHC.Classes’
-instance Ord () -- Defined in ‘GHC.Classes’
-instance Read () -- Defined in ‘GHC.Read’
-instance Show () -- Defined in ‘GHC.Show’
-instance Monoid () -- Defined in ‘GHC.Base’
-type instance D () () = Bool 	-- Defined at T4175.hs:22:10
-type instance D Int () = String 	-- Defined at T4175.hs:19:10
-data instance B () = MkB 	-- Defined at T4175.hs:13:15
-data Maybe a = Nothing | Just a 	-- Defined in ‘GHC.Base’
-instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’
-instance Monad Maybe -- Defined in ‘GHC.Base’
-instance Functor Maybe -- Defined in ‘GHC.Base’
-instance Ord a => Ord (Maybe a) -- Defined in ‘GHC.Base’
-instance Read a => Read (Maybe a) -- Defined in ‘GHC.Read’
-instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
-instance Applicative Maybe -- Defined in ‘GHC.Base’
-instance Foldable Maybe -- Defined in ‘Data.Foldable’
-instance Traversable Maybe -- Defined in ‘Data.Traversable’
-instance Monoid a => Monoid (Maybe a) -- Defined in ‘GHC.Base’
-type instance A (Maybe a) a = a 	-- Defined at T4175.hs:9:15
-data Int = I# Int# 	-- Defined in ‘GHC.Types’
-instance C Int -- Defined at T4175.hs:18:10
-instance Bounded Int -- Defined in ‘GHC.Enum’
-instance Enum Int -- Defined in ‘GHC.Enum’
-instance Eq Int -- Defined in ‘GHC.Classes’
-instance Integral Int -- Defined in ‘GHC.Real’
-instance Num Int -- Defined in ‘GHC.Num’
-instance Ord Int -- Defined in ‘GHC.Classes’
-instance Read Int -- Defined in ‘GHC.Read’
-instance Real Int -- Defined in ‘GHC.Real’
-instance Show Int -- Defined in ‘GHC.Show’
-type instance D Int () = String 	-- Defined at T4175.hs:19:10
-type instance A Int Int = () 	-- Defined at T4175.hs:8:15
-class Z a 	-- Defined at T4175.hs:28:1
-instance F (Z a) -- Defined at T4175.hs:31:10
+type family A a b :: * 	-- Defined at T4175.hs:7:1

+type instance A (B a) b = () 	-- Defined at T4175.hs:10:15

+type instance A (Maybe a) a = a 	-- Defined at T4175.hs:9:15

+type instance A Int Int = () 	-- Defined at T4175.hs:8:15

+data family B a 	-- Defined at T4175.hs:12:1

+instance G B -- Defined at T4175.hs:34:10

+data instance B () = MkB 	-- Defined at T4175.hs:13:15

+type instance A (B a) b = () 	-- Defined at T4175.hs:10:15

+class C a where

+  type family D a b :: *

+  	-- Defined at T4175.hs:16:5

+type instance D () a = Bool 	-- Defined at T4175.hs:22:10

+type instance D Int b = String 	-- Defined at T4175.hs:19:10

+type family E a :: *

+  where

+      E () = Bool

+      E Int = String

+  	-- Defined at T4175.hs:24:1

+data () = () 	-- Defined in ‘GHC.Tuple’

+instance C () -- Defined at T4175.hs:21:10

+instance Bounded () -- Defined in ‘GHC.Enum’

+instance Enum () -- Defined in ‘GHC.Enum’

+instance Eq () -- Defined in ‘GHC.Classes’

+instance Ord () -- Defined in ‘GHC.Classes’

+instance Read () -- Defined in ‘GHC.Read’

+instance Show () -- Defined in ‘GHC.Show’

+instance Monoid () -- Defined in ‘GHC.Base’

+type instance D () a = Bool 	-- Defined at T4175.hs:22:10

+data instance B () = MkB 	-- Defined at T4175.hs:13:15

+data Maybe a = Nothing | Just a 	-- Defined in ‘GHC.Base’

+instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’

+instance Monad Maybe -- Defined in ‘GHC.Base’

+instance Functor Maybe -- Defined in ‘GHC.Base’

+instance Ord a => Ord (Maybe a) -- Defined in ‘GHC.Base’

+instance Read a => Read (Maybe a) -- Defined in ‘GHC.Read’

+instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’

+instance Applicative Maybe -- Defined in ‘GHC.Base’

+instance Foldable Maybe -- Defined in ‘Data.Foldable’

+instance Traversable Maybe -- Defined in ‘Data.Traversable’

+instance Monoid a => Monoid (Maybe a) -- Defined in ‘GHC.Base’

+type instance A (Maybe a) a = a 	-- Defined at T4175.hs:9:15

+data Int = I# Int# 	-- Defined in ‘GHC.Types’

+instance C Int -- Defined at T4175.hs:18:10

+instance Bounded Int -- Defined in ‘GHC.Enum’

+instance Enum Int -- Defined in ‘GHC.Enum’

+instance Eq Int -- Defined in ‘GHC.Classes’

+instance Integral Int -- Defined in ‘GHC.Real’

+instance Num Int -- Defined in ‘GHC.Num’

+instance Ord Int -- Defined in ‘GHC.Classes’

+instance Read Int -- Defined in ‘GHC.Read’

+instance Real Int -- Defined in ‘GHC.Real’

+instance Show Int -- Defined in ‘GHC.Show’

+type instance D Int b = String 	-- Defined at T4175.hs:19:10

+type instance A Int Int = () 	-- Defined at T4175.hs:8:15

+class Z a 	-- Defined at T4175.hs:28:1

+instance F (Z a) -- Defined at T4175.hs:31:10

diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index c81c5218f8..5964262843 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -38,11 +38,14 @@
       L a = MaybeSyn a -- Defined at <interactive>:49:15
 
 <interactive>:55:41: error:
-    Type family equation violates injectivity annotation.
-    Kind variable ‘k’ cannot be inferred from the right-hand side.
-    (enabling -fprint-explicit-kinds might help)
-    In the type family equation:
-      PolyKindVarsF '[] = '[] -- Defined at <interactive>:55:41
+    • Polymorphic type indexes of associated type ‘PolyKindVarsF’
+        (i.e. ones independent of the class type variables)
+        must be distinct type variables
+      Expected: PolyKindVarsF '[]
+      Actual:   PolyKindVarsF '[]
+      Use -fprint-explicit-kinds to see the kind arguments
+    • In the type instance declaration for ‘PolyKindVarsF’
+      In the instance declaration for ‘PolyKindVarsC '[]’
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.