Re-polish error messages around injective TFs.

The previous message was wrong, as pointed out by Jan Stolarek.

4 files changed, 69 insertions, 57 deletions

diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index 0fc692eadb..796bbcb582 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -559,27 +559,28 @@ conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
 unusedInjectiveVarsErr :: TyVarSet -> InjErrorBuilder -> CoAxBranch
                        -> (SDoc, SrcSpan)
 unusedInjectiveVarsErr unused_tyvars errorBuilder tyfamEqn
-  = errorBuilder (injectivityErrorHerald True $$
-                  mkUnusedInjectiveVarsErr unused_tyvars) [tyfamEqn]
+  = errorBuilder (injectivityErrorHerald True $$ unusedInjectiveVarsErr)
+                 [tyfamEqn]
     where
-      mkUnusedInjectiveVarsErr :: TyVarSet -> SDoc
-      mkUnusedInjectiveVarsErr unused_tyvars =
-          let tyVars = varSetElems $ filterVarSet isTypeVar unused_tyvars
-              kiVars = varSetElems $ filterVarSet isKindVar unused_tyvars
-              tyVarsSDoc
-                  = if not (null tyVars)
-                    then text "Injective type variable" <> plural tyVars <+>
-                         pprQuotedList tyVars <+> doOrDoes tyVars <+>
-                         text "not appear on the right-hand side."
-                    else empty
-              kiVarsSDoc
-                  = if not (null kiVars)
-                    then text "Injective kind variable" <> plural kiVars <+>
-                         pprQuotedList kiVars <+> isOrAre kiVars <+>
-                         text "not inferrable from the RHS type variables."
-                    else empty
-          in tyVarsSDoc $$ kiVarsSDoc $$
-             text "In the type family equation:"
+      tvs = varSetElemsKvsFirst unused_tyvars
+      has_types = any isTypeVar tvs
+      has_kinds = any isKindVar tvs
+
+      doc = sep [ what <+> text "variable" <>
+                  plural tvs <+> pprQuotedList tvs
+                , text "cannot be inferred from the right-hand side." ]
+      what = case (has_types, has_kinds) of
+               (True, True)   -> text "Type and kind"
+               (True, False)  -> text "Type"
+               (False, True)  -> text "Kind"
+               (False, False) -> pprPanic "mkUnusedInjectiveVarsErr" $
+                                 ppr unused_tyvars
+      print_kinds_info = sdocWithDynFlags $ \ dflags ->
+                         if has_kinds && not (gopt Opt_PrintExplicitKinds dflags)
+                         then text "(enabling -fprint-explicit-kinds might help)"
+                         else empty
+      unusedInjectiveVarsErr = doc $$ print_kinds_info $$
+                               text "In the type family equation:"
 
 -- | Build error message for equation that has a type family call at the top
 -- level of RHS
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index d90dcce897..d1ebe58007 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -22,13 +22,13 @@
 
 <interactive>:40:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘b’ does not appear on the right-hand side.
+    Type variable ‘b’ cannot be inferred from the right-hand side.
     In the type family equation:
       J Int b c = Char
 
 <interactive>:44:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘n’ does not appear on the right-hand side.
+    Type variable ‘n’ cannot be inferred from the right-hand side.
     In the type family equation:
       K ('S n) m = 'S m
 
@@ -39,26 +39,30 @@
 
 <interactive>:55:41: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k’ is not inferrable from the RHS type variables.
+    Kind variable ‘k’ cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
       PolyKindVarsF '[] = '[]
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k1’ is not inferrable from the RHS type variables.
+    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
       PolyKindVars '[] = '[]
 
 <interactive>:64:15: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k’ is not inferrable from the RHS type variables.
+    Kind variable ‘k’ cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Fc a b = Int
 
 <interactive>:68:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variables ‘a’, ‘b’ do not appear on the right-hand side.
-    Injective kind variable ‘k’ is not inferrable from the RHS type variables.
+    Type and kind variables ‘k’, ‘a’, ‘b’
+    cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
 
@@ -95,7 +99,7 @@
 
 <interactive>:104:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘b’ does not appear on the right-hand side.
+    Type variable ‘b’ cannot be inferred from the right-hand side.
     In the type family equation:
       G4 a b = [a]
 
@@ -106,6 +110,6 @@
 
 <interactive>:111:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘a’ does not appear on the right-hand side.
+    Type variable ‘a’ cannot be inferred from the right-hand side.
     In the type family equation:
       G6 [a] = [HF1 a]
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index cb8d8abb6e..a86ad808c8 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -42,13 +42,13 @@ T6018fail.hs:37:15: error:
 
 T6018fail.hs:42:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘b’ does not appear on the right-hand side.
+    Type variable ‘b’ cannot be inferred from the right-hand side.
     In the type family equation:
       J Int b c = Char
 
 T6018fail.hs:46:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘n’ does not appear on the right-hand side.
+    Type variable ‘n’ cannot be inferred from the right-hand side.
     In the type family equation:
       K ('S n) m = 'S m
 
@@ -59,26 +59,30 @@ T6018fail.hs:51:15: error:
 
 T6018fail.hs:59:10: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k’ is not inferrable from the RHS type variables.
+    Kind variable ‘k’ cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
       PolyKindVarsF '[] = '[]
 
 T6018fail.hs:62:15: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k1’ is not inferrable from the RHS type variables.
+    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
       PolyKindVars '[] = '[]
 
 T6018fail.hs:66:15: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k’ is not inferrable from the RHS type variables.
+    Kind variable ‘k’ cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Fc a b = Int
 
 T6018fail.hs:70:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variables ‘a’, ‘b’ do not appear on the right-hand side.
-    Injective kind variable ‘k’ is not inferrable from the RHS type variables.
+    Type and kind variables ‘k’, ‘a’, ‘b’
+    cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
 
@@ -115,7 +119,7 @@ T6018fail.hs:103:15: error:
 
 T6018fail.hs:106:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘b’ does not appear on the right-hand side.
+    Type variable ‘b’ cannot be inferred from the right-hand side.
     In the type family equation:
       G4 a b = [a]
 
@@ -126,14 +130,15 @@ T6018fail.hs:110:15: error:
 
 T6018fail.hs:113:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘a’ does not appear on the right-hand side.
+    Type variable ‘a’ cannot be inferred from the right-hand side.
     In the type family equation:
       G6 [a] = [HF1 a]
 
 T6018fail.hs:118:15: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘c’ does not appear on the right-hand side.
-    Injective kind variable ‘k’ is not inferrable from the RHS type variables.
+    Type and kind variables ‘k’, ‘c’
+    cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
     forall (k :: BOX) a b (c :: k). G7 a b c = [G7a a b c]
 
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
index e8fcef8896..674440046e 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
@@ -1,12 +1,12 @@
 
-T6018failclosed.hs:11:5:
+T6018failclosed.hs:11:5: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       IdProxyClosed a = IdClosed a
     In the equations for closed type family ‘IdProxyClosed’
     In the type family declaration for ‘IdProxyClosed’
 
-T6018failclosed.hs:19:5:
+T6018failclosed.hs:19:5: 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’
@@ -14,71 +14,73 @@ T6018failclosed.hs:19:5:
     In the equations for closed type family ‘PClosed’
     In the type family declaration for ‘PClosed’
 
-T6018failclosed.hs:19:5:
+T6018failclosed.hs:19:5: error:
     Type family equations violate injectivity annotation:
       PClosed 'Z m = m
       PClosed ('S n) m = 'S (PClosed n m)
     In the equations for closed type family ‘PClosed’
     In the type family declaration for ‘PClosed’
 
-T6018failclosed.hs:25:5:
+T6018failclosed.hs:25:5: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘b’ does not appear on the right-hand side.
-    Injective kind variable ‘k’ is not inferrable from the RHS type variables.
+    Type and kind variables ‘k’, ‘b’
+    cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
     forall (k :: BOX) (k1 :: BOX) (b :: k) (c :: k1).
       JClosed Int b c = Char
     In the equations for closed type family ‘JClosed’
     In the type family declaration for ‘JClosed’
 
-T6018failclosed.hs:30:5:
+T6018failclosed.hs:30:5: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘n’ does not appear on the right-hand side.
+    Type variable ‘n’ cannot be inferred from the right-hand side.
     In the type family equation:
       KClosed ('S n) m = 'S m
     In the equations for closed type family ‘KClosed’
     In the type family declaration for ‘KClosed’
 
-T6018failclosed.hs:35:5:
+T6018failclosed.hs:35:5: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
     forall (k :: BOX) (a :: k). LClosed a = MaybeSynClosed a
     In the equations for closed type family ‘LClosed’
     In the type family declaration for ‘LClosed’
 
-T6018failclosed.hs:39:5:
+T6018failclosed.hs:39:5: error:
     Type family equations violate injectivity annotation:
       FClosed Char Bool Int = Int
       FClosed Bool Int Char = Int
     In the equations for closed type family ‘FClosed’
     In the type family declaration for ‘FClosed’
 
-T6018failclosed.hs:43:5:
+T6018failclosed.hs:43:5: error:
     Type family equations violate injectivity annotation:
       IClosed Int Char Bool = Bool
       IClosed Int Int Int = Bool
     In the equations for closed type family ‘IClosed’
     In the type family declaration for ‘IClosed’
 
-T6018failclosed.hs:50:3:
+T6018failclosed.hs:50:3: error:
     Type family equation violates injectivity annotation.
-    Injective type variable ‘a’ does not appear on the right-hand side.
+    Type variable ‘a’ cannot be inferred from the right-hand side.
     In the type family equation:
       E2 a = 'False
     In the equations for closed type family ‘E2’
     In the type family declaration for ‘E2’
 
-T6018failclosed.hs:61:3:
+T6018failclosed.hs:61:3: error:
     Type family equations violate injectivity annotation:
       F a IO = IO a
       F Char b = b Int
     In the equations for closed type family ‘F’
     In the type family declaration for ‘F’
 
-T6018failclosed.hs:66:5:
+T6018failclosed.hs:66:5: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k’ is not inferrable from the RHS type variables.
+    Kind variable ‘k’ cannot be inferred from the right-hand side.
+    (enabling -fprint-explicit-kinds might help)
     In the type family equation:
-      forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
+    forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
     In the equations for closed type family ‘Gc’
     In the type family declaration for ‘Gc’