Check for duplicate variables in associated default equations

A follow-up to !696's, which attempted to clean up the error messages
for ill formed associated type family default equations. The previous
attempt, !696, forgot to account for the possibility of duplicate
kind variable arguments, as in the following example:

```hs
class C (a :: j) where
  type T (a :: j) (b :: k)
  type T (a :: k) (b :: k) = k
```

This patch addresses this shortcoming by adding an additional check
for this. Fixes #13971 (hopefully for good this time).

1 files changed, 62 insertions, 13 deletions

diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 114d839df5..8b5142158d 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -73,7 +73,9 @@ import BasicTypes
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
+import Data.Foldable
 import Data.List
+import qualified Data.List.NonEmpty as NE
 import Data.List.NonEmpty ( NonEmpty(..) )
 import qualified Data.Set as Set
 
@@ -1544,13 +1546,15 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
                                                     hs_pats hs_rhs_ty
 
        ; let fam_tvs = tyConTyVars fam_tc
+             ppr_eqn = ppr_default_eqn pats rhs_ty
        ; 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
+       ; pat_tvs <- traverse (extract_tv ppr_eqn) pats
+       ; check_all_distinct_tvs ppr_eqn pat_tvs
        ; 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
@@ -1561,14 +1565,12 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
     -- 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
+    extract_tv :: SDoc   -- The pretty-printed default equation
                          -- (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 =
+    extract_tv ppr_eqn pat =
       case getTyVar_maybe pat of
         Just tv -> pure tv
         Nothing ->
@@ -1579,10 +1581,39 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
           -- 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" ])
+             2 (vcat [ppr_eqn, suggestion])
+
+
+    -- Checks that no type variables in an associated default declaration are
+    -- duplicated. If that is the case, throw an error.
+    -- See Note [Type-checking default assoc decls]
+    check_all_distinct_tvs :: SDoc    -- The pretty-printed default equation
+                                      -- (only used for error message purposes)
+                           -> [TyVar] -- The type variable arguments in the
+                                      -- associated default declaration
+                           -> TcM ()
+    check_all_distinct_tvs ppr_eqn tvs =
+      let dups = findDupsEq (==) tvs in
+      traverse_
+        (\d -> -- Per Note [Type-checking default assoc decls], we already
+               -- know by this point that if any arguments in the default
+               -- instance are duplicates, then they must be
+               -- invisible kind arguments. Therefore, always display the
+               -- error message with -fprint-explicit-kinds enabled.
+               failWithTc $ pprWithExplicitKindsWhen True $
+               hang (text "Illegal duplicate variable"
+                       <+> quotes (ppr (NE.head d)) <+> text "in:")
+                  2 (vcat [ppr_eqn, suggestion]))
+        dups
+
+    ppr_default_eqn :: [Type] -> Type -> SDoc
+    ppr_default_eqn pats rhs_ty =
+      quotes (text "type" <+> ppr (mkTyConApp fam_tc pats)
+                <+> equals <+> ppr rhs_ty)
+
+    suggestion :: SDoc
+    suggestion = text "The arguments to" <+> quotes (ppr fam_tc)
+             <+> text "must all be distinct type variables"
 tcDefaultAssocDecl _ [dL->L _ (XFamEqn _)] = panic "tcDefaultAssocDecl"
 tcDefaultAssocDecl _ [dL->L _ (FamEqn _ _ _ (XLHsQTyVars _) _ _)]
   = panic "tcDefaultAssocDecl"
@@ -1610,10 +1641,15 @@ 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):
+the arguments in the default instance consist of distinct type variables.
+This property has already been checked to some degree earlier in the compiler:
+RdrHsSyn.checkTyVars ensures that all visible type arguments are type
+variables, and RnTypes.bindLHsTyVarBndrs ensures that no visible type arguments
+are duplicated. But these only check /visible/ arguments, however, so we still
+must check the invisible kind arguments to see if these invariants are upheld.
+
+First, we must check that all arguments are type variables. As a motivating
+example, consider this erroneous program (inspired by #11361):
 
    class C a where
       type F (a :: k) b :: Type
@@ -1622,6 +1658,19 @@ catch so easily. Consider this erroneous program (inspired by #11361):
 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.
 
+Next, we must check that all arguments are distinct. Here is another offending
+example, this time taken from #13971:
+
+   class C2 (a :: j) where
+      type F2 (a :: j) (b :: k)
+      type F2 (x :: z) (y :: z) = z
+
+All of the arguments in the default equation for `F2` are type variables, so
+that passes the first check. However, if we were to build this substitution,
+then both `j` and `k` map to `z`! In terms of visible kind application, it's as
+if we had written `type F2 @z @z x y = z`, which makes it clear that we have
+duplicated a use of `z`. Therefore, `F2`'s default is also rejected.
+
 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