Taming the Kind Inference Monster

My original goal was (Trac #15809) to move towards using level numbers
as the basis for deciding which type variables to generalise, rather
than searching for the free varaibles of the environment.  However
it has turned into a truly major refactoring of the kind inference
engine.

Let's deal with the level-numbers part first:

* Augment quantifyTyVars to calculate the type variables to
  quantify using level numbers, and compare the result with
  the existing approach.  That is; no change in behaviour,
  just a WARNing if the two approaches give different answers.

* To do this I had to get the level number right when calling
  quantifyTyVars, and this entailed a bit of care, especially
  in the code for kind-checking type declarations.

* However, on the way I was able to eliminate or simplify
  a number of calls to solveEqualities.

This work is incomplete: I'm not /using/ level numbers yet.
When I subsequently get rid of any remaining WARNings in
quantifyTyVars, that the level-number answers differ from
the current answers, then I can rip out the current
"free vars of the environment" stuff.

Anyway, this led me into deep dive into kind inference for type and
class declarations, which is an increasingly soggy part of GHC.
Richard already did some good work recently in

   commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3
   Date:   Thu Sep 13 09:56:02 2018 +0200

    Finish fix for #14880.

    The real change that fixes the ticket is described in
    Note [Naughty quantification candidates] in TcMType.

but I kept turning over stones. So this patch has ended up
with a pretty significant refactoring of that code too.

Kind inference for types and classes
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

* Major refactoring in the way we generalise the inferred kind of
  a TyCon, in kcTyClGroup.  Indeed, I made it into a new top-level
  function, generaliseTcTyCon.  Plus a new Note to explain it
  Note [Inferring kinds for type declarations].

* We decided (Trac #15592) not to treat class type variables specially
  when dealing with Inferred/Specified/Required for associated types.
  That simplifies things quite a bit. I also rewrote
  Note [Required, Specified, and Inferred for types]

* Major refactoring of the crucial function kcLHsQTyVars:
  I split it into
       kcLHsQTyVars_Cusk  and  kcLHsQTyVars_NonCusk
  because the two are really quite different. The CUSK case is
  almost entirely rewritten, and is much easier because of our new
  decision not to treat the class variables specially

* I moved all the error checks from tcTyClTyVars (which was a bizarre
  place for it) into generaliseTcTyCon and/or the CUSK case of
  kcLHsQTyVars.  Now tcTyClTyVars is extremely simple.

* I got rid of all the all the subtleties in tcImplicitTKBndrs. Indeed
  now there is no difference between tcImplicitTKBndrs and
  kcImplicitTKBndrs; there is now a single bindImplicitTKBndrs.
  Same for kc/tcExplicitTKBndrs.  None of them monkey with level
  numbers, nor build implication constraints.  scopeTyVars is gone
  entirely, as is kcLHsQTyVarBndrs. It's vastly simpler.

  I found I could get rid of kcLHsQTyVarBndrs entirely, in favour of
  the bnew bindExplicitTKBndrs.

Quantification
~~~~~~~~~~~~~~
* I now deal with the "naughty quantification candidates"
  of the previous patch in candidateQTyVars, rather than in
  quantifyTyVars; see Note [Naughty quantification candidates]
  in TcMType.

  I also killed off closeOverKindsCQTvs in favour of the same
  strategy that we use for tyCoVarsOfType: namely, close over kinds
  at the occurrences.

  And candidateQTyVars no longer needs a gbl_tvs argument.

* Passing the ContextKind, rather than the expected kind itself,
  to tc_hs_sig_type_and_gen makes it easy to allocate the expected
  result kind (when we are in inference mode) at the right level.

Type families
~~~~~~~~~~~~~~
* I did a major rewrite of the impenetrable tcFamTyPats. The result
  is vastly more comprehensible.

* I got rid of kcDataDefn entirely, quite a big function.

* I re-did the way that checkConsistentFamInst works, so
  that it allows alpha-renaming of invisible arguments.

* The interaction of kind signatures and family instances is tricky.
    Type families: see Note [Apparently-nullary families]
    Data families: see Note [Result kind signature for a data family instance]
                   and Note [Eta-reduction for data families]

* The consistent instantation of an associated type family is tricky.
  See Note [Checking consistent instantiation] and
      Note [Matching in the consistent-instantation check]
  in TcTyClsDecls.  It's now checked in TcTyClsDecls because that is
  when we have the relevant info to hand.

* I got tired of the compromises in etaExpandFamInst, so I did the
  job properly by adding a field cab_eta_tvs to CoAxBranch.
  See Coercion.etaExpandCoAxBranch.

tcInferApps and friends
~~~~~~~~~~~~~~~~~~~~~~~
* I got rid of the mysterious and horrible ClsInstInfo argument
  to tcInferApps, checkExpectedKindX, and various checkValid
  functions.  It was horrible!

* I got rid of [Type] result of tcInferApps.  This list was used
  only in tcFamTyPats, when checking the LHS of a type instance;
  and if there is a cast in the middle, the list is meaningless.
  So I made tcInferApps simpler, and moved the complexity
  (not much) to tcInferApps.

  Result: tcInferApps is now pretty comprehensible again.

* I refactored the many function in TcMType that instantiate skolems.

Smaller things

* I rejigged the error message in checkValidTelescope; I think it's
  quite a bit better now.

* checkValidType was not rejecting constraints in a kind signature
     forall (a :: Eq b => blah). blah2
  That led to further errors when we then do an ambiguity check.
  So I make checkValidType reject it more aggressively.

* I killed off quantifyConDecl, instead calling kindGeneralize
  directly.

* I fixed an outright bug in tyCoVarsOfImplic, where we were not
  colleting the tyvar of the kind of the skolems

* Renamed ClsInstInfo to AssocInstInfo, and made it into its
  own data type

* Some fiddling around with pretty-printing of family
  instances which was trickier than I thought.  I wanted
  wildcards to print as plain "_" in user messages, although
  they each need a unique identity in the CoAxBranch.

Some other oddments

* Refactoring around the trace messages from reportUnsolved.
* A bit of extra tc-tracing in TcHsSyn.commitFlexi

This patch fixes a raft of bugs, and includes tests for them.

 * #14887
 * #15740
 * #15764
 * #15789
 * #15804
 * #15817
 * #15870
 * #15874
 * #15881

38 files changed, 298 insertions, 79 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/T15711.stderr b/testsuite/tests/indexed-types/should_compile/T15711.stderr
index 1d23612cfc..2a012489e7 100644
--- a/testsuite/tests/indexed-types/should_compile/T15711.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T15711.stderr
@@ -1,7 +1,7 @@
 TYPE CONSTRUCTORS
-  C :: * -> Constraint
+  C{1} :: * -> Constraint
   type role F nominal nominal
-  F :: forall a. Maybe a -> *
+  F{2} :: forall a. Maybe a -> *
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/indexed-types/should_compile/T15740a.hs b/testsuite/tests/indexed-types/should_compile/T15740a.hs
new file mode 100644
index 0000000000..2d79a99878
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T15740a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-}
+
+module T15740a where
+
+import Data.Kind
+import Data.Proxy
+
+type family F2 :: forall k. k -> Type
+
+-- This should succeed
+type instance F2 = Proxy
+
diff --git a/testsuite/tests/indexed-types/should_compile/T15764a.hs b/testsuite/tests/indexed-types/should_compile/T15764a.hs
new file mode 100644
index 0000000000..91d348bd96
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T15764a.hs
@@ -0,0 +1,14 @@
+{-# Language PolyKinds #-}
+{-# Language TypeFamilies #-}
+{-# Language KindSignatures #-}
+{-# Language DataKinds #-}
+{-# Language MultiParamTypeClasses #-}
+
+module T15764a where
+
+import Data.Kind
+import Data.Proxy
+import GHC.TypeLits
+
+class C6 (k :: Type) (a :: k) (b :: Proxy (a :: k)) where
+ type T6 (proxy :: Proxy '(k, (b :: Proxy a)))
diff --git a/testsuite/tests/indexed-types/should_compile/T15852.stderr b/testsuite/tests/indexed-types/should_compile/T15852.stderr
index bc5fd2a72e..6908d000ab 100644
--- a/testsuite/tests/indexed-types/should_compile/T15852.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T15852.stderr
@@ -1,13 +1,14 @@
 TYPE CONSTRUCTORS
   type role DF nominal nominal nominal
-  DF :: forall k. * -> k -> *
+  DF{3} :: forall k. * -> k -> *
 COERCION AXIOMS
   axiom T15852.D:R:DFProxyProxy0 ::
-    forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j).
-      DF (Proxy c) a = T15852.R:DFProxyProxy k1 k2 c j a
-        -- Defined at T15852.hs:10:15
+    forall k1 k2 (j :: k1) (c :: k2).
+      DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c
 FAMILY INSTANCES
-  data instance DF (Proxy c) c j a
+  data instance forall k1 k2 (j :: k1) (c :: k2).
+                  DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c
+                    -- Defined at T15852.hs:10:15
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr
index 3b4361a2a5..9cf31965a4 100644
--- a/testsuite/tests/indexed-types/should_compile/T3017.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr
@@ -5,19 +5,18 @@ TYPE SIGNATURES
   test2 ::
     forall c a b. (Coll c, Num a, Num b, Elem c ~ (a, b)) => c -> c
 TYPE CONSTRUCTORS
-  Coll :: * -> Constraint
+  Coll{1} :: * -> Constraint
   type role Elem nominal
-  Elem :: * -> *
-  ListColl :: * -> *
+  Elem{1} :: * -> *
+  ListColl{1} :: * -> *
 COERCION AXIOMS
-  axiom Foo.D:R:ElemListColl ::
-    Elem (ListColl a) = a -- Defined at T3017.hs:13:9
+  axiom Foo.D:R:ElemListColl :: Elem (ListColl a) = a
 DATA CONSTRUCTORS
   L :: forall a. [a] -> ListColl a
 CLASS INSTANCES
   instance Coll (ListColl a) -- Defined at T3017.hs:12:11
 FAMILY INSTANCES
-  type Elem (ListColl a)
+  type instance Elem (ListColl a) = a -- Defined at T3017.hs:13:9
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 409e1efce1..484d843672 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -298,3 +298,5 @@ test('T15943', normal, compile, [''])
 test('T15704', normal, compile, [''])
 test('T15711', normal, compile, ['-ddump-types'])
 test('T15852', normal, compile, ['-ddump-types'])
+test('T15764a', normal, compile, [''])
+test('T15740a', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr
index ecbd7d9e79..776ee19592 100644
--- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr
@@ -1,8 +1,12 @@
 
 ExplicitForAllFams4a.hs:7:12: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
-    • In the type family declaration for ‘H’
+    • Type variable ‘b’ is bound by a forall,
+        but not used in the family instance
+    • In the equations for closed type family ‘H’
+      In the type family declaration for ‘H’
 
 ExplicitForAllFams4a.hs:8:10: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
-    • In the type family declaration for ‘H’
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
+    • In the equations for closed type family ‘H’
+      In the type family declaration for ‘H’
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
index cb5665401b..c488f45a65 100644
--- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
@@ -22,5 +22,6 @@ class C a where
 instance C Int where
   type forall a b. CT [a] (a,a)     = Float
   type forall b.   CT _ _           = Maybe b
+
   data forall a b. CD [a] (a,a)     = CD5 Float
   data forall b.   CD _ _           = CD6 (Maybe b)
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
index 0861a8a756..8e268d6301 100644
--- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
@@ -1,44 +1,107 @@
 
 ExplicitForAllFams4b.hs:7:24: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • Type variable ‘b’ is bound by a forall,
+        but not used in the family instance
     • In the type instance declaration for ‘J’
 
+ExplicitForAllFams4b.hs:7:27: error:
+    Conflicting family instance declarations:
+      J [a] = Float -- Defined at ExplicitForAllFams4b.hs:7:27
+      J _ = Maybe b -- Defined at ExplicitForAllFams4b.hs:8:27
+
 ExplicitForAllFams4b.hs:8:22: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
     • In the type instance declaration for ‘J’
 
 ExplicitForAllFams4b.hs:11:24: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
     • In the data instance declaration for ‘K’
 
+ExplicitForAllFams4b.hs:11:27: error:
+    Conflicting family instance declarations:
+      K (a, Bool) -- Defined at ExplicitForAllFams4b.hs:11:27
+      K _ -- Defined at ExplicitForAllFams4b.hs:12:27
+
 ExplicitForAllFams4b.hs:12:22: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
     • In the data instance declaration for ‘K’
 
 ExplicitForAllFams4b.hs:15:27: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
     • In the newtype instance declaration for ‘L’
 
+ExplicitForAllFams4b.hs:15:30: error:
+    Conflicting family instance declarations:
+      L (a, Bool) -- Defined at ExplicitForAllFams4b.hs:15:30
+      L _ -- Defined at ExplicitForAllFams4b.hs:16:30
+
 ExplicitForAllFams4b.hs:16:25: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
     • In the newtype instance declaration for ‘L’
 
+ExplicitForAllFams4b.hs:23:3: error:
+    • Type indexes must match class instance head
+      Expected: CT Int _
+        Actual: CT [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:23:20
+    • In the type instance declaration for ‘CT’
+      In the instance declaration for ‘C Int’
+
 ExplicitForAllFams4b.hs:23:17: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • Type variable ‘b’ is bound by a forall,
+        but not used in the family instance
+    • In the type instance declaration for ‘CT’
+      In the instance declaration for ‘C Int’
+
+ExplicitForAllFams4b.hs:23:20: error:
+    Conflicting family instance declarations:
+      CT [a] (a, a) = Float -- Defined at ExplicitForAllFams4b.hs:23:20
+      CT _ _ = Maybe b -- Defined at ExplicitForAllFams4b.hs:24:20
+
+ExplicitForAllFams4b.hs:24:3: error:
+    • Type indexes must match class instance head
+      Expected: CT Int _
+        Actual: CT _ _ -- Defined at ExplicitForAllFams4b.hs:24:20
     • In the type instance declaration for ‘CT’
       In the instance declaration for ‘C Int’
 
 ExplicitForAllFams4b.hs:24:15: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
     • In the type instance declaration for ‘CT’
       In the instance declaration for ‘C Int’
 
-ExplicitForAllFams4b.hs:25:17: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+ExplicitForAllFams4b.hs:26:3: error:
+    • Type indexes must match class instance head
+      Expected: CD Int _
+        Actual: CD [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:26:20
+    • In the data instance declaration for ‘CD’
+      In the instance declaration for ‘C Int’
+
+ExplicitForAllFams4b.hs:26:17: error:
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
+    • In the data instance declaration for ‘CD’
+      In the instance declaration for ‘C Int’
+
+ExplicitForAllFams4b.hs:26:20: error:
+    Conflicting family instance declarations:
+      CD [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:26:20
+      CD _ _ -- Defined at ExplicitForAllFams4b.hs:27:20
+
+ExplicitForAllFams4b.hs:27:3: error:
+    • Type indexes must match class instance head
+      Expected: CD Int _
+        Actual: CD _ _ -- Defined at ExplicitForAllFams4b.hs:27:20
     • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C Int’
 
-ExplicitForAllFams4b.hs:26:15: error:
-    • Explicitly quantified but not used in LHS pattern: type variable ‘b’
+ExplicitForAllFams4b.hs:27:15: error:
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
     • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C Int’
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
index cfbab576b9..eb54cf2e11 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
@@ -1,5 +1,5 @@
 
-SimpleFail13.hs:9:1: error:
+SimpleFail13.hs:9:15: error:
     • Illegal type synonym family application ‘C a’ in instance:
         D [C a]
     • In the data instance declaration for ‘D’
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs
index fc773af0ff..7d78a15baa 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs
@@ -8,7 +8,7 @@ class C a where
   type St a :: *
 
 instance C Int where
-  data    Sd a :: *   -- Looks like a nullary data instance decl
+  data    Sd a = MkSd -- :: *   -- Looks like a nullary data instance decl
   data    Sd Int = SdC Char
   newtype Sn Int = SnC Char
   type    St Int = Char
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr
index 9bd571e2b9..b21375ceb2 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr
@@ -2,6 +2,11 @@
 SimpleFail2a.hs:11:3: error:
     • Type indexes must match class instance head
       Expected: Sd Int
-        Actual: Sd a :: *
+        Actual: Sd a -- Defined at SimpleFail2a.hs:11:11
     • In the data instance declaration for ‘Sd’
       In the instance declaration for ‘C Int’
+
+SimpleFail2a.hs:11:11: error:
+    Conflicting family instance declarations:
+      Sd a -- Defined at SimpleFail2a.hs:11:11
+      Sd Int -- Defined at SimpleFail2a.hs:12:11
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs
index 9c1c4a82d2..0f20f78e95 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs
@@ -2,8 +2,10 @@
 
 module ShouldFail where
 
+import Data.Kind
+
 class C7 a b where
-  data S7 b :: *
+  data S7 b :: Type
 
 instance C7 Char (a, Bool) where
   data S7 (a, Bool) = S7_1
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr
index b0c421fce8..b3dd8ef839 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr
@@ -1,7 +1,7 @@
 
-SimpleFail9.hs:14:3: error:
+SimpleFail9.hs:16:3: error:
     • Type indexes must match class instance head
       Expected: S7 (a, Int)
-      Actual:   S7 (b, Int)
+        Actual: S7 (b, Int) -- Defined at SimpleFail9.hs:16:8
     • In the data instance declaration for ‘S7’
       In the instance declaration for ‘C7 Char (a, Int)’
diff --git a/testsuite/tests/indexed-types/should_fail/T10817.stderr b/testsuite/tests/indexed-types/should_fail/T10817.stderr
index 715febdc25..af8acae33a 100644
--- a/testsuite/tests/indexed-types/should_fail/T10817.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T10817.stderr
@@ -1,6 +1,7 @@
 
 T10817.hs:9:3: error:
-    The type family application ‘F a’
-      is no smaller than the instance head ‘F a’
-    (Use UndecidableInstances to permit this)
-    In the class declaration for ‘C’
+    • The type family application ‘F a’
+        is no smaller than the instance head ‘F a’
+      (Use UndecidableInstances to permit this)
+    • In the default type instance declaration for ‘F’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T10899.stderr b/testsuite/tests/indexed-types/should_fail/T10899.stderr
index 925e4348fe..0dd92ef9bf 100644
--- a/testsuite/tests/indexed-types/should_fail/T10899.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T10899.stderr
@@ -1,4 +1,5 @@
 
 T10899.hs:7:3: error:
     • Illegal polymorphic type: forall (m :: * -> *). m a
-    • In the class declaration for ‘C’
+    • In the default type instance declaration for ‘F’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T11450.stderr b/testsuite/tests/indexed-types/should_fail/T11450.stderr
index a6fe961fcf..f5be9d48c3 100644
--- a/testsuite/tests/indexed-types/should_fail/T11450.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T11450.stderr
@@ -1,7 +1,7 @@
 
-T11450.hs:9:8: error:
+T11450.hs:9:3: error:
     • Type indexes must match class instance head
       Expected: T (Either a b)
-      Actual:   T (Either b a)
+        Actual: T (Either b a) -- Defined at T11450.hs:9:8
     • In the type instance declaration for ‘T’
       In the instance declaration for ‘C (Either a b)’
diff --git a/testsuite/tests/indexed-types/should_fail/T12041.stderr b/testsuite/tests/indexed-types/should_fail/T12041.stderr
index 006ca37bae..d16a9cc49c 100644
--- a/testsuite/tests/indexed-types/should_fail/T12041.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T12041.stderr
@@ -1,7 +1,7 @@
 
-T12041.hs:12:15: error:
-    • Expected kind ‘i -> Constraint’,
-        but ‘(~) Int’ has kind ‘* -> Constraint’
-    • In the type ‘(~) Int’
-      In the type instance declaration for ‘Ob’
+T12041.hs:12:3: error:
+    • Type indexes must match class instance head
+      Expected: Ob @i (I @{i} @{i})
+        Actual: Ob @* (I @{*} @{*}) -- Defined at T12041.hs:12:8
+    • In the type instance declaration for ‘Ob’
       In the instance declaration for ‘Category I’
diff --git a/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr b/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr
index 9df66e7cd1..c13bde5ad8 100644
--- a/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr
@@ -2,4 +2,4 @@
 Main.hs:10:15: error:
     Conflicting family instance declarations:
       A (a, Y) = Bool -- Defined at Main.hs:10:15
-      A (B.X, b) = () -- Defined in ‘B’
+      A (B.X, b) = () -- Defined in module B
diff --git a/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr b/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr
index 6676684ec1..ab714e3ecc 100644
--- a/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr
@@ -2,4 +2,4 @@
 T13092c_4.hs:7:15: error:
     Conflicting family instance declarations:
       F (a, Char) = String -- Defined at T13092c_4.hs:7:15
-      F (T13092c_2.X, b) = Bool -- Defined in ‘T13092c_2’
+      F (T13092c_2.X, b) = Bool -- Defined in module T13092c_2
diff --git a/testsuite/tests/indexed-types/should_fail/T13972.hs b/testsuite/tests/indexed-types/should_fail/T13972.hs
index a0a203d30a..9a5af411e2 100644
--- a/testsuite/tests/indexed-types/should_fail/T13972.hs
+++ b/testsuite/tests/indexed-types/should_fail/T13972.hs
@@ -8,5 +8,11 @@ import Data.Kind
 class C (a :: k) where
   type T k :: Type
 
+-- This used to fail, with a mysterious error messate
+--    Type indexes must match class instance head
+--      Expected: T (a1 -> Either a1 b1)
+--      Actual: T (a -> Either a b)
+-- but now it succeeds fine
+
 instance C Left where
   type T (a -> Either a b) = Int
diff --git a/testsuite/tests/indexed-types/should_fail/T13972.stderr b/testsuite/tests/indexed-types/should_fail/T13972.stderr
deleted file mode 100644
index b1f05b3105..0000000000
--- a/testsuite/tests/indexed-types/should_fail/T13972.stderr
+++ /dev/null
@@ -1,7 +0,0 @@
-
-T13972.hs:12:8: error:
-    • Type indexes must match class instance head
-      Expected: T (a1 -> Either a1 b1)
-        Actual: T (a -> Either a b)
-    • In the type instance declaration for ‘T’
-      In the instance declaration for ‘C Left’
diff --git a/testsuite/tests/indexed-types/should_fail/T14045a.hs b/testsuite/tests/indexed-types/should_fail/T14045a.hs
index fc545a8d41..985220c472 100644
--- a/testsuite/tests/indexed-types/should_fail/T14045a.hs
+++ b/testsuite/tests/indexed-types/should_fail/T14045a.hs
@@ -7,6 +7,11 @@ import Data.Kind
 class C (a :: k) where
   data S (a :: k)
 
+-- This used to fail with the mysterious error
+--   Type indexes must match class instance head
+--     Expected: S z
+--     Actual: S a
+-- But now it is fine
 instance C (z :: Bool) where
   data S :: Bool -> Type where
     SF :: S False
diff --git a/testsuite/tests/indexed-types/should_fail/T14045a.stderr b/testsuite/tests/indexed-types/should_fail/T14045a.stderr
deleted file mode 100644
index 0306bd2a07..0000000000
--- a/testsuite/tests/indexed-types/should_fail/T14045a.stderr
+++ /dev/null
@@ -1,7 +0,0 @@
-
-T14045a.hs:11:3: error:
-    • Type indexes must match class instance head
-      Expected: S z
-        Actual: S :: Bool -> Type
-    • In the data instance declaration for ‘S’
-      In the instance declaration for ‘C (z :: Bool)’
diff --git a/testsuite/tests/indexed-types/should_fail/T14179.stderr b/testsuite/tests/indexed-types/should_fail/T14179.stderr
index 38d77f1cca..bb956c7b51 100644
--- a/testsuite/tests/indexed-types/should_fail/T14179.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14179.stderr
@@ -6,8 +6,8 @@ T14179.hs:7:15: error:
 
 T14179.hs:11:15: error:
     Conflicting family instance declarations:
-      Foo2 a -- Defined at T14179.hs:11:15
-      Foo2 a -- Defined at T14179.hs:12:15
+      Foo2 -- Defined at T14179.hs:11:15
+      Foo2 -- Defined at T14179.hs:12:15
 
 T14179.hs:15:15: error:
     Conflicting family instance declarations:
diff --git a/testsuite/tests/indexed-types/should_fail/T14887.hs b/testsuite/tests/indexed-types/should_fail/T14887.hs
new file mode 100644
index 0000000000..63fbbd3943
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T14887.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fprint-explicit-kinds #-}
+module T14887 where
+
+import Data.Kind
+import Data.Type.Equality
+
+type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where
+  Foo1 (e :: a :~: a) = a :~: a
+
+type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where
+  Foo2 k (e :: a :~: a) = a :~: a
diff --git a/testsuite/tests/indexed-types/should_fail/T14887.stderr b/testsuite/tests/indexed-types/should_fail/T14887.stderr
new file mode 100644
index 0000000000..56875a7628
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T14887.stderr
@@ -0,0 +1,12 @@
+
+T14887.hs:13:1: error:
+    • The kind of ‘Foo2’ is ill-scoped
+        Inferred kind: Foo2 :: forall (a :: k). forall k -> (a :~: a) -> *
+      NB: Specified variables (namely: (a :: k)) always come first
+      Perhaps try this order instead: k (a :: k) (e :: a :~: a)
+    • In the type family declaration for ‘Foo2’
+
+T14887.hs:14:11: error:
+    • Expected kind ‘a0 :~: a0’, but ‘e :: a :~: a’ has kind ‘a :~: a’
+    • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’
+      In the type family declaration for ‘Foo2’
diff --git a/testsuite/tests/indexed-types/should_fail/T15740.hs b/testsuite/tests/indexed-types/should_fail/T15740.hs
new file mode 100644
index 0000000000..e564a87509
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T15740.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeInType, TypeFamilies, KindSignatures, RankNTypes #-}
+
+module T15740 where
+
+import Data.Kind
+
+type family F2 :: forall k. k -> Type
+data SBool :: Bool -> Type
+data Nat
+data SNat :: Nat -> Type
+type instance F2 = SBool
+type instance F2 = SNat
diff --git a/testsuite/tests/indexed-types/should_fail/T15740.stderr b/testsuite/tests/indexed-types/should_fail/T15740.stderr
new file mode 100644
index 0000000000..9d7cdcfee7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T15740.stderr
@@ -0,0 +1,11 @@
+
+T15740.hs:11:20: error:
+    • Expected kind ‘forall k. k -> *’,
+        but ‘SBool’ has kind ‘Bool -> *’
+    • In the type ‘SBool’
+      In the type instance declaration for ‘F2’
+
+T15740.hs:12:20: error:
+    • Expected kind ‘forall k. k -> *’, but ‘SNat’ has kind ‘Nat -> *’
+    • In the type ‘SNat’
+      In the type instance declaration for ‘F2’
diff --git a/testsuite/tests/indexed-types/should_fail/T15764.hs b/testsuite/tests/indexed-types/should_fail/T15764.hs
new file mode 100644
index 0000000000..f4c164cd05
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T15764.hs
@@ -0,0 +1,14 @@
+{-# Language PolyKinds #-}
+{-# Language TypeFamilies #-}
+{-# Language KindSignatures #-}
+{-# Language DataKinds #-}
+{-# Language MultiParamTypeClasses #-}
+
+module T15764 where
+
+import Data.Kind
+import Data.Proxy
+import GHC.TypeLits
+
+class C6 (k :: Type) (a :: k) (b :: Proxy (a :: k)) where
+ type T6 (proxy :: Proxy '(k, b))
diff --git a/testsuite/tests/indexed-types/should_fail/T15764.stderr b/testsuite/tests/indexed-types/should_fail/T15764.stderr
new file mode 100644
index 0000000000..5c04427841
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T15764.stderr
@@ -0,0 +1,11 @@
+
+T15764.hs:14:2: error:
+    • The kind of ‘T6’ is ill-scoped
+        Inferred kind: T6 :: forall (a :: k) k (b :: Proxy a).
+                             Proxy '(k, b) -> *
+      NB: Inferred variables
+        (namely: (a :: k)) always come first
+        then Specified variables (namely: k (b :: Proxy a))
+      Perhaps try this order instead:
+        k (a :: k) (b :: Proxy a) (proxy :: Proxy '(k, b))
+    • In the associated type family declaration for ‘T6’
diff --git a/testsuite/tests/indexed-types/should_fail/T15870.hs b/testsuite/tests/indexed-types/should_fail/T15870.hs
new file mode 100644
index 0000000000..0a07c3e5e5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T15870.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+
+module T15870 where
+
+data Optic a where
+  --Index :: Nat    -> Optic a
+  --Name  :: Symbol -> Optic a
+  (:.:) :: Optic a -> Optic b -> Optic a -- composition
+
+class Gettable a (optic :: Optic a) where
+  type Get a (optic :: Optic a)
+
+{-
+some basic instances, e.g.
+instance Gettable (a,b) (Index 0) where
+  type Get (a,b) (Index 0) = a
+...
+-}
+
+instance forall a b (g1 :: Optic a) (g2 :: Optic b).
+        ( Gettable a g1
+        , b ~ Get a g1
+        , Gettable b g2
+        ) => Gettable a (g1 :.: g2) where
+  type Get a (g1 :.: g2) = Get a g2
diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr
new file mode 100644
index 0000000000..4acacbab50
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr
@@ -0,0 +1,6 @@
+
+T15870.hs:32:34: error:
+    • Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’
+    • In the second argument of ‘Get’, namely ‘g2’
+      In the type ‘Get a g2’
+      In the type instance declaration for ‘Get’
diff --git a/testsuite/tests/indexed-types/should_fail/T7536.stderr b/testsuite/tests/indexed-types/should_fail/T7536.stderr
index 9e7ed3010e..22c565be62 100644
--- a/testsuite/tests/indexed-types/should_fail/T7536.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7536.stderr
@@ -1,5 +1,6 @@
 
-T7536.hs:8:15:
-    Family instance purports to bind type variable ‘a’
-      but the real LHS (expanding synonyms) is: TF Int = ...
-    In the type instance declaration for ‘TF’
+T7536.hs:8:21: error:
+    • Type variable ‘a’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
+        The real LHS (expanding synonyms) is: TF Int
+    • In the type instance declaration for ‘TF’
diff --git a/testsuite/tests/indexed-types/should_fail/T7938.hs b/testsuite/tests/indexed-types/should_fail/T7938.hs
index 405a7e54d0..246015ddf7 100644
--- a/testsuite/tests/indexed-types/should_fail/T7938.hs
+++ b/testsuite/tests/indexed-types/should_fail/T7938.hs
@@ -9,4 +9,4 @@ class Foo (a :: k1) (b :: k2) where
   type Bar a
 
 instance Foo (a :: k1) (b :: k2) where
-  type Bar a = (KP :: KProxy k2)
\ No newline at end of file
+  type Bar a = (KP :: KProxy k2)
diff --git a/testsuite/tests/indexed-types/should_fail/T7938.stderr b/testsuite/tests/indexed-types/should_fail/T7938.stderr
index 890be7b7b8..5751c4e992 100644
--- a/testsuite/tests/indexed-types/should_fail/T7938.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7938.stderr
@@ -1,6 +1,6 @@
 
 T7938.hs:12:17: error:
-    • Expected a type, but ‘KP :: KProxy k2’ has kind ‘KProxy k4’
+    • Expected a type, but ‘KP :: KProxy k2’ has kind ‘KProxy k2’
     • In the type ‘(KP :: KProxy k2)’
       In the type instance declaration for ‘Bar’
       In the instance declaration for ‘Foo (a :: k1) (b :: k2)’
diff --git a/testsuite/tests/indexed-types/should_fail/T9160.stderr b/testsuite/tests/indexed-types/should_fail/T9160.stderr
index 4ed166cfdb..36a1cb6767 100644
--- a/testsuite/tests/indexed-types/should_fail/T9160.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9160.stderr
@@ -1,7 +1,7 @@
 
-T9160.hs:19:12: error:
-    Expecting one more argument to ‘Maybe’
-    Expected a type, but ‘Maybe’ has kind ‘* -> *’
-    In the type ‘Maybe’
-    In the type instance declaration for ‘F’
-    In the instance declaration for ‘C (a :: *)’
+T9160.hs:19:3: error:
+    • Type indexes must match class instance head
+      Expected: F @*
+        Actual: F @(* -> *) -- Defined at T9160.hs:19:8
+    • In the type instance declaration for ‘F’
+      In the instance declaration for ‘C (a :: *)’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 12fa999a9f..6273f595b0 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -139,12 +139,16 @@ test('T13271', normal, compile_fail, [''])
 test('T13674', normal, compile_fail, [''])
 test('T13784', normal, compile_fail, [''])
 test('T13877', normal, compile_fail, [''])
-test('T13972', normal, compile_fail, [''])
+test('T13972', normal, compile, [''])
 test('T14033', normal, compile_fail, [''])
-test('T14045a', normal, compile_fail, [''])
+test('T14045a', normal, compile, [''])
 test('T14175', normal, compile_fail, [''])
 test('T14179', normal, compile_fail, [''])
 test('T14246', normal, compile_fail, [''])
 test('T14369', normal, compile_fail, [''])
 test('T15172', normal, compile_fail, [''])
 test('T14904', normal, compile_fail, [''])
+test('T15740', normal, compile_fail, [''])
+test('T15764', normal, compile_fail, [''])
+test('T15870', normal, compile_fail, [''])
+test('T14887', normal, compile_fail, [''])