Tweak error messages for narrowly-kinded assoc default decls

This program, from #13971, currently has a rather confusing error
message:

```hs
class C a where
  type T a :: k
  type T a = Int
```
```
    • Kind mis-match on LHS of default declaration for ‘T’
    • In the default type instance declaration for ‘T’
      In the class declaration for ‘C’
```

It's not at all obvious why GHC is complaining about the LHS until
you realize that the default, when printed with
`-fprint-explicit-kinds`, is actually `type T @{k} @* a = Int`.
That is to say, the kind of `a` is being instantiated to `Type`,
whereas it ought to be a kind variable. The primary thrust of this
patch is to weak the error message to make this connection
more obvious:

```
    • Illegal argument ‘*’ in:
        ‘type T @{k} @* a = Int’
        The arguments to ‘T’ must all be type variables
    • In the default type instance declaration for ‘T’
      In the class declaration for ‘C’
```

Along the way, I performed some code cleanup suggested by @rae in
https://gitlab.haskell.org/ghc/ghc/issues/13971#note_191287. Before,
we were creating a substitution from the default declaration's type
variables to the type family tycon's type variables by way of
`tcMatchTys`. But this is overkill, since we already know (from the
aforementioned validity checking) that all the arguments in a default
declaration must be type variables anyway. Therefore, creating the
substitution is as simple as using `zipTvSubst`. I took the
opportunity to perform this refactoring while I was in town.

Fixes #13971.

5 files changed, 78 insertions, 25 deletions

diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 1ac12b096b..533c6d0ac3 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1497,7 +1497,7 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
   = -- See Note [Type-checking default assoc decls]
     setSrcSpan loc $
     tcAddFamInstCtxt (text "default type instance") tc_name $
-    do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
+    do { traceTc "tcDefaultAssocDecl 1" (ppr tc_name)
        ; let fam_tc_name = tyConName fam_tc
              fam_arity = length (tyConVisibleTyVars fam_tc)
 
@@ -1524,14 +1524,46 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
                                                     imp_vars exp_vars
                                                     hs_pats hs_rhs_ty
 
-         -- See Note [Type-checking default assoc decls]
-       ; traceTc "tcDefault" (vcat [ppr (tyConTyVars fam_tc), ppr qtvs, ppr pats])
-       ; case tcMatchTys pats (mkTyVarTys (tyConTyVars fam_tc)) of
-           Just subst -> return (Just (substTyUnchecked subst rhs_ty, loc) )
-           Nothing    -> failWithTc (defaultAssocKindErr fam_tc)
-           -- We check for well-formedness and validity later,
-           -- in checkValidClass
+       ; let fam_tvs = tyConTyVars fam_tc
+       ; traceTc "tcDefaultAssocDecl 2" (vcat
+           [ text "fam_tvs" <+> ppr fam_tvs
+           , text "qtvs"    <+> ppr qtvs
+           , text "pats"    <+> ppr pats
+           , text "rhs_ty"  <+> ppr rhs_ty
+           ])
+       ; pat_tvs <- traverse (extract_tv pats rhs_ty) pats
+       ; let subst = zipTvSubst pat_tvs (mkTyVarTys fam_tvs)
+       ; pure $ Just (substTyUnchecked subst rhs_ty, loc)
+           -- We also perform other checks for well-formedness and validity
+           -- later, in checkValidClass
      }
+  where
+    -- Checks that a pattern on the LHS of a default is a type
+    -- variable. If so, return the underlying type variable, and if
+    -- not, throw an error.
+    -- See Note [Type-checking default assoc decls]
+    extract_tv :: [Type] -- All default instance type patterns
+                         -- (only used for error message purposes)
+               -> Type   -- The default instance's right-hand side type
+                         -- (only used for error message purposes)
+               -> Type   -- The particular type pattern from which to extract
+                         -- its underlying type variable
+               -> TcM TyVar
+    extract_tv pats rhs_ty pat =
+      case getTyVar_maybe pat of
+        Just tv -> pure tv
+        Nothing ->
+          -- Per Note [Type-checking default assoc decls], we already
+          -- know by this point that if any arguments in the default
+          -- instance aren't type variables, then they must be
+          -- invisible kind arguments. Therefore, always display the
+          -- error message with -fprint-explicit-kinds enabled.
+          failWithTc $ pprWithExplicitKindsWhen True $
+          hang (text "Illegal argument" <+> quotes (ppr pat) <+> text "in:")
+             2 (vcat [ quotes (text "type" <+> ppr (mkTyConApp fam_tc pats)
+                       <+> equals <+> ppr rhs_ty)
+                     , text "The arguments to" <+> quotes (ppr fam_tc)
+                       <+> text "must all be type variables" ])
 tcDefaultAssocDecl _ [dL->L _ (XFamEqn _)] = panic "tcDefaultAssocDecl"
 tcDefaultAssocDecl _ [dL->L _ (FamEqn _ _ _ (XLHsQTyVars _) _ _)]
   = panic "tcDefaultAssocDecl"
@@ -1544,8 +1576,8 @@ tcDefaultAssocDecl _ [_]
 Consider this default declaration for an associated type
 
    class C a where
-      type F (a :: k) b :: *
-      type F x y = Proxy x -> y
+      type F (a :: k) b :: Type
+      type F (x :: j) y = Proxy x -> y
 
 Note that the class variable 'a' doesn't scope over the default assoc
 decl (rather oddly I think), and (less oddly) neither does the second
@@ -1555,17 +1587,26 @@ instance.
 
 However we store the default rhs (Proxy x -> y) in F's TyCon, using
 F's own type variables, so we need to convert it to (Proxy a -> b).
-We do this by calling tcMatchTys to match them up.  This also ensures
-that x's kind matches a's and similarly for y and b.  The error
-message isn't great, mind you.  (#11361 was caused by not doing a
-proper tcMatchTys here.)
+We do this by creating a substitution [j |-> k, x |-> a, b |-> y] and
+applying this substitution to the RHS.
+
+In order to create this substitution, we must first ensure that all of
+the arguments in the default instance consist of type variables. The parser
+already checks this to a certain degree (see RdrHsSyn.checkTyVars), but
+we must be wary of kind arguments being instantiated, which the parser cannot
+catch so easily. Consider this erroneous program (inspired by #11361):
 
-Recall also that the left-hand side of an associated type family
-default is always just variables -- no tycons here. Accordingly,
-the patterns used in the tcMatchTys won't actually be knot-tied,
-even though we're in the knot. This is too delicate for my taste,
-but it works.
+   class C a where
+      type F (a :: k) b :: Type
+      type F x        b = x
 
+If you squint, you'll notice that the kind of `x` is actually Type. However,
+we cannot substitute from [Type |-> k], so we reject this default.
+
+Since the LHS of an associated type family default is always just variables,
+it won't contain any tycons. Accordingly, the patterns used in the substitution
+won't actually be knot-tied, even though we're in the knot. This is too
+delicate for my taste, but it works.
 -}
 
 {- *********************************************************************
@@ -3849,11 +3890,6 @@ wrongNumberOfParmsErr max_args
   = text "Number of parameters must match family declaration; expected"
     <+> ppr max_args
 
-defaultAssocKindErr :: TyCon -> SDoc
-defaultAssocKindErr fam_tc
-  = text "Kind mis-match on LHS of default declaration for"
-    <+> quotes (ppr fam_tc)
-
 badRoleAnnot :: Name -> Role -> Role -> SDoc
 badRoleAnnot var annot inferred
   = hang (text "Role mismatch on variable" <+> ppr var <> colon)
diff --git a/testsuite/tests/indexed-types/should_compile/T11361a.stderr b/testsuite/tests/indexed-types/should_compile/T11361a.stderr
index 4eb8bf6426..bf6d22c4df 100644
--- a/testsuite/tests/indexed-types/should_compile/T11361a.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T11361a.stderr
@@ -1,5 +1,7 @@
 
 T11361a.hs:7:3: error:
-    • Kind mis-match on LHS of default declaration for ‘F’
+    • Illegal argument ‘*’ in:
+        ‘type F @* x = x’
+        The arguments to ‘F’ must all be type variables
     • In the default type instance declaration for ‘F’
       In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T13971.hs b/testsuite/tests/indexed-types/should_fail/T13971.hs
new file mode 100644
index 0000000000..8632ac5d4d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T13971.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T13971 where
+
+class C a where
+  type T a :: k
+  type T a = Int
diff --git a/testsuite/tests/indexed-types/should_fail/T13971.stderr b/testsuite/tests/indexed-types/should_fail/T13971.stderr
new file mode 100644
index 0000000000..df1a6bae3e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T13971.stderr
@@ -0,0 +1,7 @@
+
+T13971.hs:7:3: error:
+    • Illegal argument ‘*’ in:
+        ‘type T @{k} @* a = Int’
+        The arguments to ‘T’ must all be type variables
+    • In the default type instance declaration for ‘T’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 4e29910c21..27c1f5ac37 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -136,6 +136,7 @@ test('T13271', normal, compile_fail, [''])
 test('T13674', normal, compile_fail, [''])
 test('T13784', normal, compile_fail, [''])
 test('T13877', normal, compile_fail, [''])
+test('T13971', normal, compile_fail, [''])
 test('T13972', normal, compile, [''])
 test('T14033', normal, compile_fail, [''])
 test('T14045a', normal, compile, [''])