Fix #14369 by making injectivity warnings finer-grained

Summary:
Previously, GHC would always raise the possibility that a
type family might not be injective in certain error messages, even if
that type family actually //was// injective. Fix this by actually
checking for a type family's lack of injectivity before emitting
such an error message.

Test Plan: ./validate

Reviewers: goldfire, austin, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie

GHC Trac Issues: #14369

Differential Revision: https://phabricator.haskell.org/D4106

16 files changed, 58 insertions, 27 deletions

diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 525c6fbd72..0c6b54d1ff 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -1830,8 +1830,9 @@ mkEqInfoMsg ct ty1 ty2
     tyfun_msg | Just tc1 <- mb_fun1
               , Just tc2 <- mb_fun2
               , tc1 == tc2
+              , not (isInjectiveTyCon tc1 Nominal)
               = text "NB:" <+> quotes (ppr tc1)
-                <+> text "is a type function, and may not be injective"
+                <+> text "is a non-injective type family"
               | otherwise = empty
 
 isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
diff --git a/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr b/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
index 7a553f301c..9eab513529 100644
--- a/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
+++ b/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
@@ -3,9 +3,8 @@ NoMatchErr.hs:19:7: error:
     • Couldn't match type ‘Memo d0’ with ‘Memo d’
       Expected type: Memo d a -> Memo d a
         Actual type: Memo d0 a -> Memo d0 a
-      NB: ‘Memo’ is a type function, and may not be injective
+      NB: ‘Memo’ is a non-injective type family
       The type variable ‘d0’ is ambiguous
     • In the ambiguity check for ‘f’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature:
-        f :: (Fun d) => Memo d a -> Memo d a
+      In the type signature: f :: (Fun d) => Memo d a -> Memo d a
diff --git a/testsuite/tests/indexed-types/should_fail/T14369.hs b/testsuite/tests/indexed-types/should_fail/T14369.hs
new file mode 100644
index 0000000000..98afa3ecd6
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T14369.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T14369 where
+
+data family Sing (a :: k)
+
+data instance Sing (z :: Maybe a) where
+  SNothing :: Sing Nothing
+  SJust :: Sing x -> Sing (Just x)
+
+class SingKind k where
+  type Demote k = r | r -> k
+  fromSing :: Sing (a :: k) -> Demote k
+
+instance SingKind a => SingKind (Maybe a) where
+  type Demote (Maybe a) = Maybe (Demote a)
+  fromSing SNothing = Nothing
+  fromSing (SJust x) = Just (fromSing x)
+
+f :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x -> Maybe (Demote a)
+f = fromSing
diff --git a/testsuite/tests/indexed-types/should_fail/T14369.stderr b/testsuite/tests/indexed-types/should_fail/T14369.stderr
new file mode 100644
index 0000000000..4cac995464
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T14369.stderr
@@ -0,0 +1,9 @@
+
+T14369.hs:27:5: error:
+    • Couldn't match type ‘Demote a’ with ‘Demote a1’
+      Expected type: Sing (x a) -> Maybe (Demote a1)
+        Actual type: Sing (x a) -> Demote (Maybe a)
+    • In the expression: fromSing
+      In an equation for ‘f’: f = fromSing
+    • Relevant bindings include
+        f :: Sing (x a) -> Maybe (Demote a1) (bound at T14369.hs:27:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T1897b.stderr b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
index d3c8b06451..7694672b10 100644
--- a/testsuite/tests/indexed-types/should_fail/T1897b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
@@ -3,7 +3,7 @@ T1897b.hs:16:1: error:
     • Couldn't match type ‘Depend a’ with ‘Depend a0’
       Expected type: t (Depend a) -> Bool
         Actual type: t (Depend a0) -> Bool
-      NB: ‘Depend’ is a type function, and may not be injective
+      NB: ‘Depend’ is a non-injective type family
       The type variable ‘a0’ is ambiguous
     • In the ambiguity check for the inferred type for ‘isValid’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
diff --git a/testsuite/tests/indexed-types/should_fail/T1900.stderr b/testsuite/tests/indexed-types/should_fail/T1900.stderr
index 0783a2dba7..4b144f85f6 100644
--- a/testsuite/tests/indexed-types/should_fail/T1900.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T1900.stderr
@@ -3,7 +3,7 @@ T1900.hs:7:3: error:
     • Couldn't match type ‘Depend s0’ with ‘Depend s’
       Expected type: Depend s -> Depend s
         Actual type: Depend s0 -> Depend s0
-      NB: ‘Depend’ is a type function, and may not be injective
+      NB: ‘Depend’ is a non-injective type family
       The type variable ‘s0’ is ambiguous
     • In the ambiguity check for ‘trans’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index b943db2087..d5a9c56516 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -3,7 +3,7 @@ T2544.hs:17:12: error:
     • Couldn't match type ‘IxMap r’ with ‘IxMap i1’
       Expected type: IxMap (l :|: r) [Int]
         Actual type: BiApp (IxMap l) (IxMap i1) [Int]
-      NB: ‘IxMap’ is a type function, and may not be injective
+      NB: ‘IxMap’ is a non-injective type family
       The type variable ‘i1’ is ambiguous
     • In the expression: BiApp empty empty
       In an equation for ‘empty’: empty = BiApp empty empty
@@ -15,7 +15,7 @@ T2544.hs:17:18: error:
     • Couldn't match type ‘IxMap i0’ with ‘IxMap l’
       Expected type: IxMap l [Int]
         Actual type: IxMap i0 [Int]
-      NB: ‘IxMap’ is a type function, and may not be injective
+      NB: ‘IxMap’ is a non-injective type family
       The type variable ‘i0’ is ambiguous
     • In the first argument of ‘BiApp’, namely ‘empty’
       In the expression: BiApp empty empty
diff --git a/testsuite/tests/indexed-types/should_fail/T2664.stderr b/testsuite/tests/indexed-types/should_fail/T2664.stderr
index 21fbb64e3c..f52703865f 100644
--- a/testsuite/tests/indexed-types/should_fail/T2664.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2664.stderr
@@ -9,7 +9,7 @@ T2664.hs:31:9: error:
         at T2664.hs:23:5-12
       Expected type: IO (PChan (a :*: b), PChan c)
         Actual type: IO (PChan (a :*: b), PChan (Dual b :+: Dual a))
-      NB: ‘Dual’ is a type function, and may not be injective
+      NB: ‘Dual’ is a non-injective type family
     • In a stmt of a 'do' block:
         return
           (O $ takeMVar v, 
diff --git a/testsuite/tests/indexed-types/should_fail/T4099.stderr b/testsuite/tests/indexed-types/should_fail/T4099.stderr
index a0ddc964ff..acc2ed29ae 100644
--- a/testsuite/tests/indexed-types/should_fail/T4099.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4099.stderr
@@ -1,7 +1,7 @@
 
 T4099.hs:11:30: error:
     • Couldn't match expected type ‘T a0’ with actual type ‘T b’
-      NB: ‘T’ is a type function, and may not be injective
+      NB: ‘T’ is a non-injective type family
       The type variable ‘a0’ is ambiguous
     • In the second argument of ‘foo’, namely ‘x’
       In the expression: foo (error "urk") x
diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr
index 516bdf3802..2f0d5e3644 100644
--- a/testsuite/tests/indexed-types/should_fail/T4179.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr
@@ -7,7 +7,7 @@ T4179.hs:26:16: error:
         Actual type: x (A2 (FCon x) -> A3 (FCon x))
                      -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
                      -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
-      NB: ‘A2’ is a type function, and may not be injective
+      NB: ‘A2’ is a non-injective type family
     • In the first argument of ‘foldDoC’, namely ‘op’
       In the expression: foldDoC op
       In an equation for ‘fCon’: fCon = foldDoC op
diff --git a/testsuite/tests/indexed-types/should_fail/T9036.stderr b/testsuite/tests/indexed-types/should_fail/T9036.stderr
index cb12dea5b5..6f2c162f1a 100644
--- a/testsuite/tests/indexed-types/should_fail/T9036.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9036.stderr
@@ -3,7 +3,7 @@ T9036.hs:17:17: error:
     • Couldn't match type ‘Curried t0 [t0]’ with ‘Curried t [t]’
       Expected type: Maybe (GetMonad t after) -> Curried t [t]
         Actual type: Maybe (GetMonad t0 after) -> Curried t0 [t0]
-      NB: ‘Curried’ is a type function, and may not be injective
+      NB: ‘Curried’ is a non-injective type family
       The type variable ‘t0’ is ambiguous
     • In the ambiguity check for ‘simpleLogger’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
diff --git a/testsuite/tests/indexed-types/should_fail/T9171.stderr b/testsuite/tests/indexed-types/should_fail/T9171.stderr
index db44dd7185..0f70348850 100644
--- a/testsuite/tests/indexed-types/should_fail/T9171.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9171.stderr
@@ -2,7 +2,7 @@
 T9171.hs:10:20: error:
     • Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
                   with actual type ‘GetParam Base (GetParam Base Int)’
-      NB: ‘GetParam’ is a type function, and may not be injective
+      NB: ‘GetParam’ is a non-injective type family
       The type variable ‘k20’ is ambiguous
       Use -fprint-explicit-kinds to see the kind arguments
     • In the ambiguity check for an expression type signature
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 3af724d1b9..4d25d970b9 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -140,3 +140,4 @@ test('T13972', normal, compile_fail, [''])
 test('T14033', normal, compile_fail, [''])
 test('T14045a', normal, compile_fail, [''])
 test('T14175', normal, compile_fail, [''])
+test('T14369', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index 719895af6c..decc6adaba 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -2,18 +2,12 @@
 T5853.hs:15:46: error:
     • Could not deduce: Subst (Subst fa a) b ~ Subst fa b
         arising from a use of ‘<$>’
-      from the context: (F fa,
-                         Elem fa ~ Elem fa,
-                         Elem (Subst fa b) ~ b,
-                         Subst fa b ~ Subst fa b,
-                         Subst (Subst fa b) (Elem fa) ~ fa,
-                         F (Subst fa a),
-                         Elem (Subst fa a) ~ a,
-                         Elem fa ~ Elem fa,
-                         Subst (Subst fa a) (Elem fa) ~ fa,
-                         Subst fa a ~ Subst fa a)
+      from the context: (F fa, Elem fa ~ Elem fa, Elem (Subst fa b) ~ b,
+                         Subst fa b ~ Subst fa b, Subst (Subst fa b) (Elem fa) ~ fa,
+                         F (Subst fa a), Elem (Subst fa a) ~ a, Elem fa ~ Elem fa,
+                         Subst (Subst fa a) (Elem fa) ~ fa, Subst fa a ~ Subst fa a)
         bound by the RULE "map/map" at T5853.hs:15:2-57
-      NB: ‘Subst’ is a type function, and may not be injective
+      NB: ‘Subst’ is a non-injective type family
     • In the expression: (f . g) <$> xs
       When checking the transformation rule "map/map"
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/T8030.stderr b/testsuite/tests/typecheck/should_fail/T8030.stderr
index d9c34cd533..c1ff38b685 100644
--- a/testsuite/tests/typecheck/should_fail/T8030.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8030.stderr
@@ -1,7 +1,7 @@
 
 T8030.hs:9:3: error:
     • Couldn't match expected type ‘Pr a’ with actual type ‘Pr a0’
-      NB: ‘Pr’ is a type function, and may not be injective
+      NB: ‘Pr’ is a non-injective type family
       The type variable ‘a0’ is ambiguous
     • In the ambiguity check for ‘op1’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
@@ -13,7 +13,7 @@ T8030.hs:10:3: error:
     • Couldn't match type ‘Pr a0’ with ‘Pr a’
       Expected type: Pr a -> Pr a -> Pr a
         Actual type: Pr a0 -> Pr a0 -> Pr a0
-      NB: ‘Pr’ is a type function, and may not be injective
+      NB: ‘Pr’ is a non-injective type family
       The type variable ‘a0’ is ambiguous
     • In the ambiguity check for ‘op2’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
diff --git a/testsuite/tests/typecheck/should_fail/T8034.stderr b/testsuite/tests/typecheck/should_fail/T8034.stderr
index 247732a0bd..cce73f355a 100644
--- a/testsuite/tests/typecheck/should_fail/T8034.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8034.stderr
@@ -3,7 +3,7 @@ T8034.hs:6:3: error:
     • Couldn't match type ‘F a0’ with ‘F a’
       Expected type: F a -> F a
         Actual type: F a0 -> F a0
-      NB: ‘F’ is a type function, and may not be injective
+      NB: ‘F’ is a non-injective type family
       The type variable ‘a0’ is ambiguous
     • In the ambiguity check for ‘foo’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes