Fix #13972 by producing tidier errors

Summary:
Previously, one could experience an error message like this:

```
Expected: T (a -> Either a b)
  Actual: T (a -> Either a b)
```

This makes the error message an iota clearer by tidying it first, which will
instead produce:

```
Expected: T (a1 -> Either a1 b1)
  Actual: T (a -> Either a b)
```

Which steers users towards the understanding that the two sets of tyvars are
actually different.

Test Plan: make test TEST=T13972

Reviewers: simonpj, austin, bgamari, goldfire

Reviewed By: goldfire

Subscribers: goldfire, rwbarton, thomie

GHC Trac Issues: #13972

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

4 files changed, 32 insertions, 3 deletions

diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index bd4938eeaa..65c7afdf98 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1555,8 +1555,8 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat
        ; checkTc (all check_arg type_shapes)   pp_wrong_at_arg
 
        -- And now kind args
-       ; checkTc (all check_arg kind_shapes)
-                 (pp_wrong_at_arg $$ ppSuggestExplicitKinds)
+       ; checkTcM (all check_arg kind_shapes)
+                  (tidy_env2, pp_wrong_at_arg $$ ppSuggestExplicitKinds)
 
        ; traceTc "cfi" (vcat [ ppr inst_tvs
                              , ppr arg_shapes
@@ -1585,7 +1585,16 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat
                vcat [ text "where the `<tv>' arguments are type variables,"
                     , text "distinct from each other and from the instance variables" ] ]
 
-    expected_args = [ exp_ty `orElse` mk_tv at_ty | (exp_ty, at_ty) <- arg_shapes ]
+    -- We need to tidy, since it's possible that expected_args will contain
+    -- inferred kind variables with names identical to those in at_tys. If we
+    -- don't, we'll end up with horrible messages like this one (#13972):
+    --
+    --   Expected: T (a -> Either a b)
+    --     Actual: T (a -> Either a b)
+    (tidy_env1, _) = tidyOpenTypes emptyTidyEnv at_tys
+    (tidy_env2, expected_args)
+      = tidyOpenTypes tidy_env1 [ exp_ty `orElse` mk_tv at_ty
+                                | (exp_ty, at_ty) <- arg_shapes ]
     mk_tv at_ty   = mkTyVarTy (mkTyVar tv_name (typeKind at_ty))
     tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan
 
diff --git a/testsuite/tests/indexed-types/should_fail/T13972.hs b/testsuite/tests/indexed-types/should_fail/T13972.hs
new file mode 100644
index 0000000000..8a43e2016f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T13972.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+
+class C (a :: k) where
+  type T k :: Type
+
+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
new file mode 100644
index 0000000000..b1f05b3105
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T13972.stderr
@@ -0,0 +1,7 @@
+
+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/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index c3a2f16d6d..ee4fccefb4 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -136,5 +136,6 @@ 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('T14033', normal, compile_fail, [''])
 test('T14045a', normal, compile_fail, [''])