Reject class instances with type families in kinds

Summary:
GHC doesn't know how to handle type families that appear in
class instances. Unfortunately, GHC didn't reject instances where
type families appear in //kinds//, leading to #15515. This is easily
rectified by calling `checkValidTypePat` on all arguments to a class
in an instance (and not just the type arguments).

Test Plan: make test TEST=T15515

Reviewers: bgamari, goldfire, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, carter

GHC Trac Issues: #15515

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

2 files changed, 48 insertions, 23 deletions

diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index d773420b2c..2fde421f79 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -63,6 +63,7 @@ import Unique      ( mkAlphaTyVarUnique )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
+import Data.Foldable
 import Data.List        ( (\\), nub )
 import qualified Data.List.NonEmpty as NE
 
@@ -1174,7 +1175,7 @@ check_valid_inst_head dflags this_mod is_boot ctxt clas cls_args
   = failWithTc (instTypeErr clas cls_args msg)
 
   | otherwise
-  = mapM_ checkValidTypePat ty_args
+  = checkValidTypePats (classTyCon clas) cls_args
   where
     clas_nm = getName clas
     ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
@@ -1963,7 +1964,7 @@ checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar]
 --         type instance F (T a) = a
 -- c) For associated types, are consistently instantiated
 checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats pp_hs_pats
-  = do { mapM_ checkValidTypePat user_ty_pats
+  = do { checkValidTypePats fam_tc user_ty_pats
 
        ; let unbound_tcvs = filterOut (`elemVarSet` exactTyCoVarsOfTypes user_ty_pats)
                                       (tvs ++ cvs)
@@ -1972,19 +1973,44 @@ checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats pp_hs_pat
          -- Check that type patterns match the class instance head
        ; checkConsistentFamInst mb_clsinfo fam_tc (user_ty_pats `chkAppend` extra_ty_pats) pp_hs_pats }
 
-checkValidTypePat :: Type -> TcM ()
--- Used for type patterns in class instances,
--- and in type/data family instances
-checkValidTypePat pat_ty
-  = do { -- Check that pat_ty is a monotype
-         checkValidMonoType pat_ty
-             -- One could imagine generalising to allow
-             --      instance C (forall a. a->a)
-             -- but we don't know what all the consequences might be
-
-          -- Ensure that no type family instances occur a type pattern
-       ; checkTc (isTyFamFree pat_ty) $
-         tyFamInstIllegalErr pat_ty }
+-- | Checks for occurrences of type families in class instances and type/data
+-- family instances.
+checkValidTypePats :: TyCon -> [Type] -> TcM ()
+checkValidTypePats tc pat_ty_args =
+  traverse_ (check_valid_type_pat False) invis_ty_args *>
+  traverse_ (check_valid_type_pat True)  vis_ty_args
+  where
+    (invis_ty_args, vis_ty_args) = partitionInvisibleTypes tc pat_ty_args
+    inst_ty = mkTyConApp tc pat_ty_args
+
+    check_valid_type_pat
+      :: Bool -- True if this is an /visible/ argument to the TyCon.
+      -> Type -> TcM ()
+    -- Used for type patterns in class instances,
+    -- and in type/data family instances
+    check_valid_type_pat vis_arg pat_ty
+      = do { -- Check that pat_ty is a monotype
+             checkValidMonoType pat_ty
+                 -- One could imagine generalising to allow
+                 --      instance C (forall a. a->a)
+                 -- but we don't know what all the consequences might be
+
+              -- Ensure that no type family instances occur a type pattern
+           ; case tcTyFamInsts pat_ty of
+               [] -> pure ()
+               ((tf_tc, tf_args):_) ->
+                 failWithTc $
+                 ty_fam_inst_illegal_err vis_arg (mkTyConApp tf_tc tf_args) }
+
+    ty_fam_inst_illegal_err :: Bool -> Type -> SDoc
+    ty_fam_inst_illegal_err vis_arg ty
+      = sdocWithDynFlags $ \dflags ->
+        hang (text "Illegal type synonym family application"
+                <+> quotes (ppr ty) <+> text "in instance" <>
+             colon) 2 $
+          vcat [ ppr inst_ty
+               , ppUnless (vis_arg || gopt Opt_PrintExplicitKinds dflags) $
+                 text "Use -fprint-explicit-kinds to see the kind arguments" ]
 
 -- Error messages
 
@@ -1993,12 +2019,6 @@ inaccessibleCoAxBranch fi_ax cur_branch
   = text "Type family instance equation is overlapped:" $$
     nest 2 (pprCoAxBranch fi_ax cur_branch)
 
-tyFamInstIllegalErr :: Type -> SDoc
-tyFamInstIllegalErr ty
-  = hang (text "Illegal type synonym family application in instance" <>
-         colon) 2 $
-      ppr ty
-
 nestedMsg :: SDoc -> SDoc
 nestedMsg what
   = sep [ text "Illegal nested" <+> what
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 2529bfb89d..180af3862c 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -60,7 +60,7 @@ module Type (
         stripCoercionTy, splitCoercionType_maybe,
 
         splitPiTysInvisible, filterOutInvisibleTypes,
-        partitionInvisibles,
+        partitionInvisibleTypes, partitionInvisibles,
         synTyConResKind,
 
         modifyJoinResTy, setJoinResTy,
@@ -1450,7 +1450,12 @@ splitPiTysInvisible ty = split ty ty []
 
 -- | Given a tycon and its arguments, filters out any invisible arguments
 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
-filterOutInvisibleTypes tc tys = snd $ partitionInvisibles tc id tys
+filterOutInvisibleTypes tc tys = snd $ partitionInvisibleTypes tc tys
+
+-- | Given a 'TyCon' and its arguments, partition the arguments into
+-- (invisible arguments, visible arguments).
+partitionInvisibleTypes :: TyCon -> [Type] -> ([Type], [Type])
+partitionInvisibleTypes tc tys = partitionInvisibles tc id tys
 
 -- | Given a tycon and a list of things (which correspond to arguments),
 -- partitions the things into