From 80cac93f030cd0bbd5ff8dd197effaacf6ae651d Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <eir@cis.upenn.edu>
Date: Fri, 21 Dec 2012 20:55:29 -0500
Subject: [PATCH] Implement overlapping type family instances.

An ordered, overlapping type family instance is introduced by 'type
instance
where', followed by equations. See the new section in the user manual
(7.7.2.2) for details. The canonical example is Boolean equality at the
type
level:

type family Equals (a :: k) (b :: k) :: Bool
type instance where
  Equals a a = True
  Equals a b = False

A branched family instance, such as this one, checks its equations in
order
and applies only the first the matches. As explained in the note
[Instance
checking within groups] in FamInstEnv.lhs, we must be careful not to
simplify,
say, (Equals Int b) to False, because b might later unify with Int.

This commit includes all of the commits on the overlapping-tyfams
branch. SPJ
requested that I combine all my commits over the past several months
into one
monolithic commit. The following GHC repos are affected: ghc, testsuite,
utils/haddock, libraries/template-haskell, and libraries/dph.

Here are some details for the interested:

- The definition of CoAxiom has been moved from TyCon.lhs to a
  new file CoAxiom.lhs. I made this decision because of the
  number of definitions necessary to support BranchList.

- BranchList is a GADT whose type tracks whether it is a
  singleton list or not-necessarily-a-singleton-list. The reason
  I introduced this type is to increase static checking of places
  where GHC code assumes that a FamInst or CoAxiom is indeed a
  singleton. This assumption takes place roughly 10 times
  throughout the code. I was worried that a future change to GHC
  would invalidate the assumption, and GHC might subtly fail to
  do the right thing. By explicitly labeling CoAxioms and
  FamInsts as being Unbranched (singleton) or
  Branched (not-necessarily-singleton), we make this assumption
  explicit and checkable. Furthermore, to enforce the accuracy of
  this label, the list of branches of a CoAxiom or FamInst is
  stored using a BranchList, whose constructors constrain its
  type index appropriately.

I think that the decision to use BranchList is probably the most
controversial decision I made from a code design point of view.
Although I provide conversions to/from ordinary lists, it is more
efficient to use the brList... functions provided in CoAxiom than
always to convert. The use of these functions does not wander far
from the core CoAxiom/FamInst logic.

BranchLists are motivated and explained in the note [Branched axioms] in
CoAxiom.lhs.

- The CoAxiom type has changed significantly. You can see the new
  type in CoAxiom.lhs. It uses a CoAxBranch type to track
  branches of the CoAxiom. Correspondingly various functions
  producing and consuming CoAxioms had to change, including the
  binary layout of interface files.

- To get branched axioms to work correctly, it is important to have a
  notion
  of type "apartness": two types are apart if they cannot unify, and no
  substitution of variables can ever get them to unify, even after type
family
  simplification. (This is different than the normal failure to unify
because
  of the type family bit.) This notion in encoded in tcApartTys, in
Unify.lhs.
  Because apartness is finer-grained than unification, the tcUnifyTys
now
  calls tcApartTys.

- CoreLinting axioms has been updated, both to reflect the new
  form of CoAxiom and to enforce the apartness rules of branch
  application. The formalization of the new rules is in
  docs/core-spec/core-spec.pdf.

- The FamInst type (in types/FamInstEnv.lhs) has changed
  significantly, paralleling the changes to CoAxiom. Of course,
  this forced minor changes in many files.

- There are several new Notes in FamInstEnv.lhs, including one
  discussing confluent overlap and why we're not doing it.

- lookupFamInstEnv, lookupFamInstEnvConflicts, and
  lookup_fam_inst_env' (the function that actually does the work)
  have all been more-or-less completely rewritten. There is a
  Note [lookup_fam_inst_env' implementation] describing the
  implementation. One of the changes that affects other files is
  to change the type of matches from a pair of (FamInst, [Type])
  to a new datatype (which now includes the index of the matching
  branch). This seemed a better design.

- The TySynInstD constructor in Template Haskell was updated to
  use the new datatype TySynEqn. I also bumped the TH version
  number, requiring changes to DPH cabal files. (That's why the
  DPH repo has an overlapping-tyfams branch.)

- As SPJ requested, I refactored some of the code in HsDecls:

 * splitting up TyDecl into SynDecl and DataDecl, correspondingly
   changing HsTyDefn to HsDataDefn (with only one constructor)

 * splitting FamInstD into TyFamInstD and DataFamInstD and
   splitting FamInstDecl into DataFamInstDecl and TyFamInstDecl

 * making the ClsInstD take a ClsInstDecl, for parallelism with
   InstDecl's other constructors

 * changing constructor TyFamily into FamDecl

 * creating a FamilyDecl type that stores the details for a family
   declaration; this is useful because FamilyDecls can appear in classes
but
   other decls cannot

 * restricting the associated types and associated type defaults for a
 * class
   to be the new, more restrictive types

 * splitting cid_fam_insts into cid_tyfam_insts and cid_datafam_insts,
   according to the new types

 * perhaps one or two more that I'm overlooking

None of these changes has far-reaching implications.

- The user manual, section 7.7.2.2, is updated to describe the new type
  family
  instances.
---
 .../indexed-types/should_compile/Overlap1.hs  | 14 +++++
 .../indexed-types/should_compile/Overlap12.hs | 16 +++++
 .../indexed-types/should_compile/Overlap2.hs  | 14 +++++
 .../indexed-types/should_compile/T3017.stderr |  2 +-
 tests/indexed-types/should_compile/all.T      |  4 ++
 .../should_fail/NotRelaxedExamples.stderr     |  6 +-
 tests/indexed-types/should_fail/Over.stderr   |  8 +--
 tests/indexed-types/should_fail/Overlap10.hs  | 15 +++++
 .../should_fail/Overlap10.stderr              |  7 +++
 tests/indexed-types/should_fail/Overlap11.hs  | 15 +++++
 .../should_fail/Overlap11.stderr              |  6 ++
 tests/indexed-types/should_fail/Overlap3.hs   | 15 +++++
 .../indexed-types/should_fail/Overlap3.stderr | 10 ++++
 tests/indexed-types/should_fail/Overlap4.hs   | 16 +++++
 .../indexed-types/should_fail/Overlap4.stderr |  5 ++
 tests/indexed-types/should_fail/Overlap5.hs   | 22 +++++++
 .../indexed-types/should_fail/Overlap5.stderr | 29 ++++++++++
 tests/indexed-types/should_fail/Overlap6.hs   | 16 +++++
 .../indexed-types/should_fail/Overlap6.stderr | 15 +++++
 tests/indexed-types/should_fail/Overlap7.hs   | 10 ++++
 .../indexed-types/should_fail/Overlap7.stderr | 10 ++++
 tests/indexed-types/should_fail/Overlap8.hs   | 11 ++++
 .../indexed-types/should_fail/Overlap8.stderr |  5 ++
 tests/indexed-types/should_fail/Overlap9.hs   | 14 +++++
 .../indexed-types/should_fail/Overlap9.stderr | 12 ++++
 .../should_fail/SimpleFail11a.stderr          |  8 +--
 .../should_fail/SimpleFail11b.stderr          |  8 +--
 .../should_fail/SimpleFail11c.stderr          |  8 +--
 .../should_fail/SimpleFail11d.stderr          |  4 +-
 .../should_fail/SimpleFail12.stderr           |  2 +-
 .../should_fail/SimpleFail13.stderr           |  2 +-
 .../should_fail/SimpleFail2a.stderr           | 17 ++++--
 .../should_fail/SimpleFail2b.stderr           |  4 +-
 .../should_fail/SimpleFail4.stderr            |  2 +-
 .../should_fail/SimpleFail9.stderr            | 12 ++--
 tests/indexed-types/should_fail/T2157.stderr  |  2 +-
 tests/indexed-types/should_fail/T2334.stderr  |  4 +-
 tests/indexed-types/should_fail/T2677.stderr  |  4 +-
 tests/indexed-types/should_fail/T3330b.stderr |  4 +-
 tests/indexed-types/should_fail/T4246.stderr  |  8 +--
 tests/indexed-types/should_fail/T5515.stderr  |  4 +-
 .../should_fail/TyFamArity1.stderr            |  2 +-
 .../should_fail/TyFamArity2.stderr            |  2 +-
 .../should_fail/TyFamUndec.stderr             |  6 +-
 tests/indexed-types/should_fail/all.T         | 10 ++++
 tests/simplCore/should_compile/Makefile       |  2 +-
 tests/simplCore/should_compile/T4201.stdout   |  4 +-
 tests/th/T5886a.hs                            |  2 +-
 tests/th/TH_TyInstWhere1.hs                   | 17 ++++++
 tests/th/TH_TyInstWhere1.stderr               |  9 +++
 tests/th/TH_TyInstWhere2.hs                   | 15 +++++
 tests/th/TH_TyInstWhere2.stderr               |  5 ++
 tests/th/TH_TyInstWhere3.hs                   | 18 ++++++
 tests/th/TH_TyInstWhere3.stderr               |  3 +
 tests/th/TH_TyInstWhere4.hs                   | 20 +++++++
 tests/th/TH_TyInstWhere4.stderr               | 16 +++++
 tests/th/all.T                                |  5 ++
 tests/typecheck/should_compile/T5481.stderr   |  4 +-
 tests/typecheck/should_compile/tc231.stderr   | 58 +++++++++----------
 .../typecheck/should_fail/AssocTyDef02.stderr |  2 +-
 .../typecheck/should_fail/AssocTyDef05.stderr | 10 ++--
 .../typecheck/should_fail/AssocTyDef06.stderr | 10 ++--
 62 files changed, 508 insertions(+), 102 deletions(-)
 create mode 100644 tests/indexed-types/should_compile/Overlap1.hs
 create mode 100644 tests/indexed-types/should_compile/Overlap12.hs
 create mode 100644 tests/indexed-types/should_compile/Overlap2.hs
 create mode 100644 tests/indexed-types/should_fail/Overlap10.hs
 create mode 100644 tests/indexed-types/should_fail/Overlap10.stderr
 create mode 100644 tests/indexed-types/should_fail/Overlap11.hs
 create mode 100644 tests/indexed-types/should_fail/Overlap11.stderr
 create mode 100644 tests/indexed-types/should_fail/Overlap3.hs
 create mode 100644 tests/indexed-types/should_fail/Overlap3.stderr
 create mode 100644 tests/indexed-types/should_fail/Overlap4.hs
 create mode 100644 tests/indexed-types/should_fail/Overlap4.stderr
 create mode 100644 tests/indexed-types/should_fail/Overlap5.hs
 create mode 100644 tests/indexed-types/should_fail/Overlap5.stderr
 create mode 100644 tests/indexed-types/should_fail/Overlap6.hs
 create mode 100644 tests/indexed-types/should_fail/Overlap6.stderr
 create mode 100644 tests/indexed-types/should_fail/Overlap7.hs
 create mode 100644 tests/indexed-types/should_fail/Overlap7.stderr
 create mode 100644 tests/indexed-types/should_fail/Overlap8.hs
 create mode 100644 tests/indexed-types/should_fail/Overlap8.stderr
 create mode 100644 tests/indexed-types/should_fail/Overlap9.hs
 create mode 100644 tests/indexed-types/should_fail/Overlap9.stderr
 create mode 100644 tests/th/TH_TyInstWhere1.hs
 create mode 100644 tests/th/TH_TyInstWhere1.stderr
 create mode 100644 tests/th/TH_TyInstWhere2.hs
 create mode 100644 tests/th/TH_TyInstWhere2.stderr
 create mode 100644 tests/th/TH_TyInstWhere3.hs
 create mode 100644 tests/th/TH_TyInstWhere3.stderr
 create mode 100644 tests/th/TH_TyInstWhere4.hs
 create mode 100644 tests/th/TH_TyInstWhere4.stderr

diff --git a/tests/indexed-types/should_compile/Overlap1.hs b/tests/indexed-types/should_compile/Overlap1.hs
new file mode 100644
index 000000000..b285deece
--- /dev/null
+++ b/tests/indexed-types/should_compile/Overlap1.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Overlap1 where
+
+type family F a
+type instance where
+  F Int = Int
+  F a = Bool
+
+g :: F Int
+g = 5
+
+h :: F Char
+h = False
diff --git a/tests/indexed-types/should_compile/Overlap12.hs b/tests/indexed-types/should_compile/Overlap12.hs
new file mode 100644
index 000000000..414c9d9f0
--- /dev/null
+++ b/tests/indexed-types/should_compile/Overlap12.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
+
+module Overlap12 where
+
+type family And (a :: Bool) (b :: Bool) :: Bool
+type instance where
+  And False x = False
+  And True x = x
+  And x False = False
+  And x True = x
+  And x x = x
+
+data Proxy p = P
+
+i :: Proxy (And False x)
+i = (P :: Proxy False)
\ No newline at end of file
diff --git a/tests/indexed-types/should_compile/Overlap2.hs b/tests/indexed-types/should_compile/Overlap2.hs
new file mode 100644
index 000000000..ced2dd429
--- /dev/null
+++ b/tests/indexed-types/should_compile/Overlap2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Overlap2 where
+
+type family F a b
+type instance where
+  F a a = Int
+  F a b = Bool
+
+g :: F Char Double
+g = False
+
+h :: F Double Double
+h = -2
diff --git a/tests/indexed-types/should_compile/T3017.stderr b/tests/indexed-types/should_compile/T3017.stderr
index 4218a4a60..b7bedaea6 100644
--- a/tests/indexed-types/should_compile/T3017.stderr
+++ b/tests/indexed-types/should_compile/T3017.stderr
@@ -15,7 +15,7 @@ TYPE CONSTRUCTORS
       = L :: forall a. [a] -> ListColl a Stricts: _
       FamilyInstance: none
 COERCION AXIOMS
-  axiom Foo.TFCo:R:ElemListColl a :: Elem (ListColl a) ~# a
+  axiom Foo.TFCo:R:ElemListColl :: forall a. Elem (ListColl a) ~# a
 INSTANCES
   instance Coll (ListColl a) -- Defined at T3017.hs:12:11
 FAMILY INSTANCES
diff --git a/tests/indexed-types/should_compile/all.T b/tests/indexed-types/should_compile/all.T
index 2f94d9518..d785e82b8 100644
--- a/tests/indexed-types/should_compile/all.T
+++ b/tests/indexed-types/should_compile/all.T
@@ -196,6 +196,10 @@ test('T6152',
 
 test('T6088', normal, compile, [''])
 test('T7082', normal, compile, [''])
+
+test('Overlap1', normal, compile, [''])
+test('Overlap2', normal, compile, [''])
+test('Overlap12', normal, compile, [''])
 test('T7156', normal, compile, [''])
 test('T5591a', normal, compile, [''])
 test('T5591b', normal, compile, [''])
diff --git a/tests/indexed-types/should_fail/NotRelaxedExamples.stderr b/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
index 030f742ee..d08570a06 100644
--- a/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
+++ b/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
@@ -1,17 +1,17 @@
 
-NotRelaxedExamples.hs:9:1:
+NotRelaxedExamples.hs:9:15:
     Nested type family application
       in the type family application: F1 (F1 Char)
     (Use -XUndecidableInstances to permit this)
     In the type instance declaration for `F1'
 
-NotRelaxedExamples.hs:10:1:
+NotRelaxedExamples.hs:10:15:
     Application is no smaller than the instance head
       in the type family application: F2 [x]
     (Use -XUndecidableInstances to permit this)
     In the type instance declaration for `F2'
 
-NotRelaxedExamples.hs:11:1:
+NotRelaxedExamples.hs:11:15:
     Application is no smaller than the instance head
       in the type family application: F3 [Char]
     (Use -XUndecidableInstances to permit this)
diff --git a/tests/indexed-types/should_fail/Over.stderr b/tests/indexed-types/should_fail/Over.stderr
index bb973eee0..ae89d053b 100644
--- a/tests/indexed-types/should_fail/Over.stderr
+++ b/tests/indexed-types/should_fail/Over.stderr
@@ -1,10 +1,10 @@
 
 OverB.hs:7:15:
     Conflicting family instance declarations:
-      data instance OverA.C [Int] [a] -- Defined at OverB.hs:7:15
-      data instance OverA.C [a] [Int] -- Defined at OverC.hs:7:15
+      OverA.C [Int] [a] -- Defined at OverB.hs:7:15
+      OverA.C [a] [Int] -- Defined at OverC.hs:7:15
 
 OverB.hs:9:15:
     Conflicting family instance declarations:
-      type instance OverA.D [Int] [a] -- Defined at OverB.hs:9:15
-      type instance OverA.D [a] [Int] -- Defined at OverC.hs:9:15
+      OverA.D [Int] [a] -- Defined at OverB.hs:9:15
+      OverA.D [a] [Int] -- Defined at OverC.hs:9:15
diff --git a/tests/indexed-types/should_fail/Overlap10.hs b/tests/indexed-types/should_fail/Overlap10.hs
new file mode 100644
index 000000000..25fca9a72
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap10.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Overlap10 where
+
+type family F a b
+type instance where
+  F a a = Int
+  F a b = b
+
+g :: F a Bool
+g = False
+
+
+
+
diff --git a/tests/indexed-types/should_fail/Overlap10.stderr b/tests/indexed-types/should_fail/Overlap10.stderr
new file mode 100644
index 000000000..c8f68bad9
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap10.stderr
@@ -0,0 +1,7 @@
+
+Overlap10.hs:11:5:
+    Couldn't match expected type `F a Bool' with actual type `Bool'
+    Relevant bindings include
+      g :: F a Bool (bound at Overlap10.hs:11:1)
+    In the expression: False
+    In an equation for `g': g = False
diff --git a/tests/indexed-types/should_fail/Overlap11.hs b/tests/indexed-types/should_fail/Overlap11.hs
new file mode 100644
index 000000000..f10375958
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap11.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Overlap11 where
+
+type family F a b
+type instance where
+  F a a = Int
+  F a b = b
+
+g :: F a Int
+g = (5 :: Int)
+
+
+
+
diff --git a/tests/indexed-types/should_fail/Overlap11.stderr b/tests/indexed-types/should_fail/Overlap11.stderr
new file mode 100644
index 000000000..0d657dac8
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap11.stderr
@@ -0,0 +1,6 @@
+
+Overlap11.hs:11:6:
+    Couldn't match expected type `F a Int' with actual type `Int'
+    Relevant bindings include g :: F a Int (bound at Overlap11.hs:11:1)
+    In the expression: (5 :: Int)
+    In an equation for `g': g = (5 :: Int)
diff --git a/tests/indexed-types/should_fail/Overlap3.hs b/tests/indexed-types/should_fail/Overlap3.hs
new file mode 100644
index 000000000..654d62690
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap3.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Overlap3 where
+
+type family F a b
+type instance where
+  F a a = Int
+  F a b = Bool
+type instance F Char Char = Int
+
+g :: F Char Double
+g = False
+
+h :: F Double Double
+h = -2
diff --git a/tests/indexed-types/should_fail/Overlap3.stderr b/tests/indexed-types/should_fail/Overlap3.stderr
new file mode 100644
index 000000000..7226058e1
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap3.stderr
@@ -0,0 +1,10 @@
+
+Overlap3.hs:7:3:
+    Conflicting family instance declarations:
+      F a a -- Defined at Overlap3.hs:7:3
+      F Char Char -- Defined at Overlap3.hs:9:15
+
+Overlap3.hs:8:3:
+    Conflicting family instance declarations:
+      F a b -- Defined at Overlap3.hs:8:3
+      F Char Char -- Defined at Overlap3.hs:9:15
diff --git a/tests/indexed-types/should_fail/Overlap4.hs b/tests/indexed-types/should_fail/Overlap4.hs
new file mode 100644
index 000000000..4f1b872b9
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap4.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Overlap4 where
+
+type family F a b
+type instance F Char Char = Int
+type instance where
+  F a a = Int
+  F a b = Bool
+
+
+g :: F Char Double
+g = False
+
+h :: F Double Double
+h = -2
diff --git a/tests/indexed-types/should_fail/Overlap4.stderr b/tests/indexed-types/should_fail/Overlap4.stderr
new file mode 100644
index 000000000..fd97e9748
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap4.stderr
@@ -0,0 +1,5 @@
+
+Overlap4.hs:6:15:
+    Conflicting family instance declarations:
+      F Char Char -- Defined at Overlap4.hs:6:15
+      F a a -- Defined at Overlap4.hs:8:3
diff --git a/tests/indexed-types/should_fail/Overlap5.hs b/tests/indexed-types/should_fail/Overlap5.hs
new file mode 100644
index 000000000..fbf05d4f4
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap5.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
+
+module Overlap5 where
+
+type family And (a :: Bool) (b :: Bool) :: Bool
+type instance where
+  And False x = False
+  And True x = x
+  And x False = False
+  And x True = x
+  And x x = x
+
+data Proxy p = P
+
+g :: Proxy x -> Proxy (And x True)
+g x = x
+
+h :: Proxy x -> Proxy (And x x)
+h x = x
+
+i :: Proxy x -> Proxy (And False x)
+i x = (P :: Proxy False)
\ No newline at end of file
diff --git a/tests/indexed-types/should_fail/Overlap5.stderr b/tests/indexed-types/should_fail/Overlap5.stderr
new file mode 100644
index 000000000..329d410fd
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap5.stderr
@@ -0,0 +1,29 @@
+
+Overlap5.hs:16:7:
+    Couldn't match type `x' with `And x 'True'
+      `x' is a rigid type variable bound by
+          the type signature for
+            g :: Proxy Bool x -> Proxy Bool (And x 'True)
+          at Overlap5.hs:15:6
+    Expected type: Proxy Bool (And x 'True)
+      Actual type: Proxy Bool x
+    Relevant bindings include
+      g :: Proxy Bool x -> Proxy Bool (And x 'True)
+        (bound at Overlap5.hs:16:1)
+      x :: Proxy Bool x (bound at Overlap5.hs:16:3)
+    In the expression: x
+    In an equation for `g': g x = x
+
+Overlap5.hs:19:7:
+    Couldn't match type `x' with `And x x'
+      `x' is a rigid type variable bound by
+          the type signature for h :: Proxy Bool x -> Proxy Bool (And x x)
+          at Overlap5.hs:18:6
+    Expected type: Proxy Bool (And x x)
+      Actual type: Proxy Bool x
+    Relevant bindings include
+      h :: Proxy Bool x -> Proxy Bool (And x x)
+        (bound at Overlap5.hs:19:1)
+      x :: Proxy Bool x (bound at Overlap5.hs:19:3)
+    In the expression: x
+    In an equation for `h': h x = x
diff --git a/tests/indexed-types/should_fail/Overlap6.hs b/tests/indexed-types/should_fail/Overlap6.hs
new file mode 100644
index 000000000..c97992e65
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap6.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
+
+module Overlap6 where
+
+type family And (a :: Bool) (b :: Bool) :: Bool
+type instance where
+  And False x = False
+  And True x = False -- this is wrong!
+  And x False = False
+  And x True = x
+  And x x = x
+
+data Proxy p = P
+
+g :: Proxy x -> Proxy (And x True)
+g x = x
diff --git a/tests/indexed-types/should_fail/Overlap6.stderr b/tests/indexed-types/should_fail/Overlap6.stderr
new file mode 100644
index 000000000..8149e2d92
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap6.stderr
@@ -0,0 +1,15 @@
+
+Overlap6.hs:16:7:
+    Couldn't match type `x' with `And x 'True'
+      `x' is a rigid type variable bound by
+          the type signature for
+            g :: Proxy Bool x -> Proxy Bool (And x 'True)
+          at Overlap6.hs:15:6
+    Expected type: Proxy Bool (And x 'True)
+      Actual type: Proxy Bool x
+    Relevant bindings include
+      g :: Proxy Bool x -> Proxy Bool (And x 'True)
+        (bound at Overlap6.hs:16:1)
+      x :: Proxy Bool x (bound at Overlap6.hs:16:3)
+    In the expression: x
+    In an equation for `g': g x = x
diff --git a/tests/indexed-types/should_fail/Overlap7.hs b/tests/indexed-types/should_fail/Overlap7.hs
new file mode 100644
index 000000000..352103c4c
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap7.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Overlap7 where
+
+type family F a b
+type instance where
+  F Int a = Int
+  F a b = Bool
+type instance F a Int = Int
+
diff --git a/tests/indexed-types/should_fail/Overlap7.stderr b/tests/indexed-types/should_fail/Overlap7.stderr
new file mode 100644
index 000000000..a87186eec
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap7.stderr
@@ -0,0 +1,10 @@
+
+Overlap7.hs:7:3:
+    Conflicting family instance declarations:
+      F Int a -- Defined at Overlap7.hs:7:3
+      F a Int -- Defined at Overlap7.hs:9:15
+
+Overlap7.hs:8:3:
+    Conflicting family instance declarations:
+      F a b -- Defined at Overlap7.hs:8:3
+      F a Int -- Defined at Overlap7.hs:9:15
diff --git a/tests/indexed-types/should_fail/Overlap8.hs b/tests/indexed-types/should_fail/Overlap8.hs
new file mode 100644
index 000000000..b998d2661
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap8.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Overlap8 where
+
+type family F a b
+type instance F a Int = Int
+type instance where
+  F Int a = Int
+  F a b = Bool
+
+
diff --git a/tests/indexed-types/should_fail/Overlap8.stderr b/tests/indexed-types/should_fail/Overlap8.stderr
new file mode 100644
index 000000000..9443a4636
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap8.stderr
@@ -0,0 +1,5 @@
+
+Overlap8.hs:6:15:
+    Conflicting family instance declarations:
+      F a Int -- Defined at Overlap8.hs:6:15
+      F Int a -- Defined at Overlap8.hs:8:3
diff --git a/tests/indexed-types/should_fail/Overlap9.hs b/tests/indexed-types/should_fail/Overlap9.hs
new file mode 100644
index 000000000..61d1dff72
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap9.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Overlap9 where
+
+type family F a
+type instance where
+  F Int = Bool
+  F a   = Int
+
+g :: Show a => a -> F a
+g x = length (show x)
+
+
+
diff --git a/tests/indexed-types/should_fail/Overlap9.stderr b/tests/indexed-types/should_fail/Overlap9.stderr
new file mode 100644
index 000000000..d70a76c8e
--- /dev/null
+++ b/tests/indexed-types/should_fail/Overlap9.stderr
@@ -0,0 +1,12 @@
+
+Overlap9.hs:11:7:
+    Could not deduce (F a ~ Int)
+    from the context (Show a)
+      bound by the type signature for g :: Show a => a -> F a
+      at Overlap9.hs:10:6-23
+    Relevant bindings include
+      g :: a -> F a (bound at Overlap9.hs:11:1)
+      x :: a (bound at Overlap9.hs:11:3)
+    In the return type of a call of `length'
+    In the expression: length (show x)
+    In an equation for `g': g x = length (show x)
diff --git a/tests/indexed-types/should_fail/SimpleFail11a.stderr b/tests/indexed-types/should_fail/SimpleFail11a.stderr
index e9615eddc..2e6b9570e 100644
--- a/tests/indexed-types/should_fail/SimpleFail11a.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail11a.stderr
@@ -1,10 +1,10 @@
 
 SimpleFail11a.hs:6:15:
     Conflicting family instance declarations:
-      data instance C9 Int Int -- Defined at SimpleFail11a.hs:6:15
-      data instance C9 Int Int -- Defined at SimpleFail11a.hs:8:15
+      C9 Int Int -- Defined at SimpleFail11a.hs:6:15
+      C9 Int Int -- Defined at SimpleFail11a.hs:8:15
 
 SimpleFail11a.hs:11:15:
     Conflicting family instance declarations:
-      type instance D9 Int Int -- Defined at SimpleFail11a.hs:11:15
-      type instance D9 Int Int -- Defined at SimpleFail11a.hs:13:15
+      D9 Int Int -- Defined at SimpleFail11a.hs:11:15
+      D9 Int Int -- Defined at SimpleFail11a.hs:13:15
diff --git a/tests/indexed-types/should_fail/SimpleFail11b.stderr b/tests/indexed-types/should_fail/SimpleFail11b.stderr
index 297a18c5d..6994b9bcd 100644
--- a/tests/indexed-types/should_fail/SimpleFail11b.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail11b.stderr
@@ -1,10 +1,10 @@
 
 SimpleFail11b.hs:7:15:
     Conflicting family instance declarations:
-      data instance C9 [a] Int -- Defined at SimpleFail11b.hs:7:15
-      data instance C9 [a] Int -- Defined at SimpleFail11b.hs:9:15
+      C9 [a] Int -- Defined at SimpleFail11b.hs:7:15
+      C9 [a] Int -- Defined at SimpleFail11b.hs:9:15
 
 SimpleFail11b.hs:13:15:
     Conflicting family instance declarations:
-      type instance D9 [a] Int -- Defined at SimpleFail11b.hs:13:15
-      type instance D9 [a] Int -- Defined at SimpleFail11b.hs:15:15
+      D9 [a] Int -- Defined at SimpleFail11b.hs:13:15
+      D9 [a] Int -- Defined at SimpleFail11b.hs:15:15
diff --git a/tests/indexed-types/should_fail/SimpleFail11c.stderr b/tests/indexed-types/should_fail/SimpleFail11c.stderr
index 39870055e..a323efa25 100644
--- a/tests/indexed-types/should_fail/SimpleFail11c.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail11c.stderr
@@ -1,10 +1,10 @@
 
 SimpleFail11c.hs:7:15:
     Conflicting family instance declarations:
-      data instance C9 [a] Int -- Defined at SimpleFail11c.hs:7:15
-      data instance C9 [Int] Int -- Defined at SimpleFail11c.hs:9:15
+      C9 [a] Int -- Defined at SimpleFail11c.hs:7:15
+      C9 [Int] Int -- Defined at SimpleFail11c.hs:9:15
 
 SimpleFail11c.hs:13:15:
     Conflicting family instance declarations:
-      type instance D9 [a] Int -- Defined at SimpleFail11c.hs:13:15
-      type instance D9 [Int] Int -- Defined at SimpleFail11c.hs:15:15
+      D9 [a] Int -- Defined at SimpleFail11c.hs:13:15
+      D9 [Int] Int -- Defined at SimpleFail11c.hs:15:15
diff --git a/tests/indexed-types/should_fail/SimpleFail11d.stderr b/tests/indexed-types/should_fail/SimpleFail11d.stderr
index 062d29d8f..72a9f7945 100644
--- a/tests/indexed-types/should_fail/SimpleFail11d.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail11d.stderr
@@ -1,5 +1,5 @@
 
 SimpleFail11d.hs:8:15:
     Conflicting family instance declarations:
-      data instance C9 [Int] [a] -- Defined at SimpleFail11d.hs:8:15
-      data instance C9 [a] [Int] -- Defined at SimpleFail11d.hs:10:15
+      C9 [Int] [a] -- Defined at SimpleFail11d.hs:8:15
+      C9 [a] [Int] -- Defined at SimpleFail11d.hs:10:15
diff --git a/tests/indexed-types/should_fail/SimpleFail12.stderr b/tests/indexed-types/should_fail/SimpleFail12.stderr
index 09420061a..93eabd618 100644
--- a/tests/indexed-types/should_fail/SimpleFail12.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail12.stderr
@@ -1,4 +1,4 @@
 
-SimpleFail12.hs:8:1:
+SimpleFail12.hs:8:15:
     Illegal polymorphic or qualified type: forall a. [a]
     In the type instance declaration for `C'
diff --git a/tests/indexed-types/should_fail/SimpleFail13.stderr b/tests/indexed-types/should_fail/SimpleFail13.stderr
index 116da4c0f..a927fec6f 100644
--- a/tests/indexed-types/should_fail/SimpleFail13.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail13.stderr
@@ -3,6 +3,6 @@ SimpleFail13.hs:9:1:
     Illegal type synonym family application in instance: [C a]
     In the data instance declaration for `D'
 
-SimpleFail13.hs:13:1:
+SimpleFail13.hs:13:15:
     Illegal type synonym family application in instance: [C a]
     In the type instance declaration for `E'
diff --git a/tests/indexed-types/should_fail/SimpleFail2a.stderr b/tests/indexed-types/should_fail/SimpleFail2a.stderr
index 67d9d24da..5769e4784 100644
--- a/tests/indexed-types/should_fail/SimpleFail2a.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail2a.stderr
@@ -1,6 +1,11 @@
-
-SimpleFail2a.hs:11:3:
-    Type indexes must match class instance head
-    Found `a' but expected `Int'
-    In the data instance declaration for `Sd'
-    In the instance declaration for `C Int'
+
+SimpleFail2a.hs:11:11:
+    Type indexes must match class instance head
+    Found `a' but expected `Int'
+    In the data declaration for `Sd'
+    In the instance declaration for `C Int'
+
+SimpleFail2a.hs:11:11:
+    Conflicting family instance declarations:
+      Sd a -- Defined at SimpleFail2a.hs:11:11
+      Sd Int -- Defined at SimpleFail2a.hs:12:11
diff --git a/tests/indexed-types/should_fail/SimpleFail2b.stderr b/tests/indexed-types/should_fail/SimpleFail2b.stderr
index 119fec014..1b63dfe3f 100644
--- a/tests/indexed-types/should_fail/SimpleFail2b.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail2b.stderr
@@ -1,5 +1,5 @@
 
 SimpleFail2b.hs:9:11:
     Conflicting family instance declarations:
-      data Sd Int -- Defined at SimpleFail2b.hs:9:11
-      data Sd Int -- Defined at SimpleFail2b.hs:10:11
+      Sd Int -- Defined at SimpleFail2b.hs:9:11
+      Sd Int -- Defined at SimpleFail2b.hs:10:11
diff --git a/tests/indexed-types/should_fail/SimpleFail4.stderr b/tests/indexed-types/should_fail/SimpleFail4.stderr
index 71164f74c..1eca808bd 100644
--- a/tests/indexed-types/should_fail/SimpleFail4.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail4.stderr
@@ -1,5 +1,5 @@
 
-SimpleFail4.hs:8:3:
+SimpleFail4.hs:8:8:
     Type indexes must match class instance head
     Found `Int' but expected `a'
     In the type synonym instance default declaration for `S2'
diff --git a/tests/indexed-types/should_fail/SimpleFail9.stderr b/tests/indexed-types/should_fail/SimpleFail9.stderr
index fb75e60bc..4eecbde7f 100644
--- a/tests/indexed-types/should_fail/SimpleFail9.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail9.stderr
@@ -1,6 +1,6 @@
-
-SimpleFail9.hs:13:3:
-    Type indexes must match class instance head
-    Found `(b, Int)' but expected `(a, Int)'
-    In the data instance declaration for `S7'
-    In the instance declaration for `C7 Char (a, Int)'
+
+SimpleFail9.hs:13:8:
+    Type indexes must match class instance head
+    Found `(b, Int)' but expected `(a, Int)'
+    In the data declaration for `S7'
+    In the instance declaration for `C7 Char (a, Int)'
diff --git a/tests/indexed-types/should_fail/T2157.stderr b/tests/indexed-types/should_fail/T2157.stderr
index d9e11c26d..44f0a2436 100644
--- a/tests/indexed-types/should_fail/T2157.stderr
+++ b/tests/indexed-types/should_fail/T2157.stderr
@@ -1,4 +1,4 @@
 
-T2157.hs:7:1:
+T2157.hs:7:15:
     Type synonym `S' should have 2 arguments, but has been given 1
     In the type instance declaration for `F'
diff --git a/tests/indexed-types/should_fail/T2334.stderr b/tests/indexed-types/should_fail/T2334.stderr
index deceb4875..b8efc5938 100644
--- a/tests/indexed-types/should_fail/T2334.stderr
+++ b/tests/indexed-types/should_fail/T2334.stderr
@@ -13,5 +13,5 @@ T2334.hs:10:27:
 
 T2334.hs:12:15:
     Conflicting family instance declarations:
-      data instance F Bool -- Defined at T2334.hs:12:15
-      data instance F Bool -- Defined at T2334.hs:13:15
+      F Bool -- Defined at T2334.hs:12:15
+      F Bool -- Defined at T2334.hs:13:15
diff --git a/tests/indexed-types/should_fail/T2677.stderr b/tests/indexed-types/should_fail/T2677.stderr
index d160b2a89..fcc6f8aaf 100644
--- a/tests/indexed-types/should_fail/T2677.stderr
+++ b/tests/indexed-types/should_fail/T2677.stderr
@@ -1,5 +1,5 @@
 
 T2677.hs:6:15:
     Conflicting family instance declarations:
-      type instance A a -- Defined at T2677.hs:6:15
-      type instance A Int -- Defined at T2677.hs:7:15
+      A a -- Defined at T2677.hs:6:15
+      A Int -- Defined at T2677.hs:7:15
diff --git a/tests/indexed-types/should_fail/T3330b.stderr b/tests/indexed-types/should_fail/T3330b.stderr
index 6c00e2f93..5f06978d1 100644
--- a/tests/indexed-types/should_fail/T3330b.stderr
+++ b/tests/indexed-types/should_fail/T3330b.stderr
@@ -1,5 +1,5 @@
 
 T3330b.hs:14:10:
     Conflicting family instance declarations:
-      type Res c a b -- Defined at T3330b.hs:14:10
-      type Res [c] a b -- Defined at T3330b.hs:18:10
+      Res c a b -- Defined at T3330b.hs:14:10
+      Res [c] a b -- Defined at T3330b.hs:18:10
diff --git a/tests/indexed-types/should_fail/T4246.stderr b/tests/indexed-types/should_fail/T4246.stderr
index 14bd8ba40..26e967a67 100644
--- a/tests/indexed-types/should_fail/T4246.stderr
+++ b/tests/indexed-types/should_fail/T4246.stderr
@@ -1,10 +1,10 @@
 
 T4246.hs:8:9:
     Conflicting family instance declarations:
-      type F a -- Defined at T4246.hs:8:9
-      type F Int -- Defined at T4246.hs:11:9
+      F a -- Defined at T4246.hs:8:9
+      F Int -- Defined at T4246.hs:11:9
 
 T4246.hs:14:15:
     Conflicting family instance declarations:
-      type instance G Int -- Defined at T4246.hs:14:15
-      type instance G Int -- Defined at T4246.hs:15:15
+      G Int -- Defined at T4246.hs:14:15
+      G Int -- Defined at T4246.hs:15:15
diff --git a/tests/indexed-types/should_fail/T5515.stderr b/tests/indexed-types/should_fail/T5515.stderr
index e1d7979d7..535048d88 100644
--- a/tests/indexed-types/should_fail/T5515.stderr
+++ b/tests/indexed-types/should_fail/T5515.stderr
@@ -1,8 +1,8 @@
 
-T5515.hs:9:3:
+T5515.hs:9:8:
     The RHS of an associated type declaration mentions type variable `a'
       All such variables must be bound on the LHS
 
-T5515.hs:15:3:
+T5515.hs:15:8:
     The RHS of an associated type declaration mentions type variable `a'
       All such variables must be bound on the LHS
diff --git a/tests/indexed-types/should_fail/TyFamArity1.stderr b/tests/indexed-types/should_fail/TyFamArity1.stderr
index f92f986d2..b0076287f 100644
--- a/tests/indexed-types/should_fail/TyFamArity1.stderr
+++ b/tests/indexed-types/should_fail/TyFamArity1.stderr
@@ -1,4 +1,4 @@
 
-TyFamArity1.hs:4:1:
+TyFamArity1.hs:4:15:
     Number of parameters must match family declaration; expected 2
     In the type instance declaration for `T'
diff --git a/tests/indexed-types/should_fail/TyFamArity2.stderr b/tests/indexed-types/should_fail/TyFamArity2.stderr
index 2423a065b..ad71adc7d 100644
--- a/tests/indexed-types/should_fail/TyFamArity2.stderr
+++ b/tests/indexed-types/should_fail/TyFamArity2.stderr
@@ -1,4 +1,4 @@
 
-TyFamArity2.hs:4:1:
+TyFamArity2.hs:4:15:
     Number of parameters must match family declaration; expected 1
     In the type instance declaration for `T'
diff --git a/tests/indexed-types/should_fail/TyFamUndec.stderr b/tests/indexed-types/should_fail/TyFamUndec.stderr
index 2b8825ac3..6bb2af771 100644
--- a/tests/indexed-types/should_fail/TyFamUndec.stderr
+++ b/tests/indexed-types/should_fail/TyFamUndec.stderr
@@ -1,17 +1,17 @@
 
-TyFamUndec.hs:6:1:
+TyFamUndec.hs:6:15:
     Variable `b' occurs more often than in the instance head
       in the type family application: T (b, b)
     (Use -XUndecidableInstances to permit this)
     In the type instance declaration for `T'
 
-TyFamUndec.hs:7:1:
+TyFamUndec.hs:7:15:
     Application is no smaller than the instance head
       in the type family application: T (a, Maybe b)
     (Use -XUndecidableInstances to permit this)
     In the type instance declaration for `T'
 
-TyFamUndec.hs:8:1:
+TyFamUndec.hs:8:15:
     Nested type family application
       in the type family application: T (a, T b)
     (Use -XUndecidableInstances to permit this)
diff --git a/tests/indexed-types/should_fail/all.T b/tests/indexed-types/should_fail/all.T
index 820fe7de5..eaf1b1970 100644
--- a/tests/indexed-types/should_fail/all.T
+++ b/tests/indexed-types/should_fail/all.T
@@ -77,6 +77,16 @@ test('T5934', normal, compile_fail, [''])
 test('T6123', normal, compile_fail, [''])
 test('ExtraTcsUntch', normal, compile_fail, [''])
 test('T7010', normal, compile_fail, [''])
+
+test('Overlap3', normal, compile_fail, [''])
+test('Overlap4', normal, compile_fail, [''])
+test('Overlap5', normal, compile_fail, [''])
+test('Overlap6', normal, compile_fail, [''])
+test('Overlap7', normal, compile_fail, [''])
+test('Overlap8', normal, compile_fail, [''])
+test('Overlap9', normal, compile_fail, [''])
+test('Overlap10', normal, compile_fail, [''])
+test('Overlap11', normal, compile_fail, [''])
 test('T7194', normal, compile_fail, [''])
 test('T7354', normal, compile_fail, [''])
 test('T7354a',
diff --git a/tests/simplCore/should_compile/Makefile b/tests/simplCore/should_compile/Makefile
index 1026363ff..1c2372db6 100644
--- a/tests/simplCore/should_compile/Makefile
+++ b/tests/simplCore/should_compile/Makefile
@@ -29,7 +29,7 @@ T4306:
 T4201:
 	$(RM) -f T4201.hi T4201.o
 	'$(TEST_HC)' $(TEST_HC_OPTS) -c -O T4201.hs 
-	'$(TEST_HC)' $(TEST_HC_OPTS) --show-iface T4201.hi | grep 'Sym'
+	'$(TEST_HC)' $(TEST_HC_OPTS) --show-iface T4201.hi | grep -B2 'Sym'
 
 # This one looped as a result of bogus specialisation
 T4903:
diff --git a/tests/simplCore/should_compile/T4201.stdout b/tests/simplCore/should_compile/T4201.stdout
index e1808560d..c3b7e8d26 100644
--- a/tests/simplCore/should_compile/T4201.stdout
+++ b/tests/simplCore/should_compile/T4201.stdout
@@ -1 +1,3 @@
-       Unfolding: (Eta.bof `cast` (Sym (Eta.NTCo:Foo) -> Refl Eta.T)) -}
+       Unfolding: (Eta.bof
+                     `cast`
+                   (Sym (Eta.NTCo:Foo[0]) -> Refl Eta.T)) -}
diff --git a/tests/th/T5886a.hs b/tests/th/T5886a.hs
index 4c6f433b5..74db6fa19 100644
--- a/tests/th/T5886a.hs
+++ b/tests/th/T5886a.hs
@@ -11,4 +11,4 @@ class C α where
 
 bang ∷ DecsQ
 bang = return [InstanceD [] (AppT (ConT ''C) (ConT ''Int))
-                [TySynInstD ''AT [ConT ''Int] (ConT ''Int)]]
+                [TySynInstD ''AT [TySynEqn [ConT ''Int] (ConT ''Int)]]]
diff --git a/tests/th/TH_TyInstWhere1.hs b/tests/th/TH_TyInstWhere1.hs
new file mode 100644
index 000000000..8352d4bf0
--- /dev/null
+++ b/tests/th/TH_TyInstWhere1.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE PolyKinds, DataKinds, TemplateHaskell, TypeFamilies #-}
+
+module TH_TyInstWhere1 where
+
+type family F (a :: k) (b :: k) :: Bool
+
+$([d| type instance where
+        F a a = True
+        F a b = False |])
+
+data Proxy a = P
+
+f :: Proxy True -> Proxy (F Int Int)
+f x = x
+
+g :: Proxy False -> Proxy (F Int Bool)
+g x = x 
\ No newline at end of file
diff --git a/tests/th/TH_TyInstWhere1.stderr b/tests/th/TH_TyInstWhere1.stderr
new file mode 100644
index 000000000..480e5bf4f
--- /dev/null
+++ b/tests/th/TH_TyInstWhere1.stderr
@@ -0,0 +1,9 @@
+TH_TyInstWhere1.hs:1:1: Splicing declarations
+    [d| type instance where
+          F a a = True
+          F a b = False |]
+  ======>
+    TH_TyInstWhere1.hs:(7,3)-(9,24)
+    type instance where
+      F a a = True
+      F a b = False
diff --git a/tests/th/TH_TyInstWhere2.hs b/tests/th/TH_TyInstWhere2.hs
new file mode 100644
index 000000000..ec27ced78
--- /dev/null
+++ b/tests/th/TH_TyInstWhere2.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE PolyKinds, DataKinds, TemplateHaskell, TypeFamilies #-}
+
+module TH_TyInstWhere2 where
+
+import Language.Haskell.TH
+
+type family F (a :: k) (b :: k) :: Bool
+
+$( do { decs <- [d| type instance where
+                      F a a = True
+                      F a b = False |]
+      ; reportWarning (pprint decs)
+      ; return [] })
+
+
diff --git a/tests/th/TH_TyInstWhere2.stderr b/tests/th/TH_TyInstWhere2.stderr
new file mode 100644
index 000000000..4ed490e8e
--- /dev/null
+++ b/tests/th/TH_TyInstWhere2.stderr
@@ -0,0 +1,5 @@
+
+TH_TyInstWhere2.hs:9:4: Warning:
+    type instance where
+    TH_TyInstWhere2.F a_0 a_0 = 'GHC.Types.True
+    TH_TyInstWhere2.F a_1 b_2 = 'GHC.Types.False
diff --git a/tests/th/TH_TyInstWhere3.hs b/tests/th/TH_TyInstWhere3.hs
new file mode 100644
index 000000000..54d76f522
--- /dev/null
+++ b/tests/th/TH_TyInstWhere3.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE PolyKinds, DataKinds, TemplateHaskell, TypeFamilies #-}
+
+module TH_TyInstWhere3 where
+
+import Language.Haskell.TH
+
+type family F a
+
+$( do { decs <- [d| type instance where
+                      F Int = Int |]
+      ; reportWarning (pprint decs)
+      ; return decs })
+
+type instance F a = a 
+
+-- When this test was written, TH considered all singleton type family instance
+-- as unbranched. Thus, even though the two instances above would not play nicely
+-- without TH, they should be fine with TH.
diff --git a/tests/th/TH_TyInstWhere3.stderr b/tests/th/TH_TyInstWhere3.stderr
new file mode 100644
index 000000000..eaebfec89
--- /dev/null
+++ b/tests/th/TH_TyInstWhere3.stderr
@@ -0,0 +1,3 @@
+
+TH_TyInstWhere3.hs:9:4: Warning:
+    type instance TH_TyInstWhere3.F GHC.Types.Int = GHC.Types.Int
diff --git a/tests/th/TH_TyInstWhere4.hs b/tests/th/TH_TyInstWhere4.hs
new file mode 100644
index 000000000..86415ffd5
--- /dev/null
+++ b/tests/th/TH_TyInstWhere4.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE PolyKinds, DataKinds, TemplateHaskell, TypeFamilies #-}
+
+module TH_TyInstWhere4 where
+
+import Language.Haskell.TH
+
+type family F a b :: Bool
+type instance where
+  F a a = True
+  F a b = False
+
+$( do { info1 <- reify ''F
+      ; reportWarning (pprint info1)
+      ; info2 <- reifyInstances ''F [ConT ''Int, ConT ''Int]
+      ; reportWarning (pprint info2)
+      ; info3 <- reifyInstances ''F [ConT ''Int, ConT ''Bool]
+      ; reportWarning (pprint info3)
+      ; return [] })
+
+
diff --git a/tests/th/TH_TyInstWhere4.stderr b/tests/th/TH_TyInstWhere4.stderr
new file mode 100644
index 000000000..70dfe85b7
--- /dev/null
+++ b/tests/th/TH_TyInstWhere4.stderr
@@ -0,0 +1,16 @@
+
+TH_TyInstWhere4.hs:12:4: Warning:
+    type family TH_TyInstWhere4.F a_0 b_1 :: * -> * -> GHC.Types.Bool
+type instance where
+    TH_TyInstWhere4.F a_2 a_2 = GHC.Types.True
+    TH_TyInstWhere4.F a_3 b_4 = GHC.Types.False
+
+TH_TyInstWhere4.hs:12:4: Warning:
+    type instance where
+    TH_TyInstWhere4.F a_0 a_0 = GHC.Types.True
+    TH_TyInstWhere4.F a_1 b_2 = GHC.Types.False
+
+TH_TyInstWhere4.hs:12:4: Warning:
+    type instance where
+    TH_TyInstWhere4.F a_0 a_0 = GHC.Types.True
+    TH_TyInstWhere4.F a_1 b_2 = GHC.Types.False
diff --git a/tests/th/all.T b/tests/th/all.T
index 78e76553a..1a97cff27 100644
--- a/tests/th/all.T
+++ b/tests/th/all.T
@@ -255,6 +255,11 @@ test('T7092', extra_clean(['T7092a.hi','T7092a.o']),
 test('T7276', normal, compile_fail, ['-v0'])
 test('T7276a', combined_output, ghci_script, ['T7276a.script'])
 
+test('TH_TyInstWhere1', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
+test('TH_TyInstWhere2', normal, compile, ['-v0'])
+test('TH_TyInstWhere3', normal, compile, ['-v0'])
+test('TH_TyInstWhere4', normal, compile, ['-v0'])
+
 test('T7445', extra_clean(['T7445a.hi', 'T7445a.o']),
 	      run_command,
 	      ['$MAKE -s --no-print-directory T7445'] )
diff --git a/tests/typecheck/should_compile/T5481.stderr b/tests/typecheck/should_compile/T5481.stderr
index 34eb747a8..c88aecbca 100644
--- a/tests/typecheck/should_compile/T5481.stderr
+++ b/tests/typecheck/should_compile/T5481.stderr
@@ -1,8 +1,8 @@
 
-T5481.hs:6:5:
+T5481.hs:6:10:
     The RHS of an associated type declaration mentions type variable `b'
       All such variables must be bound on the LHS
 
-T5481.hs:8:5:
+T5481.hs:8:10:
     The RHS of an associated type declaration mentions type variable `a'
       All such variables must be bound on the LHS
diff --git a/tests/typecheck/should_compile/tc231.stderr b/tests/typecheck/should_compile/tc231.stderr
index 72f0c2007..0e9196c3f 100644
--- a/tests/typecheck/should_compile/tc231.stderr
+++ b/tests/typecheck/should_compile/tc231.stderr
@@ -1,29 +1,29 @@
-TYPE SIGNATURES
-  foo ::
-    forall s b chain.
-    Zork s (Z [Char]) b =>
-    Q s (Z [Char]) chain -> ST s ()
-  s :: forall t t1. Q t (Z [Char]) t1 -> Q t (Z [Char]) t1
-TYPE CONSTRUCTORS
-  Q :: * -> * -> * -> *
-  data Q s a chain
-      No C type associated
-      RecFlag NonRecursive
-      = Node :: forall s a chain. s -> a -> chain -> Q s a chain
-            Stricts: _ _ _
-      FamilyInstance: none
-  Z :: * -> *
-  data Z a
-      No C type associated
-      RecFlag NonRecursive
-      = Z :: forall a. a -> Z a Stricts: _
-      FamilyInstance: none
-  Zork :: * -> * -> * -> Constraint
-  class Zork s a b | a -> b
-      RecFlag NonRecursive
-      huh :: forall chain. Q s a chain -> ST s ()
-COERCION AXIOMS
-  axiom ShouldCompile.NTCo:Zork s a b
-    :: Zork s a b ~# (forall chain. Q s a chain -> ST s ())
-Dependent modules: []
-Dependent packages: [base, ghc-prim, integer-gmp]
+TYPE SIGNATURES
+  foo ::
+    forall s b chain.
+    Zork s (Z [Char]) b =>
+    Q s (Z [Char]) chain -> ST s ()
+  s :: forall t t1. Q t (Z [Char]) t1 -> Q t (Z [Char]) t1
+TYPE CONSTRUCTORS
+  Q :: * -> * -> * -> *
+  data Q s a chain
+      No C type associated
+      RecFlag NonRecursive
+      = Node :: forall s a chain. s -> a -> chain -> Q s a chain
+            Stricts: _ _ _
+      FamilyInstance: none
+  Z :: * -> *
+  data Z a
+      No C type associated
+      RecFlag NonRecursive
+      = Z :: forall a. a -> Z a Stricts: _
+      FamilyInstance: none
+  Zork :: * -> * -> * -> Constraint
+  class Zork s a b | a -> b
+      RecFlag NonRecursive
+      huh :: forall chain. Q s a chain -> ST s ()
+COERCION AXIOMS
+  axiom ShouldCompile.NTCo:Zork ::
+    forall s a b. Zork s a b ~# (forall chain. Q s a chain -> ST s ())
+Dependent modules: []
+Dependent packages: [base, ghc-prim, integer-gmp]
diff --git a/tests/typecheck/should_fail/AssocTyDef02.stderr b/tests/typecheck/should_fail/AssocTyDef02.stderr
index 93832ed3e..920ae0acd 100644
--- a/tests/typecheck/should_fail/AssocTyDef02.stderr
+++ b/tests/typecheck/should_fail/AssocTyDef02.stderr
@@ -1,5 +1,5 @@
 
-AssocTyDef02.hs:6:5:
+AssocTyDef02.hs:6:10:
     Type indexes must match class instance head
     Found `b' but expected `a'
     In the type synonym instance default declaration for `Typ'
diff --git a/tests/typecheck/should_fail/AssocTyDef05.stderr b/tests/typecheck/should_fail/AssocTyDef05.stderr
index 3416a3c44..797c83891 100644
--- a/tests/typecheck/should_fail/AssocTyDef05.stderr
+++ b/tests/typecheck/should_fail/AssocTyDef05.stderr
@@ -1,5 +1,5 @@
-
-AssocTyDef05.hs:6:5:
-    Number of parameters must match family declaration; expected 1
-    In the type instance declaration for `Typ'
-    In the class declaration for `Cls'
+
+AssocTyDef05.hs:6:10:
+    Number of parameters must match family declaration; expected 1
+    In the type instance declaration for `Typ'
+    In the class declaration for `Cls'
diff --git a/tests/typecheck/should_fail/AssocTyDef06.stderr b/tests/typecheck/should_fail/AssocTyDef06.stderr
index dd88bc3c1..6100ef2a9 100644
--- a/tests/typecheck/should_fail/AssocTyDef06.stderr
+++ b/tests/typecheck/should_fail/AssocTyDef06.stderr
@@ -1,5 +1,5 @@
-
-AssocTyDef06.hs:6:5:
-    Number of parameters must match family declaration; expected 1
-    In the type instance declaration for `Typ'
-    In the class declaration for `Cls'
+
+AssocTyDef06.hs:6:10:
+    Number of parameters must match family declaration; expected 1
+    In the type instance declaration for `Typ'
+    In the class declaration for `Cls'