Injective type families

For details see #6018, Phab:D202 and the wiki page:

https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies

This patch also wires-in Maybe data type and updates haddock submodule.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Subscribers: mpickering, bgamari, alanz, thomie, goldfire, simonmar,
             carter

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

GHC Trac Issues: #6018

71 files changed, 1504 insertions, 45 deletions

diff --git a/testsuite/tests/ghci.debugger/scripts/print019.stderr b/testsuite/tests/ghci.debugger/scripts/print019.stderr
index 39bc29fae9..5c1822456e 100644
--- a/testsuite/tests/ghci.debugger/scripts/print019.stderr
+++ b/testsuite/tests/ghci.debugger/scripts/print019.stderr
@@ -7,7 +7,7 @@
     Potential instances:
       instance Show TyCon -- Defined in ‘Data.Typeable.Internal’
       instance Show TypeRep -- Defined in ‘Data.Typeable.Internal’
-      instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
+      instance Show Ordering -- Defined in ‘GHC.Show’
       ...plus 30 others
       (use -fprint-potential-instances to see them all)
     In a stmt of an interactive GHCi command: print it
diff --git a/testsuite/tests/ghci/scripts/T6018ghci.script b/testsuite/tests/ghci/scripts/T6018ghci.script
new file mode 100644
index 0000000000..4615be2d04
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghci.script
@@ -0,0 +1,22 @@
+:set -XTypeFamilies
+:set -XDataKinds
+:set -XUndecidableInstances
+:set -XPolyKinds
+
+type family F a b c = (result :: k) | result -> a b c
+type instance F Int  Char Bool = Bool
+type instance F Char Bool Int  = Int
+type instance F Bool Int  Char = Char
+type instance F Bool Int  Char = Char
+
+type family I (a :: k) b (c :: k) = r | r -> a b
+type instance I Int  Char Bool = Bool
+type instance I Int  Char Int  = Bool
+type instance I Bool Int  Int  = Int
+
+type family J a (b :: k) = r | r -> a
+type instance J Int b = Char
+
+type MaybeSyn a = Maybe a
+type family K a = r | r -> a
+type instance K a = MaybeSyn a
diff --git a/testsuite/tests/ghci/scripts/T6018ghci.stdout b/testsuite/tests/ghci/scripts/T6018ghci.stdout
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghci.stdout
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.script b/testsuite/tests/ghci/scripts/T6018ghcifail.script
new file mode 100644
index 0000000000..c0e073457f
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.script
@@ -0,0 +1,114 @@
+:set -XTypeFamilies
+:set -XDataKinds
+:set -XUndecidableInstances
+:set -XPolyKinds
+
+
+
+type family F a b c = (result :: *) | result -> a b c
+type instance F Int  Char Bool = Bool
+type instance F Char Bool Int  = Int
+type instance F Bool Int  Char = Int
+
+
+
+type family I a b c = r | r -> a b
+type instance I Int  Char Bool = Bool
+type instance I Int  Int  Int  = Bool
+type instance I Bool Int  Int  = Int
+
+-- Id is injective...
+type family Id a = result | result -> a
+type instance Id a = a
+
+-- ...but despite that we disallow a call to Id
+type family IdProxy a = r | r -> a
+type instance IdProxy a = Id a
+
+data N = Z | S N
+
+-- P 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 P (a :: N) (b :: N) = (r :: N) | r -> a b
+type instance P  Z    m = m
+type instance P (S n) m = S (P n m)
+
+-- this is not injective - not all injective type variables mentioned
+-- on LHS are mentioned on RHS
+type family J a b c = r | r -> a b
+type instance J Int b c = Char
+
+-- same as above, but tyvar is now nested inside a tycon
+type family K (a :: N) (b :: N) = (r :: N) | r -> a b
+type instance K (S n) m = S m
+
+-- Make sure we look through type synonyms to catch errors
+type MaybeSyn a = Id a
+type family L a = r | r -> a
+type instance L a = MaybeSyn a
+
+-- These should fail because given the RHS kind there is no way to determine LHS
+-- kind
+class PolyKindVarsC a where { type PolyKindVarsF a = (r :: k) | r -> a }
+
+instance PolyKindVarsC '[] where { type PolyKindVarsF '[] = '[] }
+
+
+
+type family PolyKindVars (a :: k0) = (r :: k1) | r -> a
+type instance PolyKindVars '[] = '[]
+
+-- This should fail because there is no way to determine k from the RHS
+type family Fc (a :: k) (b :: k) = r | r -> k
+type instance Fc a b = Int
+
+-- 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
+type instance Gc a b = Int
+
+type family GF1 a = r | r -> a
+type instance GF1 Int = Bool
+
+type family GF2 a = r | r -> a
+type instance GF2 Int = Bool
+
+type family HF1 a
+type instance HF1 Bool = Bool
+
+-- fails because injectivity is not compositional in this case
+type family F1 a = r | r -> a
+type instance F1 [a]       = Maybe (GF1 a)
+type instance F1 (Maybe a) = Maybe (GF2 a)
+
+type family W1 a = r | r -> a
+type instance W1 [a] = a
+
+type family W2 a = r | r -> a
+type instance W2 [a] = W2 a
+
+-- not injective because of infinite types
+type family Z1 a = r | r -> a
+type instance Z1 [a]       = (a, a)
+type instance Z1 (Maybe b) = (b, [b])
+
+type family G1 a = r | r -> a
+type instance G1 [a]       = [a]
+type instance G1 (Maybe b) = [(b, b)]
+
+type family G3 a b = r | r -> b
+type instance G3 a Int  = (a, Int)
+type instance G3 a Bool = (Bool, a)
+
+type family G4 a b = r | r -> a b
+type instance G4 a b = [a]
+
+type family G5 a = r | r -> a
+type instance G5 [a] = [GF1 a] -- GF1 injective
+type instance G5 Int = [Bool]
+
+type family G6 a = r | r -> a
+type instance G6 [a]  = [HF1 a] -- HF1 not injective
+type instance G6 Bool = Int
+
+
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
new file mode 100644
index 0000000000..e1c0055349
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -0,0 +1,111 @@
+
+<interactive>:10:15:
+    Type family equations violate injectivity annotation:
+      F Char Bool Int = Int
+      F Bool Int Char = Int
+
+<interactive>:16:15:
+    Type family equations violate injectivity annotation:
+      I Int Char Bool = Bool
+      I Int Int Int = Bool
+
+<interactive>:26:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      IdProxy a = Id a
+
+<interactive>:34:15:
+    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’
+      P 'Z m = m
+
+<interactive>:40:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘b’ does not appear on injective position.
+    In the RHS of type family equation:
+      J Int b c = Char
+
+<interactive>:44:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘n’ does not appear on injective position.
+    In the RHS of type family equation:
+      K ('S n) m = 'S m
+
+<interactive>:49:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      L a = MaybeSyn a
+
+<interactive>:55:41:
+    Type family equation violates injectivity annotation.
+    Injective kind variable ‘k1’ is not inferable from the RHS type variables.
+    In the RHS of type family equation:
+      PolyKindVarsF '[] = '[]
+
+<interactive>:60:15:
+    Type family equation violates injectivity annotation.
+    Injective kind variable ‘k1’ is not inferable from the RHS type variables.
+    In the RHS of type family equation:
+      PolyKindVars '[] = '[]
+
+<interactive>:64:15:
+    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). Fc a b = Int
+
+<interactive>:68:15:
+    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
+
+<interactive>:81:15:
+    Type family equations violate injectivity annotation:
+      F1 [a] = Maybe (GF1 a)
+      F1 (Maybe a) = Maybe (GF2 a)
+
+<interactive>:85:15:
+    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: ‘[a]’
+      W1 [a] = a
+
+<interactive>:88:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      W2 [a] = W2 a
+
+<interactive>:92:15:
+    Type family equations violate injectivity annotation:
+      Z1 [a] = (a, a)
+      Z1 (Maybe b) = (b, [b])
+
+<interactive>:96:15:
+    Type family equations violate injectivity annotation:
+      G1 [a] = [a]
+      G1 (Maybe b) = [(b, b)]
+
+<interactive>:100:15:
+    Type family equations violate injectivity annotation:
+      G3 a Int = (a, Int)
+      G3 a Bool = (Bool, a)
+
+<interactive>:104:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘b’ does not appear on injective position.
+    In the RHS of type family equation:
+      G4 a b = [a]
+
+<interactive>:107:15:
+    Type family equations violate injectivity annotation:
+      G5 [a] = [GF1 a]
+      G5 Int = [Bool]
+
+<interactive>:111:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘a’ does not appear on injective position.
+    In the RHS of type family equation:
+      G6 [a] = [HF1 a]
diff --git a/testsuite/tests/ghci/scripts/T6018ghcirnfail.script b/testsuite/tests/ghci/scripts/T6018ghcirnfail.script
new file mode 100644
index 0000000000..f1a5fa469a
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghcirnfail.script
@@ -0,0 +1,42 @@
+:set -XTypeFamilies
+:set -XDataKinds
+:set -XUndecidableInstances
+:set -XPolyKinds
+:set -XMultiParamTypeClasses
+
+-- IA = injectivity annotation `| foo -> bar`
+
+-- use incorrect tyvar in LHS of IA
+type family F a = r | a -> a
+type family Fc a = r | a -> a where { Fc a = a }
+class Fcl a where { type Ft a = r | a -> a }
+
+-- declare result tyvar to be duplicate (without IA)
+type family G a = a
+type family Gc a = a where { Gc a = a }
+
+-- declare result tyvar to be duplicate (with IA)
+type family Gb a = a | a -> a
+type family Gcb a = a | a -> a where { Gcb a = a }
+class Gclb a where { type Gtb a = a | a -> a } -- here we want two errors
+
+-- not in-scope tyvar in RHS of IA
+type family I a b = r | r -> c
+type family Ic a b = r | r -> c where { Ic a b = a }
+class Icl a b where { type It a b = r | r -> c }
+
+-- repeated tyvar on RHS of IA
+type family J a b = r | r -> a a
+type family Jc a b = r | r -> a a where { Jc a b = a }
+class Jcl a b where { type Jt a b = r | r -> a a }
+
+-- not in-scope tyvar in LHS of IA
+type family L a b = r | c -> a
+type family Lc a b = r | c -> a where { Lc a b = a }
+class Lcl a b where { type Lt a b = r | c -> a }
+
+-- result variable shadows variable in class head
+class M a b where { type Mt b = a | a -> b }
+
+-- here b is out-of-scope
+class N a b where { type Nt a = r | r -> a b }
diff --git a/testsuite/tests/ghci/scripts/T6018ghcirnfail.stderr b/testsuite/tests/ghci/scripts/T6018ghcirnfail.stderr
new file mode 100644
index 0000000000..87f5a040b1
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghcirnfail.stderr
@@ -0,0 +1,63 @@
+
+<interactive>:10:23:
+    Incorrect type variable on the LHS of injectivity condition
+         Expected : r
+         Actual   : a
+
+<interactive>:11:24:
+    Incorrect type variable on the LHS of injectivity condition
+         Expected : r
+         Actual   : a
+
+<interactive>:12:37:
+    Incorrect type variable on the LHS of injectivity condition
+         Expected : r
+         Actual   : a
+
+<interactive>:15:19:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:16:20:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:19:20:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:19:24:
+    Unknown type variable on the RHS of injectivity condition: a
+
+<interactive>:20:21:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:20:25:
+    Unknown type variable on the RHS of injectivity condition: a
+
+<interactive>:21:35:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:21:39:
+    Unknown type variable on the RHS of injectivity condition: a
+
+<interactive>:24:1: Not in scope: type variable ‘c’
+
+<interactive>:25:1: Not in scope: type variable ‘c’
+
+<interactive>:26:23: Not in scope: type variable ‘c’
+
+<interactive>:34:1: Not in scope: type variable ‘c’
+
+<interactive>:35:1: Not in scope: type variable ‘c’
+
+<interactive>:36:23: Not in scope: type variable ‘c’
+
+<interactive>:39:33:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:42:37:
+    Unknown type variable on the RHS of injectivity condition: b
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index bbd69ee014..d2244c1790 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -161,6 +161,9 @@ test('T7627', normal, ghci_script, ['T7627.script'])
 test('T7627b', normal, ghci_script, ['T7627b.script'])
 test('T7586', normal, ghci_script, ['T7586.script'])
 test('T4175', normal, ghci_script, ['T4175.script'])
+test('T6018ghci', normal, ghci_script, ['T6018ghci.script'])
+test('T6018ghcifail', normal, ghci_script, ['T6018ghcifail.script'])
+test('T6018ghcirnfail', normal, ghci_script, ['T6018ghcirnfail.script'])
 test('T7730', combined_output, ghci_script, ['T7730.script'])
 test('T7872', normal, ghci_script, ['T7872.script'])
 test('T7873', normal, ghci_script, ['T7873.script'])
diff --git a/testsuite/tests/indexed-types/should_compile/T9085.stderr b/testsuite/tests/indexed-types/should_compile/T9085.stderr
index ee968e0d79..8a4ebdbb7a 100644
--- a/testsuite/tests/indexed-types/should_compile/T9085.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T9085.stderr
@@ -1,4 +1,4 @@
 
 T9085.hs:7:3: Warning:
-    Overlapped type family instance equation:
+    Type family instance equation is overlapped:
       F Bool = Bool
diff --git a/testsuite/tests/indexed-types/should_fail/T9160.hs b/testsuite/tests/indexed-types/should_fail/T9160.hs
index 64ae3b9f9c..7daa6b815d 100644
--- a/testsuite/tests/indexed-types/should_fail/T9160.hs
+++ b/testsuite/tests/indexed-types/should_fail/T9160.hs
@@ -8,7 +8,7 @@ $( do { cls_nm <- newName "C"
       ; k_nm   <- newName "k"
       ; f_nm   <- newName "F"
       ; return [ClassD [] cls_nm [KindedTV a_nm (VarT k_nm)] []
-                    [FamilyD TypeFam f_nm [] (Just (VarT k_nm))]] } )
+                   [OpenTypeFamilyD f_nm [] (KindSig (VarT k_nm)) Nothing ]] } )
 
 -- Splices in:
 --     class C (a :: k) where
@@ -16,4 +16,3 @@ $( do { cls_nm <- newName "C"
 
 instance C (a :: *) where
   type F = Maybe   -- Should be illegal
-
diff --git a/testsuite/tests/overloadedlists/should_fail/overloadedlistsfail01.stderr b/testsuite/tests/overloadedlists/should_fail/overloadedlistsfail01.stderr
index 79b78658b3..75abc3b0e6 100644
--- a/testsuite/tests/overloadedlists/should_fail/overloadedlistsfail01.stderr
+++ b/testsuite/tests/overloadedlists/should_fail/overloadedlistsfail01.stderr
@@ -4,8 +4,8 @@ overloadedlistsfail01.hs:5:8: error:
     The type variable ‘a0’ is ambiguous
     Potential instances:
       instance [safe] Show Version -- Defined in ‘Data.Version’
-      instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
       instance Show Ordering -- Defined in ‘GHC.Show’
+      instance Show Integer -- Defined in ‘GHC.Show’
       ...plus 23 others
       (use -fprint-potential-instances to see them all)
     In the expression: print [1]
diff --git a/testsuite/tests/quotes/TH_localname.stderr b/testsuite/tests/quotes/TH_localname.stderr
index 76bfeea8a2..c764f576ef 100644
--- a/testsuite/tests/quotes/TH_localname.stderr
+++ b/testsuite/tests/quotes/TH_localname.stderr
@@ -8,9 +8,8 @@ TH_localname.hs:3:11: error:
     Potential instances:
       instance (Lift a, Lift b) => Lift (Either a b)
         -- Defined in ‘Language.Haskell.TH.Syntax’
-      instance Lift a => Lift (Maybe a)
-        -- Defined in ‘Language.Haskell.TH.Syntax’
       instance Lift Int16 -- Defined in ‘Language.Haskell.TH.Syntax’
+      instance Lift Int32 -- Defined in ‘Language.Haskell.TH.Syntax’
       ...plus 24 others
       (use -fprint-potential-instances to see them all)
     In the expression: lift y
diff --git a/testsuite/tests/rename/should_fail/T6018rnfail.hs b/testsuite/tests/rename/should_fail/T6018rnfail.hs
new file mode 100644
index 0000000000..14d1929ed2
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T6018rnfail.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE TypeFamilies, PolyKinds #-}
+
+module T6018rnfail where
+
+-- IA = injectivity annotation `| foo -> bar`
+
+-- use incorrect tyvar in LHS of IA
+type family F a = r | a -> a
+type family Fc a = r | a -> a where
+  Fc a = a
+class Fcl a where
+  type Ft a = r | a -> a
+
+-- declare result tyvar to be duplicate (without IA)
+type family G a = a
+type family Gc a = a where
+  Gc a = a
+
+-- declare result tyvar to be duplicate (with IA)
+type family Gb a = a | a -> a
+type family Gcb a = a | a -> a where
+  Gcb a = a
+class Gclb a where -- here we want two errors
+  type Gtb a = a | a -> a
+
+-- not in-scope tyvar in RHS of IA
+type family I a b = r | r -> c
+type family Ic a b = r | r -> c where
+  Ic a b = a
+class Icl a b where
+  type It a b = r | r -> c
+
+-- not in-scope tyvar in LHS of IA
+type family L a b = r | c -> a
+type family Lc a b = r | c -> a where
+  Lc a b = a
+class Lcl a b where
+  type Lt a b = r | c -> a
+
+-- result variable shadows variable in class head
+class M a b where
+  type Mt b = a | a -> b
+
+-- here b is out-of-scope
+class N a b where
+  type Nt a = r | r -> a b
+
+-- result is out of scope. Not possible for associated types
+type family O1  a | r -> a
+type family Oc1 a | r -> a where
+    Oc1 a = a
+type family O2  a :: * | r -> a
+type family Oc2 a :: * | r -> a where
+    Oc2 a = a
diff --git a/testsuite/tests/rename/should_fail/T6018rnfail.stderr b/testsuite/tests/rename/should_fail/T6018rnfail.stderr
new file mode 100644
index 0000000000..2628024b83
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T6018rnfail.stderr
@@ -0,0 +1,71 @@
+
+T6018rnfail.hs:8:23:
+    Incorrect type variable on the LHS of injectivity condition
+         Expected : r
+         Actual   : a
+
+T6018rnfail.hs:9:24:
+    Incorrect type variable on the LHS of injectivity condition
+         Expected : r
+         Actual   : a
+
+T6018rnfail.hs:12:19:
+    Incorrect type variable on the LHS of injectivity condition
+         Expected : r
+         Actual   : a
+
+T6018rnfail.hs:15:19:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+T6018rnfail.hs:16:20:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+T6018rnfail.hs:20:20:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+T6018rnfail.hs:20:24:
+    Unknown type variable on the RHS of injectivity condition: a
+
+T6018rnfail.hs:21:21:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+T6018rnfail.hs:21:25:
+    Unknown type variable on the RHS of injectivity condition: a
+
+T6018rnfail.hs:24:16:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+T6018rnfail.hs:24:20:
+    Unknown type variable on the RHS of injectivity condition: a
+
+T6018rnfail.hs:27:1: Not in scope: type variable ‘c’
+
+T6018rnfail.hs:28:1: Not in scope: type variable ‘c’
+
+T6018rnfail.hs:31:3: Not in scope: type variable ‘c’
+
+T6018rnfail.hs:34:1: Not in scope: type variable ‘c’
+
+T6018rnfail.hs:35:1: Not in scope: type variable ‘c’
+
+T6018rnfail.hs:38:3: Not in scope: type variable ‘c’
+
+T6018rnfail.hs:42:15:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+T6018rnfail.hs:46:19:
+    Unknown type variable on the RHS of injectivity condition: b
+
+T6018rnfail.hs:49:21: Not in scope: type variable ‘r’
+
+T6018rnfail.hs:50:21: Not in scope: type variable ‘r’
+
+T6018rnfail.hs:52:26: Not in scope: type variable ‘r’
+
+T6018rnfail.hs:53:26: Not in scope: type variable ‘r’
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index 23648c93c8..bd717dd8d5 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -101,6 +101,7 @@ test('T5745',
 test('T5892a', normal, compile_fail, ['-package containers'])
 test('T5892b', normal, compile_fail, ['-package containers'])
 test('T5951', normal, compile_fail, [''])
+test('T6018rnfail', normal, compile_fail, [''])
 test('T6060', normal, compile_fail, [''])
 test('T6148', normal, compile_fail, [''])
 test('T7164', normal, compile_fail, [''])
diff --git a/testsuite/tests/rename/should_fail/mc14.stderr b/testsuite/tests/rename/should_fail/mc14.stderr
index 3f52be33c6..bb02f9bafb 100644
--- a/testsuite/tests/rename/should_fail/mc14.stderr
+++ b/testsuite/tests/rename/should_fail/mc14.stderr
@@ -1,10 +1,9 @@
-
 mc14.hs:14:16: error:
     No instance for (Functor t0) arising from a use of ‘fmap’
     The type variable ‘t0’ is ambiguous
     Potential instances:
-      instance Functor Maybe -- Defined in ‘GHC.Base’
       instance Functor IO -- Defined in ‘GHC.Base’
+      instance Functor Maybe -- Defined in ‘GHC.Base’
       instance Functor ((->) r) -- Defined in ‘GHC.Base’
       ...plus two others
       (use -fprint-potential-instances to see them all)
diff --git a/testsuite/tests/th/ClosedFam2TH.hs b/testsuite/tests/th/ClosedFam2TH.hs
index cd2dc2de60..bb355a2790 100644
--- a/testsuite/tests/th/ClosedFam2TH.hs
+++ b/testsuite/tests/th/ClosedFam2TH.hs
@@ -4,16 +4,18 @@ module ClosedFam2 where
 
 import Language.Haskell.TH
 
-$( return [ ClosedTypeFamilyD (mkName "Equals")
-                              [ KindedTV (mkName "a") (VarT (mkName "k"))
-                              , KindedTV (mkName "b") (VarT (mkName "k")) ]
-                              Nothing
-                              [ TySynEqn [ (VarT (mkName "a"))
-                                         , (VarT (mkName "a")) ]
-                                         (ConT (mkName "Int"))
-                              , TySynEqn [ (VarT (mkName "a"))
-                                         , (VarT (mkName "b")) ]
-                                         (ConT (mkName "Bool")) ] ])
+$( return [ ClosedTypeFamilyD
+              (mkName "Equals")
+              [ KindedTV (mkName "a") (VarT (mkName "k"))
+              , KindedTV (mkName "b") (VarT (mkName "k")) ]
+              ( TyVarSig (KindedTV (mkName "r") (VarT (mkName "k"))))
+              Nothing
+              [ TySynEqn [ (VarT (mkName "a"))
+                         , (VarT (mkName "a")) ]
+                         (ConT (mkName "Int"))
+              , TySynEqn [ (VarT (mkName "a"))
+                         , (VarT (mkName "b")) ]
+                         (ConT (mkName "Bool")) ] ])
 
 a :: Equals b b
 a = (5 :: Int)
diff --git a/testsuite/tests/th/T10306.hs b/testsuite/tests/th/T10306.hs
index b93114b61c..b74eb591e9 100644
--- a/testsuite/tests/th/T10306.hs
+++ b/testsuite/tests/th/T10306.hs
@@ -9,6 +9,6 @@ import GHC.TypeLits
 -- caused a crash, because it has no equations
 $(do x <- reify ''(+)
      case x of
-       FamilyI (ClosedTypeFamilyD _ _ _ []) _ -> return []
-       _                                      -> error $ show x
+       FamilyI (ClosedTypeFamilyD _ _ _ _ []) _ -> return []
+       _                                        -> error $ show x
  )
diff --git a/testsuite/tests/th/T6018th.hs b/testsuite/tests/th/T6018th.hs
new file mode 100644
index 0000000000..32053636e2
--- /dev/null
+++ b/testsuite/tests/th/T6018th.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances, PolyKinds #-}
+
+module T6018th where
+
+import Language.Haskell.TH
+
+-- Test that injectivity works correct with TH. This test is not as exhaustive
+-- as the original T6018 test.
+
+-- type family F a b c = (result :: k) | result -> a b c
+-- type instance F Int  Char Bool = Bool
+-- type instance F Char Bool Int  = Int
+-- type instance F Bool Int  Char = Char
+$( return
+   [ OpenTypeFamilyD
+       (mkName "F")
+       [ PlainTV (mkName "a"), PlainTV (mkName "b"), PlainTV (mkName "c") ]
+       (TyVarSig (KindedTV (mkName "result") (VarT (mkName "k"))))
+       (Just $ InjectivityAnn (mkName "result")
+                             [(mkName "a"), (mkName "b"), (mkName "c") ])
+   , TySynInstD
+       (mkName "F")
+       (TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
+                 , ConT (mkName "Bool")]
+                 ( ConT (mkName "Bool")))
+   , TySynInstD
+       (mkName "F")
+       (TySynEqn [ ConT (mkName "Char"), ConT (mkName "Bool")
+                 , ConT (mkName "Int")]
+                 ( ConT (mkName "Int")))
+   , TySynInstD
+       (mkName "F")
+       (TySynEqn [ ConT (mkName "Bool"), ConT (mkName "Int")
+                 , ConT (mkName "Char")]
+                 ( ConT (mkName "Char")))
+   ] )
+
+-- this is injective - a type variables mentioned on LHS is not mentioned on RHS
+-- but we don't claim injectivity in that argument.
+--
+-- type family J a (b :: k) = r | r -> a
+---type instance J Int b = Char
+$( return
+   [ OpenTypeFamilyD
+       (mkName "J")
+       [ PlainTV (mkName "a"), KindedTV (mkName "b") (VarT (mkName "k")) ]
+       (TyVarSig (PlainTV (mkName "r")))
+       (Just $ InjectivityAnn (mkName "r") [mkName "a"])
+   , TySynInstD
+       (mkName "J")
+       (TySynEqn [ ConT (mkName "Int"), VarT (mkName "b") ]
+                 ( ConT (mkName "Int")))
+   ] )
+
+-- Closed type families
+
+-- type family IClosed (a :: *) (b :: *) (c :: *) = r | r -> a b where
+--     IClosed Int  Char Bool = Bool
+--     IClosed Int  Char Int  = Bool
+--     IClosed Bool Int  Int  = Int
+
+$( return
+   [ ClosedTypeFamilyD
+       (mkName "I")
+       [ KindedTV (mkName "a") StarT, KindedTV (mkName "b") StarT
+       , KindedTV (mkName "c") StarT ]
+       (TyVarSig (PlainTV (mkName "r")))
+       (Just $ InjectivityAnn (mkName "r") [(mkName "a"), (mkName "b")])
+       [ TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
+                  , ConT (mkName "Bool")]
+                  ( ConT (mkName "Bool"))
+       , TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
+                  , ConT (mkName "Int")]
+                  ( ConT (mkName "Bool"))
+       , TySynEqn [ ConT (mkName "Bool"), ConT (mkName "Int")
+                  , ConT (mkName "Int")]
+                  ( ConT (mkName "Int"))
+       ]
+   ] )
+
+-- reification test
+$( do { decl@([ClosedTypeFamilyD _ _ _ (Just inj) _]) <-
+               [d| type family Bak a = r | r -> a where
+                        Bak Int  = Char
+                        Bak Char = Int
+                        Bak a    = a |]
+      ; runIO $ putStrLn (pprint inj)
+      ; return decl
+      }
+ )
+
+-- Check whether incorrect injectivity declarations are caught
+
+-- type family I a b c = r | r -> a b
+-- type instance I Int  Char Bool = Bool
+-- type instance I Int  Int  Int  = Bool
+-- type instance I Bool Int  Int  = Int
+$( return
+   [ OpenTypeFamilyD
+       (mkName "H")
+       [ PlainTV (mkName "a"), PlainTV (mkName "b"), PlainTV (mkName "c") ]
+       (TyVarSig (PlainTV (mkName "r")))
+       (Just $ InjectivityAnn (mkName "r")
+                             [(mkName "a"), (mkName "b") ])
+   , TySynInstD
+       (mkName "H")
+       (TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
+                 , ConT (mkName "Bool")]
+                 ( ConT (mkName "Bool")))
+   , TySynInstD
+       (mkName "H")
+       (TySynEqn [ ConT (mkName "Int"), ConT (mkName "Int")
+                 , ConT (mkName "Int")]
+                 ( ConT (mkName "Bool")))
+   , TySynInstD
+       (mkName "H")
+       (TySynEqn [ ConT (mkName "Bool"), ConT (mkName "Int")
+                 , ConT (mkName "Int")]
+                 ( ConT (mkName "Int")))
+   ] )
diff --git a/testsuite/tests/th/T6018th.stderr b/testsuite/tests/th/T6018th.stderr
new file mode 100644
index 0000000000..98c318b63d
--- /dev/null
+++ b/testsuite/tests/th/T6018th.stderr
@@ -0,0 +1,6 @@
+| r_0 -> a_1
+
+T6018th.hs:98:4:
+    Type family equations violate injectivity annotation:
+      H Int Int Int = Bool
+      H Int Char Bool = Bool
diff --git a/testsuite/tests/th/T8028.hs b/testsuite/tests/th/T8028.hs
index 6145428aaf..c54f0e3dcf 100644
--- a/testsuite/tests/th/T8028.hs
+++ b/testsuite/tests/th/T8028.hs
@@ -12,6 +12,6 @@ $(x)
 -- subsequently be reified
 $(do f <- reify ''F
      case f of
-       FamilyI (ClosedTypeFamilyD _ _ _ []) _ -> return []
-       _                                      -> error $ show f
+       FamilyI (ClosedTypeFamilyD _ _ _ _ []) _ -> return []
+       _                                        -> error $ show f
  )
diff --git a/testsuite/tests/th/T8028a.hs b/testsuite/tests/th/T8028a.hs
index 928a96e52c..7845c13b71 100644
--- a/testsuite/tests/th/T8028a.hs
+++ b/testsuite/tests/th/T8028a.hs
@@ -3,4 +3,4 @@ module T8028a where
 import Language.Haskell.TH
 
 x = do n <- newName "F"
-       return [ClosedTypeFamilyD n [] Nothing []]
+       return [ClosedTypeFamilyD n [] NoSig Nothing []]
diff --git a/testsuite/tests/th/T8884.hs b/testsuite/tests/th/T8884.hs
index ca6ed9c4b1..acbd6208df 100644
--- a/testsuite/tests/th/T8884.hs
+++ b/testsuite/tests/th/T8884.hs
@@ -5,19 +5,20 @@ module T8884 where
 import Language.Haskell.TH
 import System.IO
 
-type family Foo a where
+type family Foo a = r | r -> a where
   Foo x = x
 
-type family Baz (a :: k)
+type family Baz (a :: k) = (r :: k) | r -> a
 type instance Baz x = x
 
-$( do FamilyI foo@(ClosedTypeFamilyD _ tvbs1 m_kind1 eqns1) [] <- reify ''Foo
-      FamilyI baz@(FamilyD TypeFam _ tvbs2 m_kind2)
+$( do FamilyI foo@(ClosedTypeFamilyD _ tvbs1 res1 m_kind1 eqns1)
+              [] <- reify ''Foo
+      FamilyI baz@(OpenTypeFamilyD _ tvbs2 res2 m_kind2)
               [inst@(TySynInstD _ eqn2)] <- reify ''Baz
       runIO $ putStrLn $ pprint foo
       runIO $ putStrLn $ pprint baz
       runIO $ putStrLn $ pprint inst
       runIO $ hFlush stdout
-      return [ ClosedTypeFamilyD (mkName "Foo'") tvbs1 m_kind1 eqns1
-             , FamilyD TypeFam (mkName "Baz'") tvbs2 m_kind2
+      return [ ClosedTypeFamilyD (mkName "Foo'") tvbs1 res1 m_kind1 eqns1
+             , OpenTypeFamilyD   (mkName "Baz'") tvbs2 res2 m_kind2
              , TySynInstD (mkName "Baz'") eqn2 ] )
diff --git a/testsuite/tests/th/T8884.stderr b/testsuite/tests/th/T8884.stderr
index 24fc15a81f..28be29951d 100644
--- a/testsuite/tests/th/T8884.stderr
+++ b/testsuite/tests/th/T8884.stderr
@@ -1,3 +1,4 @@
-type family T8884.Foo (a_0 :: k_1) :: k_1 where T8884.Foo x_2 = x_2
-type family T8884.Baz (a_0 :: k_1) :: *
-type instance T8884.Baz (x_0 :: *) = x_0
+type family T8884.Foo (a_0 :: k_1) = (r_2 :: k_1) | r_2 -> k_1 a_0 where
+    T8884.Foo x_3 = x_3
+type family T8884.Baz (a_0 :: k_1) = (r_2 :: k_1) | r_2 -> k_1 a_0
+type instance T8884.Baz (x_0 :: k_1) = x_0
diff --git a/testsuite/tests/th/TH_RichKinds2.hs b/testsuite/tests/th/TH_RichKinds2.hs
index b804688b6a..c77988c3bc 100644
--- a/testsuite/tests/th/TH_RichKinds2.hs
+++ b/testsuite/tests/th/TH_RichKinds2.hs
@@ -12,13 +12,13 @@ import Data.Char
 import Data.List
 import Language.Haskell.TH
 
-$(return [FamilyD TypeFam (mkName "Map") [KindedTV (mkName "f")
+$(return [OpenTypeFamilyD (mkName "Map") [KindedTV (mkName "f")
                                                    (AppT (AppT ArrowT (VarT (mkName "k1")))
                                                            (VarT (mkName "k2"))),
                                           KindedTV (mkName "l")
                                                    (AppT ListT
                                                          (VarT (mkName "k1")))]
-                                          (Just (AppT ListT (VarT (mkName "k2"))))])
+                                          (KindSig (AppT ListT (VarT (mkName "k2")))) Nothing])
 
 $( let fixKs :: String -> String -- need to remove TH renaming index from k variables
        fixKs s =
diff --git a/testsuite/tests/th/TH_reifyDecl1.hs b/testsuite/tests/th/TH_reifyDecl1.hs
index 7e7c9f40b9..c4ae3c065d 100644
--- a/testsuite/tests/th/TH_reifyDecl1.hs
+++ b/testsuite/tests/th/TH_reifyDecl1.hs
@@ -84,5 +84,3 @@ test = $(let
           ; display ''DF1
           ; display ''DF2
           ; [| () |] })
-
-
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index a43cf57f3d..dada44a325 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -351,3 +351,4 @@ test('T10704',
      extra_clean(['T10704a.o','T10704a.hi']),
      multimod_compile_and_run,
      ['T10704', '-v0'])
+test('T6018th', normal, compile_fail, ['-v0'])
diff --git a/testsuite/tests/typecheck/should_compile/T6018.hs b/testsuite/tests/typecheck/should_compile/T6018.hs
new file mode 100644
index 0000000000..523bc968d0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T6018.hs
@@ -0,0 +1,254 @@
+{-# LANGUAGE DataKinds                 #-}
+{-# LANGUAGE MultiParamTypeClasses     #-}
+{-# LANGUAGE PolyKinds                 #-}
+{-# LANGUAGE TypeFamilies              #-}
+{-# LANGUAGE UndecidableInstances      #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module T6018 where
+
+import T6018a -- defines G, identical to F
+
+type family F a b c = (result :: k) | result -> a b c
+type instance F Int  Char Bool = Bool
+type instance F Char Bool Int  = Int
+type instance F Bool Int  Char = Char
+
+
+type instance G Bool Int  Char = Char
+
+type family I (a :: k) b (c :: k) = r | r -> a b
+type instance I Int  Char Bool = Bool
+type instance I Int  Char Int  = Bool
+type instance I Bool Int  Int  = Int
+
+-- this is injective - a type variable introduced in the LHS is not mentioned on
+-- RHS but we don't claim injectivity in that argument.
+type family J a (b :: k) = r | r -> a
+type instance J Int b = Char
+
+type MaybeSyn a = Maybe a
+newtype MaybeNew a = MaybeNew (Maybe a)
+
+-- make sure we look through type synonyms...
+type family K a = r | r -> a
+type instance K a = MaybeSyn a
+
+-- .. but not newtypes
+type family M a = r | r -> a
+type instance M (Maybe a)    = MaybeSyn a
+type instance M (MaybeNew a) = MaybeNew a
+
+-- Closed type families
+
+-- these are simple conversions from open type families. They should behave the
+-- same
+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 = Char
+
+type family IClosed (a :: *) (b :: *) (c :: *) = r | r -> a b where
+    IClosed Int  Char Bool = Bool
+    IClosed Int  Char Int  = Bool
+    IClosed Bool Int  Int  = Int
+
+type family JClosed a (b :: k) = r | r -> a where
+    JClosed Int b = Char
+
+type family KClosed a = r | r -> a where
+    KClosed a = MaybeSyn a
+
+-- Here the last equation might return both Int and Char but we have to
+-- recognize that it is not possible due to equation overlap
+type family Bak a = r | r -> a where
+     Bak Int  = Char
+     Bak Char = Int
+     Bak a    = a
+
+-- This is similar, except that the last equation contains concrete type.  Since
+-- it is overlapped it should be dropped with a warning
+type family Foo a = r | r -> a where
+    Foo Int  = Bool
+    Foo Bool = Int
+    Foo Bool = Bool
+
+-- this one was tricky in the early implementation of injectivity.  Now it is
+-- identical to the above but we still keep it as a regression test.
+type family Bar a = r | r -> a where
+    Bar Int  = Bool
+    Bar Bool = Int
+    Bar Bool = Char
+
+-- Now let's use declared type families. All the below definitions should work
+
+-- No ambiguity for any of the arguments - all are injective
+f :: F a b c -> F a b c
+f x = x
+
+-- From 1st instance of F: a ~ Int, b ~ Char, c ~ Bool
+fapp :: Bool
+fapp = f True
+
+-- now the closed variant of F
+fc :: FClosed a b c -> FClosed a b c
+fc x = x
+
+fcapp :: Bool
+fcapp = fc True
+
+-- The last argument is not injective so it must be instantiated
+i :: I a b Int -> I a b Int
+i x = x
+
+-- From 1st instance of I: a ~ Int, b ~ Char
+iapp :: Bool
+iapp = i True
+
+-- again, closed variant of I
+ic :: IClosed a b Int -> IClosed a b Int
+ic x = x
+
+icapp :: Bool
+icapp = ic True
+
+-- Now we have to test weird closed type families:
+bak :: Bak a -> Bak a
+bak x = x
+
+bakapp1 :: Char
+bakapp1 = bak 'c'
+
+bakapp2 :: Double
+bakapp2 = bak 1.0
+
+bakapp3 :: ()
+bakapp3 = bak ()
+
+foo :: Foo a -> Foo a
+foo x = x
+
+fooapp1 :: Bool
+fooapp1 = foo True
+
+bar :: Bar a -> Bar a
+bar x = x
+
+barapp1 :: Bool
+barapp1 = bar True
+
+barapp2 :: Int
+barapp2 = bar 1
+
+-- Declarations below test more liberal RHSs of injectivity annotations:
+-- permiting variables to appear in different order than the one in which they
+-- were declared.
+type family H a b = r | r -> b a
+type family Hc a b = r | r -> b a where
+  Hc a b = a b
+class Hcl a b where
+  type Ht a b = r | r -> b a
+
+-- repeated tyvars in the RHS of injectivity annotation: no warnings or errors
+-- (consistent with behaviour for functional dependencies)
+type family Jx a b = r | r -> a a
+type family Jcx a b = r | r -> a a where
+  Jcx a b = a b
+class Jcl a b where
+  type Jt a b = r | r -> a a
+
+type family Kx a b = r | r -> a b b
+type family Kcx a b = r | r -> a b b where
+  Kcx a b = a b
+class Kcl a b where
+  type Kt a b = r | r -> a b b
+
+-- Declaring kind injectivity. Here we only claim that knowing the RHS
+-- determines the LHS kind but not the type.
+type family L (a :: k1) = (r :: k2) | r -> k1 where
+    L 'True  = Int
+    L 'False = Int
+    L Maybe  = 3
+    L IO     = 3
+
+data KProxy (a :: *) = KProxy
+type family KP (kproxy :: KProxy k) = r | r -> k
+type instance KP ('KProxy :: KProxy Bool) = Int
+type instance KP ('KProxy :: KProxy *)    = Char
+
+kproxy_id :: KP ('KProxy :: KProxy k) -> KP ('KProxy :: KProxy k)
+kproxy_id x = x
+
+kproxy_id_use = kproxy_id 'a'
+
+-- Now test some awkward cases from The Injectivity Paper.  All should be
+-- accepted.
+type family Gx a
+type family Hx a
+type family Gi a = r | r -> a
+type instance Gi Int = Char
+type family Hi a = r | r -> a
+
+type family F2 a = r | r -> a
+type instance F2 [a]       = [Gi a]
+type instance F2 (Maybe a) = Hi a -> Int
+
+type family F4 a = r | r -> a
+type instance F4 [a]       = (Gx a, a,   a,    a)
+type instance F4 (Maybe a) = (Hx a, a, Int, Bool)
+
+type family G2 a b = r | r -> a b
+type instance G2 a    Bool = (a, a)
+type instance G2 Bool b    = (b, Bool)
+
+type family G6 a = r | r -> a
+type instance G6 [a]  = [Gi a]
+type instance G6 Bool = Int
+
+g6_id :: G6 a -> G6 a
+g6_id x = x
+
+g6_use :: [Char]
+g6_use = g6_id "foo"
+
+-- A sole exception to "bare variables in the RHS" rule
+type family Id (a :: k) = (result :: k) | result -> a
+type instance Id a = a
+
+-- This makes sure that over-saturated type family applications at the top-level
+-- are accepted.
+type family IdProxy (a :: k) b = r | r -> a
+type instance IdProxy a b = (Id a) b
+
+-- make sure we look through type synonyms properly
+type IdSyn a = Id a
+type family IdProxySyn (a :: k) b = r | r -> a
+type instance IdProxySyn a b = (IdSyn a) b
+
+-- this has bare variable in the RHS but all LHS varaiables are also bare so it
+-- should be accepted
+type family Fa (a :: k) (b :: k) = (r :: k2) | r -> k
+type instance Fa a b = a
+
+-- Taken from #9587. This exposed a bug in the solver.
+type family Arr (repr :: * -> *) (a :: *) (b :: *) = (r :: *) | r -> repr a b
+
+class ESymantics repr where
+    int :: Int  -> repr Int
+    add :: repr Int  -> repr Int -> repr Int
+
+    lam :: (repr a -> repr b) -> repr (Arr repr a b)
+    app :: repr (Arr repr a b) -> repr a -> repr b
+
+te4 = let c3 = lam (\f -> lam (\x -> f `app` (f `app` (f `app` x))))
+      in (c3 `app` (lam (\x -> x `add` int 14))) `app` (int 0)
+
+-- This used to fail during development
+class Manifold' a where
+    type Base  a = r | r -> a
+    project :: a -> Base a
+    unproject :: Base a -> a
+
+id' :: forall a. ( Manifold' a ) => Base a -> Base a
+id' = project . unproject
diff --git a/testsuite/tests/typecheck/should_compile/T6018.hs-boot b/testsuite/tests/typecheck/should_compile/T6018.hs-boot
new file mode 100644
index 0000000000..8ac5ce9e51
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T6018.hs-boot
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies, PolyKinds #-}
+
+module T6018 where
+
+-- this declaration uses different type variables than the one in the source
+-- file but it should be accepted nevertheless
+type family F d e f = (r :: k) | r -> d e f
diff --git a/testsuite/tests/typecheck/should_compile/T6018.stderr b/testsuite/tests/typecheck/should_compile/T6018.stderr
new file mode 100644
index 0000000000..41e94d8670
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T6018.stderr
@@ -0,0 +1,11 @@
+[1 of 3] Compiling T6018[boot]      ( T6018.hs-boot, T6018.o-boot )
+[2 of 3] Compiling T6018a           ( T6018a.hs, T6018a.o )
+[3 of 3] Compiling T6018            ( T6018.hs, T6018.o )
+
+T6018.hs:75:5: Warning:
+    Type family instance equation is overlapped:
+       Foo Bool = Bool
+
+T6018.hs:82:5: Warning:
+    Type family instance equation is overlapped:
+       Bar Bool = Char
diff --git a/testsuite/tests/typecheck/should_compile/T6018a.hs b/testsuite/tests/typecheck/should_compile/T6018a.hs
new file mode 100644
index 0000000000..beecb57c65
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T6018a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T6018a where
+
+import {-# SOURCE #-} T6018 -- test support for hs-boot files
+
+type family G a b c = (result :: *) | result -> a b c
+type instance G Int  Char Bool = Bool
+type instance G Char Bool Int  = Int
+
+type instance F Bool Int  Char = Char
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index b469689445..eff84032b1 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -358,6 +358,7 @@ test('tc263',
     extra_clean(['Tc263_Help.o','Tc263_Help.hi']),
     multimod_compile, ['tc263','-v0'])
 test('tc264', normal, multimod_compile, ['tc264.hsig', '-sig-of "ShouldCompile is base:Data.STRef"'])
+test('tc265', compile_timeout_multiplier(0.01), compile, [''])
 
 test('GivenOverlapping', normal, compile, [''])
 test('GivenTypeSynonym', normal, compile, [''])
@@ -385,6 +386,9 @@ test('T6055', normal, compile, [''])
 test('DfltProb1', normal, compile, [''])
 test('DfltProb2', normal, compile, [''])
 test('T6134', normal, compile, [''])
+test('T6018', extra_clean(['T6018.hi' , 'T6018.o'
+                          ,'T6018A.hi', 'T6018A.o'])
+            , multimod_compile, ['T6018', ''])
 test('TcLambdaCase', when(compiler_lt('ghc', '7.5'), skip), compile, [''])
 test('T7147', normal, compile, [''])
 test('T7171',normal,run_command,
diff --git a/testsuite/tests/typecheck/should_compile/holes2.stderr b/testsuite/tests/typecheck/should_compile/holes2.stderr
index 392b69992d..ad5b530fae 100644
--- a/testsuite/tests/typecheck/should_compile/holes2.stderr
+++ b/testsuite/tests/typecheck/should_compile/holes2.stderr
@@ -3,9 +3,9 @@ holes2.hs:3:5: warning:
     No instance for (Show a0) arising from a use of ‘show’
     The type variable ‘a0’ is ambiguous
     Potential instances:
-      instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
       instance Show Ordering -- Defined in ‘GHC.Show’
       instance Show Integer -- Defined in ‘GHC.Show’
+      instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
       ...plus 22 others
       (use -fprint-potential-instances to see them all)
     In the expression: show _
diff --git a/testsuite/tests/typecheck/should_compile/tc265.hs b/testsuite/tests/typecheck/should_compile/tc265.hs
new file mode 100644
index 0000000000..eff43d8b42
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/tc265.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Tc265 where
+
+data T a = MkT (F a)
+type family F a where
+  F (T a) = a
+  F (T Int) = Bool
diff --git a/testsuite/tests/typecheck/should_compile/tc265.stderr b/testsuite/tests/typecheck/should_compile/tc265.stderr
new file mode 100644
index 0000000000..64099721b8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/tc265.stderr
@@ -0,0 +1,4 @@
+
+tc265.hs:8:3: warning:
+    Type family instance equation is overlapped:
+      F (T Int) = Bool
diff --git a/testsuite/tests/typecheck/should_fail/T6018Afail.hs b/testsuite/tests/typecheck/should_fail/T6018Afail.hs
new file mode 100644
index 0000000000..95184a177c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018Afail.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T6018Afail where
+
+type family G a b c = (result :: *) | result -> a b c
+type instance G Int  Char Bool = Bool
+type instance G Char Bool Int  = Int
diff --git a/testsuite/tests/typecheck/should_fail/T6018Bfail.hs b/testsuite/tests/typecheck/should_fail/T6018Bfail.hs
new file mode 100644
index 0000000000..ef2460187f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018Bfail.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T6018Bfail where
+
+type family H a b c = (result :: *) | result -> a b c
diff --git a/testsuite/tests/typecheck/should_fail/T6018Cfail.hs b/testsuite/tests/typecheck/should_fail/T6018Cfail.hs
new file mode 100644
index 0000000000..b7a790824c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018Cfail.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T6018Cfail where
+
+import T6018Bfail
+
+type instance H Int  Char Bool = Bool
+type instance H Char Bool Int  = Int
diff --git a/testsuite/tests/typecheck/should_fail/T6018Dfail.hs b/testsuite/tests/typecheck/should_fail/T6018Dfail.hs
new file mode 100644
index 0000000000..ec69833f1d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018Dfail.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T6018Dfail where
+
+import T6018Bfail
+
+type instance H Bool Int  Char = Int
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.hs b/testsuite/tests/typecheck/should_fail/T6018fail.hs
new file mode 100644
index 0000000000..ead4dd354f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances, PolyKinds,
+             MultiParamTypeClasses, FlexibleInstances #-}
+
+module T6018fail where
+
+import T6018Afail -- defines G, identical to F
+import T6018Cfail -- imports H from T6018Bfail, defines some equations for H
+import T6018Dfail -- imports H from T6018Bfail, defines conflicting eqns
+
+type family F a b c = (result :: *) | result -> a b c
+type instance F Int  Char Bool = Bool
+type instance F Char Bool Int  = Int
+type instance F Bool Int  Char = Int
+
+type instance G Bool Int  Char = Int
+
+type family I a b c = r | r -> a b
+type instance I Int  Char Bool = Bool
+type instance I Int  Int  Int  = Bool
+type instance I Bool Int  Int  = Int
+
+-- Id is injective...
+type family Id a = result | result -> a
+type instance Id a = a
+
+-- ...but despite that we disallow a call to Id
+type family IdProxy a = r | r -> a
+type instance IdProxy a = Id a
+
+data N = Z | S N
+
+-- P 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 P (a :: N) (b :: N) = (r :: N) | r -> a b
+type instance P  Z    m = m
+type instance P (S n) m = S (P n m)
+
+-- this is not injective - not all injective type variables mentioned
+-- on LHS are mentioned on RHS
+type family J a b c = r | r -> a b
+type instance J Int b c = Char
+
+-- same as above, but tyvar is now nested inside a tycon
+type family K (a :: N) (b :: N) = (r :: N) | r -> a b
+type instance K (S n) m = S m
+
+-- Make sure we look through type synonyms to catch errors
+type MaybeSyn a = Id a
+type family L a = r | r -> a
+type instance L a = MaybeSyn a
+
+-- These should fail because given the RHS kind there is no way to determine LHS
+-- kind
+class PolyKindVarsC a where
+    type PolyKindVarsF a = (r :: k) | r -> a
+
+instance PolyKindVarsC '[] where
+    type PolyKindVarsF '[] = '[]
+
+type family PolyKindVars (a :: k0) = (r :: k1) | r -> a
+type instance PolyKindVars '[] = '[]
+
+-- This should fail because there is no way to determine k from the RHS
+type family Fc (a :: k) (b :: k) = r | r -> k
+type instance Fc a b = Int
+
+-- 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
+type instance Gc a b = Int
+
+-- fails because injectivity is not compositional in this case
+type family F1 a = r | r -> a
+type instance F1 [a]       = Maybe (GF1 a)
+type instance F1 (Maybe a) = Maybe (GF2 a)
+
+type family GF1 a = r | r -> a
+type instance GF1 Int = Bool
+
+type family GF2 a = r | r -> a
+type instance GF2 Int = Bool
+
+type family HF1 a
+type instance HF1 Bool = Bool
+
+type family W1 a = r | r -> a
+type instance W1 [a] = a
+
+type family W2 a = r | r -> a
+type instance W2 [a] = W2 a
+
+-- not injective because of infinite types
+type family Z1 a = r | r -> a
+type instance Z1 [a]       = (a, a)
+type instance Z1 (Maybe b) = (b, [b])
+
+type family G1 a = r | r -> a
+type instance G1 [a]       = [a]
+type instance G1 (Maybe b) = [(b, b)]
+
+type family G3 a b = r | r -> b
+type instance G3 a Int  = (a, Int)
+type instance G3 a Bool = (Bool, a)
+
+type family G4 a b = r | r -> a b
+type instance G4 a b = [a]
+
+type family G5 a = r | r -> a
+type instance G5 [a] = [GF1 a] -- GF1 injective
+type instance G5 Int = [Bool]
+
+type family G6 a = r | r -> a
+type instance G6 [a]  = [HF1 a] -- HF1 not injective
+type instance G6 Bool = Int
+
+type family G7a a b (c :: k) = r | r -> a b
+type family G7 a b (c :: k) = r | r -> a b c
+type instance G7 a b c = [G7a a b c]
+
+class C a b where
+    type FC a (b :: *) = r | r -> b
+    type instance FC a b = b
+
+instance C Int Char where
+    type FC Int Char = Bool
+
+-- this should fail because the default instance conflicts with one of the
+-- earlier instances
+instance C Int Bool {- where
+    type FC Int Bool = Bool-}
+
+-- and this should fail because it violates "bare variable in the RHS"
+-- restriction
+instance C Char a
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
new file mode 100644
index 0000000000..440ddacd91
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -0,0 +1,149 @@
+[1 of 5] Compiling T6018Bfail       ( T6018Bfail.hs, T6018Bfail.o )
+[2 of 5] Compiling T6018Dfail       ( T6018Dfail.hs, T6018Dfail.o )
+[3 of 5] Compiling T6018Cfail       ( T6018Cfail.hs, T6018Cfail.o )
+[4 of 5] Compiling T6018Afail       ( T6018Afail.hs, T6018Afail.o )
+[5 of 5] Compiling T6018fail        ( T6018fail.hs, T6018fail.o )
+
+T6018Afail.hs:7:15:
+    Type family equations violate injectivity annotation:
+      G Char Bool Int = Int
+      G Bool Int Char = Int
+
+T6018Dfail.hs:7:15:
+    Type family equations violate injectivity annotation:
+      T6018Bfail.H Bool Int Char = Int
+      T6018Bfail.H Char Bool Int = Int
+
+T6018fail.hs:13:15:
+    Type family equations violate injectivity annotation:
+      F Bool Int Char = Int
+      F Char Bool Int = Int
+
+T6018fail.hs:19:15:
+    Type family equations violate injectivity annotation:
+      I Int Int Int = Bool
+      I Int Char Bool = Bool
+
+T6018fail.hs:28:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      IdProxy a = Id a
+
+T6018fail.hs:36:15:
+    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’
+      P 'Z m = m
+
+T6018fail.hs:37:15:
+    Type family equations violate injectivity annotation:
+      P ('S n) m = 'S (P n m)
+      P 'Z m = m
+
+T6018fail.hs:42:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘b’ does not appear on injective position.
+    In the RHS of type family equation:
+      J Int b c = Char
+
+T6018fail.hs:46:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘n’ does not appear on injective position.
+    In the RHS of type family equation:
+      K ('S n) m = 'S m
+
+T6018fail.hs:51:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      L a = MaybeSyn a
+
+T6018fail.hs:59:10:
+    Type family equation violates injectivity annotation.
+    Injective kind variable ‘k1’ is not inferable from the RHS type variables.
+    In the RHS of type family equation:
+      PolyKindVarsF '[] = '[]
+
+T6018fail.hs:62:15:
+    Type family equation violates injectivity annotation.
+    Injective kind variable ‘k1’ is not inferable from the RHS type variables.
+    In the RHS of type family equation:
+      PolyKindVars '[] = '[]
+
+T6018fail.hs:66:15:
+    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). Fc a b = Int
+
+T6018fail.hs:70:15:
+    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
+
+T6018fail.hs:75:15:
+    Type family equations violate injectivity annotation:
+      F1 (Maybe a) = Maybe (GF2 a)
+      F1 [a] = Maybe (GF1 a)
+
+T6018fail.hs:87:15:
+    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: ‘[a]’
+      W1 [a] = a
+
+T6018fail.hs:90:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      W2 [a] = W2 a
+
+T6018fail.hs:95:15:
+    Type family equations violate injectivity annotation:
+      Z1 (Maybe b) = (b, [b])
+      Z1 [a] = (a, a)
+
+T6018fail.hs:99:15:
+    Type family equations violate injectivity annotation:
+      G1 (Maybe b) = [(b, b)]
+      G1 [a] = [a]
+
+T6018fail.hs:103:15:
+    Type family equations violate injectivity annotation:
+      G3 a Bool = (Bool, a)
+      G3 a Int = (a, Int)
+
+T6018fail.hs:106:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘b’ does not appear on injective position.
+    In the RHS of type family equation:
+      G4 a b = [a]
+
+T6018fail.hs:110:15:
+    Type family equations violate injectivity annotation:
+      G5 Int = [Bool]
+      G5 [a] = [GF1 a]
+
+T6018fail.hs:113:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘a’ does not appear on injective position.
+    In the RHS of type family equation:
+      G6 [a] = [HF1 a]
+
+T6018fail.hs:118:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘c’ 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) a b (c :: k). G7 a b c = [G7a a b c]
+
+T6018fail.hs:129:1:
+    Type family equations violate injectivity annotation:
+      FC Int Bool = Bool
+      FC Int Char = Bool
+
+T6018fail.hs:134:1:
+    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: ‘*’, ‘Char’
+      FC Char a = a
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed1.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed1.hs
new file mode 100644
index 0000000000..c650781847
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed1.hs
@@ -0,0 +1,11 @@
+{-# 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
new file mode 100644
index 0000000000..968e9e797b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed1.stderr
@@ -0,0 +1,7 @@
+
+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
new file mode 100644
index 0000000000..99828c6809
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed10.hs
@@ -0,0 +1,17 @@
+{-# 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
new file mode 100644
index 0000000000..6248f97a47
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed10.stderr
@@ -0,0 +1,9 @@
+
+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
new file mode 100644
index 0000000000..566551cfef
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed11.hs
@@ -0,0 +1,15 @@
+{-# 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
new file mode 100644
index 0000000000..7c7496b819
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed11.stderr
@@ -0,0 +1,7 @@
+
+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
new file mode 100644
index 0000000000..9ff9a396a0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed12.hs
@@ -0,0 +1,7 @@
+{-# 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
new file mode 100644
index 0000000000..2ad07aa2a4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed12.stderr
@@ -0,0 +1,8 @@
+
+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
new file mode 100644
index 0000000000..44abb06b16
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed2.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
+
+module T6018failclosed2 where
+
+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)
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
new file mode 100644
index 0000000000..11ece3d7f5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
@@ -0,0 +1,16 @@
+
+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’
+
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed3.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed3.hs
new file mode 100644
index 0000000000..e43ee75e1f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed3.hs
@@ -0,0 +1,8 @@
+{-# 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
new file mode 100644
index 0000000000..968dd76323
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed3.stderr
@@ -0,0 +1,8 @@
+
+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
new file mode 100644
index 0000000000..116a9c6df4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed4.hs
@@ -0,0 +1,10 @@
+{-# 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
new file mode 100644
index 0000000000..5db55db602
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed4.stderr
@@ -0,0 +1,8 @@
+
+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
new file mode 100644
index 0000000000..9665365a2f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed5.hs
@@ -0,0 +1,12 @@
+{-# 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
new file mode 100644
index 0000000000..57ab357bc2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed5.stderr
@@ -0,0 +1,8 @@
+
+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
new file mode 100644
index 0000000000..ef55b558e1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed6.hs
@@ -0,0 +1,7 @@
+{-# 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
new file mode 100644
index 0000000000..be8a763ad4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed6.stderr
@@ -0,0 +1,9 @@
+
+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
new file mode 100644
index 0000000000..a82c323509
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed7.hs
@@ -0,0 +1,8 @@
+{-# 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
new file mode 100644
index 0000000000..6cdfed528a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed7.stderr
@@ -0,0 +1,7 @@
+
+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
new file mode 100644
index 0000000000..8936427547
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed8.hs
@@ -0,0 +1,8 @@
+{-# 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
new file mode 100644
index 0000000000..046eed7830
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed8.stderr
@@ -0,0 +1,7 @@
+
+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
new file mode 100644
index 0000000000..5ec59066b2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed9.hs
@@ -0,0 +1,8 @@
+{-# 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
new file mode 100644
index 0000000000..325d9c03ed
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed9.stderr
@@ -0,0 +1,8 @@
+
+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/T9201.stderr b/testsuite/tests/typecheck/should_fail/T9201.stderr
index 44e338a697..5f16dcaedd 100644
--- a/testsuite/tests/typecheck/should_fail/T9201.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9201.stderr
@@ -1,5 +1,5 @@
 
-T9201.hs:6:17:
+T9201.hs:6:17: error:
     The first argument of ‘f’ should have kind ‘x1’,
       but ‘a’ has kind ‘y1’
     In the type ‘d a (f a)’
diff --git a/testsuite/tests/typecheck/should_fail/T9260.stderr b/testsuite/tests/typecheck/should_fail/T9260.stderr
index 4d1a94a4bd..a163b16cbd 100644
--- a/testsuite/tests/typecheck/should_fail/T9260.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9260.stderr
@@ -1,8 +1,7 @@
 
 T9260.hs:12:8: error:
-    Couldn't match type ‘(n0 + 1) + 1’ with ‘1’
-    The type variable ‘n0’ is ambiguous
+    Couldn't match type ‘2’ with ‘1’
     Expected type: Fin 1
-      Actual type: Fin ((n0 + 1) + 1)
+      Actual type: Fin (1 + 1)
     In the expression: Fsucc Fzero
     In an equation for ‘test’: test = Fsucc Fzero
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 1a2ff9aa81..85532dede5 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -277,6 +277,24 @@ test('T5957', normal, compile_fail, [''])
 test('T6001', normal, compile_fail, [''])
 test('T6022', normal, compile_fail, [''])
 test('T5853', normal, compile_fail, [''])
+test('T6018fail', extra_clean([ 'T6018fail.hi' , 'T6018fail.o'
+                              , 'T6018Afail.hi', 'T6018Afail.o'
+                              , 'T6018Bfail.hi', 'T6018Bfail.o'
+                              , 'T6018Cfail.hi', 'T6018Cfail.o'
+                              , 'T6018Dfail.hi', 'T6018Dfail.o'])
+    , multimod_compile_fail, ['T6018fail', '-no-hs-main -c'])
+test('T6018failclosed1', 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, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail072.stderr b/testsuite/tests/typecheck/should_fail/tcfail072.stderr
index f3386f164b..3f40718428 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail072.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail072.stderr
@@ -7,10 +7,10 @@ tcfail072.hs:23:13: error:
       at tcfail072.hs:22:6-38
     The type variable ‘p0’ is ambiguous
     Potential instances:
-      instance Ord a => Ord (Maybe a) -- Defined in ‘GHC.Base’
       instance Ord Ordering -- Defined in ‘GHC.Classes’
       instance Ord Integer
         -- Defined in ‘integer-gmp-1.0.0.0:GHC.Integer.Type’
+      instance Ord a => Ord (Maybe a) -- Defined in ‘GHC.Base’
       ...plus 22 others
       ...plus one instance involving out-of-scope types
       (use -fprint-potential-instances to see them all)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail133.stderr b/testsuite/tests/typecheck/should_fail/tcfail133.stderr
index 1869cea44b..bba5889603 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail133.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail133.stderr
@@ -6,9 +6,10 @@ tcfail133.hs:68:7: error:
     No instance for (Show r0) arising from a use of ‘show’
     The type variable ‘r0’ is ambiguous
     Potential instances:
-      instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
       instance Show Ordering -- Defined in ‘GHC.Show’
       instance Show Integer -- Defined in ‘GHC.Show’
+      instance (Show a, Show b, Number a, Digit b) => Show (a :@ b)
+        -- Defined at tcfail133.hs:11:54
       ...plus 25 others
       (use -fprint-potential-instances to see them all)
     In the expression: show
diff --git a/testsuite/tests/typecheck/should_fail/tcfail181.stderr b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
index 3d3507f256..70dbbd5508 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail181.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
@@ -7,8 +7,8 @@ tcfail181.hs:17:9: error:
       at tcfail181.hs:17:1-30
     The type variable ‘m0’ is ambiguous
     Potential instances:
-      instance Monad Maybe -- Defined in ‘GHC.Base’
       instance Monad IO -- Defined in ‘GHC.Base’
+      instance Monad Maybe -- Defined in ‘GHC.Base’
       instance Monad ((->) r) -- Defined in ‘GHC.Base’
       ...plus two others
       (use -fprint-potential-instances to see them all)