Testsuite cleanup

As a result of fixing #10836 it is now possible to merge 11 different
tests for #6018 into one

testsuite/tests/typecheck/should_fail/T6018failclosed.hs

+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, UndecidableInstances #-}
+
+module T6018failclosed where
+
+-- Id is injective...
+type family IdClosed a = result | result -> a where
+    IdClosed a = a
+
+-- ...but despite that we disallow a call to Id
+type family IdProxyClosed (a :: *) = r | r -> a where
+    IdProxyClosed a = IdClosed a
+
+data N = Z | S N
+
+-- PClosed is not injective, although the user declares otherwise. This
+-- should be rejected on the grounds of calling a type family in the
+-- RHS.
+type family PClosed (a :: N) (b :: N) = (r :: N) | r -> a b where
+    PClosed  Z    m = m
+    PClosed (S n) m = S (PClosed n m)
+
+-- this is not injective - not all injective type variables mentioned
+-- on LHS are mentioned on RHS
+type family JClosed a b c = r | r -> a b where
+    JClosed Int b c = Char
+
+-- this is not injective - not all injective type variables mentioned
+-- on LHS are mentioned on RHS (tyvar is now nested inside a tycon)
+type family KClosed (a :: N) (b :: N) = (r :: N) | r -> a b where
+    KClosed (S n) m = S m
+
+-- hiding a type family application behind a type synonym should be rejected
+type MaybeSynClosed a = IdClosed a
+type family LClosed a = r | r -> a where
+    LClosed a = MaybeSynClosed a
+
+type family FClosed a b c = (result :: *) | result -> a b c where
+    FClosed Int  Char Bool = Bool
+    FClosed Char Bool Int  = Int
+    FClosed Bool Int  Char = Int
+
+type family IClosed a b c = r | r -> a b where
+    IClosed Int  Char Bool = Bool
+    IClosed Int  Int  Int  = Bool
+    IClosed Bool Int  Int  = Int
+
+type family E2 (a :: Bool) = r | r -> a where
+  E2 False = True
+  E2 True  = False
+  E2 a     = False
+
+-- This exposed a subtle bug in the implementation during development. After
+-- unifying the RHS of (1) and (2) the LHS substitution was done only in (2)
+-- which made it look like an overlapped equation. This is not the case and this
+-- definition should be rejected. The first two equations are here to make sure
+-- that the internal implementation does list indexing corrcectly (this is a bit
+-- tricky because the list is kept in reverse order).
+type family F a b  = r | r -> a b where
+  F Float  IO      = Float
+  F Bool   IO      = Bool
+  F a      IO      = IO a   -- (1)
+  F Char   b       = b Int  -- (2)
+
+-- This should fail because there is no way to determine a, b and k from the RHS
+type family Gc (a :: k) (b :: k) = r | r -> k where
+    Gc a b = Int

testsuite/tests/typecheck/should_fail/T6018failclosed.stderr

+
+T6018failclosed.hs:11:5:
+    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:
+    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’
+      PClosed 'Z m = m
+    In the equations for closed type family ‘PClosed’
+    In the type family declaration for ‘PClosed’
+
+T6018failclosed.hs:19:5:
+    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:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘b’ 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) (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:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘n’ does not appear on injective position.
+    In the RHS of 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:
+    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:
+    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:
+    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:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘a’ does not appear on injective position.
+    In the RHS of 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:
+    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:
+    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). Gc a b = Int
+    In the equations for closed type family ‘Gc’
+    In the type family declaration for ‘Gc’

testsuite/tests/typecheck/should_fail/T6018failclosed1.hs

-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
-
-module T6018failclosed1 where
-
--- Id is injective...
-type family IdClosed a = result | result -> a where
-    IdClosed a = a
-
--- ...but despite that we disallow a call to Id
-type family IdProxyClosed a = r | r -> a where
-    IdProxyClosed a = IdClosed a

testsuite/tests/typecheck/should_fail/T6018failclosed1.stderr

-
-T6018failclosed1.hs:11:5:
-    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’

testsuite/tests/typecheck/should_fail/T6018failclosed10.hs

-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
-
-module T6018failclosed10 where
-
--- this one is a strange beast. Last equation is unreachable and thus it is
--- removed. It is then impossible to typecheck barapp and thus we generate an
--- error
-type family Bar a = r | r -> a where
-    Bar Int  = Bool
-    Bar Bool = Int
-    Bar Bool = Char
-
-bar :: Bar a -> Bar a
-bar x = x
-
-barapp :: Char
-barapp = bar 'c'

testsuite/tests/typecheck/should_fail/T6018failclosed10.stderr

-
-T6018failclosed10.hs:17:14:
-    Couldn't match expected type ‘Bar a0’ with actual type ‘Char’
-    The type variable ‘a0’ is ambiguous
-    In the first argument of ‘bar’, namely ‘'c'’
-    In the expression: bar 'c'
-    In an equation for ‘barapp’: barapp = bar 'c'
-
-

testsuite/tests/typecheck/should_fail/T6018failclosed11.hs

-{-# LANGUAGE TypeFamilies #-}
-
-module T6018failclosed12 where
-
--- This exposed a subtle bug in the implementation during development. After
--- unifying the RHS of (1) and (2) the LHS substitution was done only in (2)
--- which made it look like an overlapped equation. This is not the case and this
--- definition should be rejected. The first two equations are here to make sure
--- that the internal implementation does list indexing corrcectly (this is a bit
--- tricky because the list is kept in reverse order).
-type family F a b  = r | r -> a b where
-  F Float  IO      = Float
-  F Bool   IO      = Bool
-  F a      IO      = IO a   -- (1)
-  F Char   b       = b Int  -- (2)

testsuite/tests/typecheck/should_fail/T6018failclosed11.stderr

-
-T6018failclosed11.hs:14:3:
-    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’

testsuite/tests/typecheck/should_fail/T6018failclosed12.hs

-{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
-
-module T6018failclosed12 where
-
--- This should fail because there is no way to determine a, b and k from the RHS
-type family Gc (a :: k) (b :: k) = r | r -> k where
-    Gc a b = Int

testsuite/tests/typecheck/should_fail/T6018failclosed12.stderr

-
-T6018failclosed12.hs:7:5:
-    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). Gc a b = Int
-    In the equations for closed type family ‘Gc’
-    In the type family declaration for ‘Gc’

testsuite/tests/typecheck/should_fail/T6018failclosed2.hs

-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies  #-}
 
 module T6018failclosed2 where
 
-data N = Z | S N
+-- this one is a strange beast. Last equation is unreachable and thus it is
+-- removed. It is then impossible to typecheck barapp and thus we generate an
+-- error
+type family Bar a = r | r -> a where
+    Bar Int  = Bool
+    Bar Bool = Int
+    Bar Bool = Char
 
--- PClosed is not injective, although the user declares otherwise. This
--- should be rejected on the grounds of calling a type family in the
--- RHS.
-type family PClosed (a :: N) (b :: N) = (r :: N) | r -> a b where
-    PClosed  Z    m = m
-    PClosed (S n) m = S (PClosed n m)
+bar :: Bar a -> Bar a
+bar x = x
+
+barapp :: Char
+barapp = bar 'c'

testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr

 
-T6018failclosed2.hs:11:5:
-    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’
-      PClosed 'Z m = m
-    In the equations for closed type family ‘PClosed’
-    In the type family declaration for ‘PClosed’
-
-T6018failclosed2.hs:11:5:
-    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’
-
+T6018failclosed2.hs:17:14:
+    Couldn't match expected type ‘Bar a0’ with actual type ‘Char’
+    The type variable ‘a0’ is ambiguous
+    In the first argument of ‘bar’, namely ‘'c'’
+    In the expression: bar 'c'
+    In an equation for ‘barapp’: barapp = bar 'c'

testsuite/tests/typecheck/should_fail/T6018failclosed3.hs

-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
-
-module T6018failclosed3 where
-
--- this is not injective - not all injective type variables mentioned
--- on LHS are mentioned on RHS
-type family JClosed a b c = r | r -> a b where
-    JClosed Int b c = Char

testsuite/tests/typecheck/should_fail/T6018failclosed3.stderr

-
-T6018failclosed3.hs:8:5:
-    Type family equation violates injectivity annotation.
-    Injective type variable ‘b’ does not appear on injective position.
-    In the RHS of type family equation:
-      JClosed Int b c = Char
-    In the equations for closed type family ‘JClosed’
-    In the type family declaration for ‘JClosed’

testsuite/tests/typecheck/should_fail/T6018failclosed4.hs

-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
-
-module T6018failclosed4 where
-
-data N = Z | S N
-
--- this is not injective - not all injective type variables mentioned
--- on LHS are mentioned on RHS (tyvar is now nested inside a tycon)
-type family KClosed (a :: N) (b :: N) = (r :: N) | r -> a b where
-    KClosed (S n) m = S m

testsuite/tests/typecheck/should_fail/T6018failclosed4.stderr

-
-T6018failclosed4.hs:10:5:
-    Type family equation violates injectivity annotation.
-    Injective type variable ‘n’ does not appear on injective position.
-    In the RHS of type family equation:
-      KClosed ('S n) m = 'S m
-    In the equations for closed type family ‘KClosed’
-    In the type family declaration for ‘KClosed’

testsuite/tests/typecheck/should_fail/T6018failclosed5.hs

-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
-
-module T6018failclosed5 where
-
--- Id is injective...
-type family IdClosed a = result | result -> a where
-    IdClosed a = a
-
--- hiding a type family application behind a type synonym should be rejected
-type MaybeSynClosed a = IdClosed a
-type family LClosed a = r | r -> a where
- LClosed a = MaybeSynClosed a

testsuite/tests/typecheck/should_fail/T6018failclosed5.stderr

-
-T6018failclosed5.hs:12:2:
-    Type family equation violates injectivity annotation.
-    RHS of injective type family equation cannot be a type family:
-      LClosed a = MaybeSynClosed a
-    In the equations for closed type family ‘LClosed’
-    In the type family declaration for ‘LClosed’
-

testsuite/tests/typecheck/should_fail/T6018failclosed6.hs

-{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
-
-module T6018failclosed6 where
-
--- This should fail because there is no way to determine a, b and k from the RHS
-type family Gc (a :: k) (b :: k) = r | r -> a b where
-    Gc a b = Int

testsuite/tests/typecheck/should_fail/T6018failclosed6.stderr

-
-T6018failclosed6.hs:7:5:
-    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
-    In the equations for closed type family ‘Gc’
-    In the type family declaration for ‘Gc’

testsuite/tests/typecheck/should_fail/T6018failclosed7.hs

-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
-
-module T6018failclosed7 where
-
-type family FClosed a b c = (result :: *) | result -> a b c where
-    FClosed Int  Char Bool = Bool
-    FClosed Char Bool Int  = Int
-    FClosed Bool Int  Char = Int

testsuite/tests/typecheck/should_fail/T6018failclosed7.stderr

-
-T6018failclosed7.hs:7:5:
-    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’

testsuite/tests/typecheck/should_fail/T6018failclosed8.hs

-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
-
-module T6018failclosed8 where
-
-type family IClosed a b c = r | r -> a b where
-    IClosed Int  Char Bool = Bool
-    IClosed Int  Int  Int  = Bool
-    IClosed Bool Int  Int  = Int

testsuite/tests/typecheck/should_fail/T6018failclosed8.stderr

-
-T6018failclosed8.hs:6:5:
-    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’

testsuite/tests/typecheck/should_fail/T6018failclosed9.hs

-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
-
-module T6018failclosed9 where
-
-type family E2 (a :: Bool) = r | r -> a where
-  E2 False = True
-  E2 True  = False
-  E2 a     = False

testsuite/tests/typecheck/should_fail/T6018failclosed9.stderr

-
-T6018failclosed9.hs:8:3:
-    Type family equation violates injectivity annotation.
-    Injective type variable ‘a’ does not appear on injective position.
-    In the RHS of type family equation:
-      E2 a = 'False
-    In the equations for closed type family ‘E2’
-    In the type family declaration for ‘E2’

testsuite/tests/typecheck/should_fail/all.T

@@ -283,18 +283,8 @@ test('T6018fail', extra_clean([ 'T6018fail.hi' , 'T6018fail.o'
                               , 'T6018Cfail.hi', 'T6018Cfail.o'
                               , 'T6018Dfail.hi', 'T6018Dfail.o'])
     , multimod_compile_fail, ['T6018fail', '-no-hs-main -c'])
-test('T6018failclosed1', normal, compile_fail, [''])
+test('T6018failclosed', normal, compile_fail, [''])
 test('T6018failclosed2', normal, compile_fail, [''])
-test('T6018failclosed3', normal, compile_fail, [''])
-test('T6018failclosed4', normal, compile_fail, [''])
-test('T6018failclosed5', normal, compile_fail, [''])
-test('T6018failclosed6', normal, compile_fail, [''])
-test('T6018failclosed7', normal, compile_fail, [''])
-test('T6018failclosed8', normal, compile_fail, [''])
-test('T6018failclosed9', normal, compile_fail, [''])
-test('T6018failclosed10', normal, compile_fail, [''])
-test('T6018failclosed11', normal, compile_fail, [''])
-test('T6018failclosed12', normal, compile_fail, [''])
 test('T6078', normal, compile_fail, [''])
 test('FDsFromGivens', normal, compile_fail, [''])
 test('FDsFromGivens2', normal, compile_fail, [''])