diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed.hs
new file mode 100644
index 0000000000000000000000000000000000000000..a69c63f7e5c173ffd66ab04ff28b68978f1328b6
 /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.hs
@@ 0,0 +1,66 @@
+{# 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
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..452022d6ed8991027113686452ab20ee636458e4
 /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
@@ 0,0 +1,84 @@
+
+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’
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed1.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed1.hs
deleted file mode 100644
index c650781847a2c4f1b21c2bfd58342d5f630fb61e..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed1.hs
+++ /dev/null
@@ 1,11 +0,0 @@
{# 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
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed1.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed1.stderr
deleted file mode 100644
index 968e9e797b512502cae6496b5f4caf788b7e85c5..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed1.stderr
+++ /dev/null
@@ 1,7 +0,0 @@

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’
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed10.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed10.hs
deleted file mode 100644
index 99828c68091a570332e0c125f588a48a9f66d339..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed10.hs
+++ /dev/null
@@ 1,17 +0,0 @@
{# 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'
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed10.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed10.stderr
deleted file mode 100644
index 6248f97a47da4da40fb79fcee5e8a6c6e351c9d0..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed10.stderr
+++ /dev/null
@@ 1,9 +0,0 @@

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'


diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed11.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed11.hs
deleted file mode 100644
index 566551cfefa26a58ad69e30099abaf4b0274aad7..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed11.hs
+++ /dev/null
@@ 1,15 +0,0 @@
{# 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)
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed11.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed11.stderr
deleted file mode 100644
index 7c7496b819a163a7b626aa981f49b3ba822a1da3..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed11.stderr
+++ /dev/null
@@ 1,7 +0,0 @@

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’
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed12.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed12.hs
deleted file mode 100644
index 9ff9a396a0c039d6ecb21c27d2fb4f89ce4190ef..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed12.hs
+++ /dev/null
@@ 1,7 +0,0 @@
{# 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
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed12.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed12.stderr
deleted file mode 100644
index 2ad07aa2a4a710283cf9e9118519183c550ba88b..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed12.stderr
+++ /dev/null
@@ 1,8 +0,0 @@

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’
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed2.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed2.hs
index 44abb06b16d039522a299a3fe315210469ba3326..d90b9decfc0fbac78863fd0e61f2ef72d6f0020c 100644
 a/testsuite/tests/typecheck/should_fail/T6018failclosed2.hs
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed2.hs
@@ 1,12 +1,17 @@
{# 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'
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
index 11ece3d7f520bddd9da8448d999ed429a1118892..3b203968f07d4fa4742138e2313c2386b4b6dea3 100644
 a/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
@@ 1,16 +1,7 @@
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'
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed3.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed3.hs
deleted file mode 100644
index e43ee75e1f92cde199b8cf83d8cf2d18cc0faa05..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed3.hs
+++ /dev/null
@@ 1,8 +0,0 @@
{# 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
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed3.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed3.stderr
deleted file mode 100644
index 968dd76323611c285ebca546d98b16fba27af799..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed3.stderr
+++ /dev/null
@@ 1,8 +0,0 @@

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’
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed4.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed4.hs
deleted file mode 100644
index 116a9c6df494fa9daeb4f082a8b3a55cdcae7ca8..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed4.hs
+++ /dev/null
@@ 1,10 +0,0 @@
{# 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
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed4.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed4.stderr
deleted file mode 100644
index 5db55db602f96d86ed53d7df644f41bb1b3000f9..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed4.stderr
+++ /dev/null
@@ 1,8 +0,0 @@

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’
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed5.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed5.hs
deleted file mode 100644
index 9665365a2f67286c1c81e6fde782432a30ae1b9a..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed5.hs
+++ /dev/null
@@ 1,12 +0,0 @@
{# 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
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed5.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed5.stderr
deleted file mode 100644
index 57ab357bc26a132390d610869bc5e866a7937b55..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed5.stderr
+++ /dev/null
@@ 1,8 +0,0 @@

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’

diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed6.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed6.hs
deleted file mode 100644
index ef55b558e1d06ee2aa210754ae118f6804b11105..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed6.hs
+++ /dev/null
@@ 1,7 +0,0 @@
{# 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
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed6.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed6.stderr
deleted file mode 100644
index be8a763ad4bddf2be6db5c4aa42ae67a7de85056..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed6.stderr
+++ /dev/null
@@ 1,9 +0,0 @@

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’
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed7.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed7.hs
deleted file mode 100644
index a82c323509208b12a68330898d96dc63fb598a3e..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed7.hs
+++ /dev/null
@@ 1,8 +0,0 @@
{# 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
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed7.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed7.stderr
deleted file mode 100644
index 6cdfed528a62a8a676da5539bfaaeba393c77919..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed7.stderr
+++ /dev/null
@@ 1,7 +0,0 @@

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’
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed8.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed8.hs
deleted file mode 100644
index 8936427547c9dce1402aa9aae15d30322449a1f5..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed8.hs
+++ /dev/null
@@ 1,8 +0,0 @@
{# 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
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed8.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed8.stderr
deleted file mode 100644
index 046eed78305b744cb672255f118f33906b54b48e..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed8.stderr
+++ /dev/null
@@ 1,7 +0,0 @@

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’
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed9.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed9.hs
deleted file mode 100644
index 5ec59066b22d75ebecb06728947824d101bae3ad..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed9.hs
+++ /dev/null
@@ 1,8 +0,0 @@
{# 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
diff git a/testsuite/tests/typecheck/should_fail/T6018failclosed9.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed9.stderr
deleted file mode 100644
index 325d9c03eda12ba0edb37bb5772a71a623632f7a..0000000000000000000000000000000000000000
 a/testsuite/tests/typecheck/should_fail/T6018failclosed9.stderr
+++ /dev/null
@@ 1,8 +0,0 @@

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’
diff git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 31646d6f94c902ac3a5c6a6479638fd48d8cde1d..0a0281a587d2c6cf9dbb08c50c0fe10dde99eaf9 100644
 a/testsuite/tests/typecheck/should_fail/all.T
+++ b/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', 'nohsmain 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, [''])