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

10 files changed, 101 insertions, 38 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
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
index 6cb6fe0e50..cfbab576b9 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
@@ -1,8 +1,10 @@
 
-SimpleFail13.hs:9:1:
-    Illegal type synonym family application in instance: [C a]
-    In the data instance declaration for ‘D’
+SimpleFail13.hs:9:1: error:
+    • Illegal type synonym family application ‘C a’ in instance:
+        D [C a]
+    • In the data instance declaration for ‘D’
 
-SimpleFail13.hs:13:15:
-    Illegal type synonym family application in instance: [C a]
-    In the type instance declaration for ‘E’
+SimpleFail13.hs:13:15: error:
+    • Illegal type synonym family application ‘C a’ in instance:
+        E [C a]
+    • In the type instance declaration for ‘E’
diff --git a/testsuite/tests/indexed-types/should_fail/T2203a.stderr b/testsuite/tests/indexed-types/should_fail/T2203a.stderr
index f6e7f31d3c..80c65504f3 100644
--- a/testsuite/tests/indexed-types/should_fail/T2203a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2203a.stderr
@@ -1,5 +1,5 @@
 
-T2203a.hs:13:19:
-    Illegal type synonym family application in instance:
-      Either a (TheFoo a)
-    In the instance declaration for ‘Bar (Either a (TheFoo a))’
+T2203a.hs:13:19: error:
+    • Illegal type synonym family application ‘TheFoo a’ in instance:
+        Bar (Either a (TheFoo a))
+    • In the instance declaration for ‘Bar (Either a (TheFoo a))’
diff --git a/testsuite/tests/indexed-types/should_fail/T9097.stderr b/testsuite/tests/indexed-types/should_fail/T9097.stderr
index 02dfc33068..32c987f70d 100644
--- a/testsuite/tests/indexed-types/should_fail/T9097.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9097.stderr
@@ -1,5 +1,6 @@
 
-T9097.hs:10:3:
-    Illegal type synonym family application in instance: Any
-    In the equations for closed type family ‘Foo’
-    In the type family declaration for ‘Foo’
+T9097.hs:10:3: error:
+    • Illegal type synonym family application ‘Any’ in instance:
+        Foo Any
+    • In the equations for closed type family ‘Foo’
+      In the type family declaration for ‘Foo’
diff --git a/testsuite/tests/polykinds/T11520.stderr b/testsuite/tests/polykinds/T11520.stderr
index 75147e6a00..93078aa23c 100644
--- a/testsuite/tests/polykinds/T11520.stderr
+++ b/testsuite/tests/polykinds/T11520.stderr
@@ -1,6 +1,8 @@
 
 T11520.hs:15:57: error:
-    • Illegal type synonym family application in instance: Compose f g
+    • Illegal type synonym family application ‘Any’ in instance:
+        Typeable (Compose f g)
+        Use -fprint-explicit-kinds to see the kind arguments
     • In the instance declaration for ‘Typeable (Compose f g)’
 
 T11520.hs:15:77: error:
diff --git a/testsuite/tests/typecheck/should_fail/T13909.stderr b/testsuite/tests/typecheck/should_fail/T13909.stderr
index 599be5a445..d70221c3fd 100644
--- a/testsuite/tests/typecheck/should_fail/T13909.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13909.stderr
@@ -1,4 +1,10 @@
 
+T13909.hs:11:10: error:
+    • Illegal type synonym family application ‘GHC.Types.Any’ in instance:
+        HasName Hm
+        Use -fprint-explicit-kinds to see the kind arguments
+    • In the instance declaration for ‘HasName Hm’
+
 T13909.hs:11:18: error:
     • Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’
     • In the first argument of ‘HasName’, namely ‘Hm’
diff --git a/testsuite/tests/typecheck/should_fail/T15515.hs b/testsuite/tests/typecheck/should_fail/T15515.hs
new file mode 100644
index 0000000000..3630609827
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15515.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T15515 where
+
+import Data.Kind
+import Data.Proxy
+
+class C a where
+  c :: Proxy a
+
+type family F
+
+data D :: F -> Type
+
+instance C (D :: F -> Type) where
+  c = Proxy
+
+c' :: Proxy (D :: F -> Type)
+c' = c @(D :: F -> Type)
diff --git a/testsuite/tests/typecheck/should_fail/T15515.stderr b/testsuite/tests/typecheck/should_fail/T15515.stderr
new file mode 100644
index 0000000000..f58d8afb2d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15515.stderr
@@ -0,0 +1,6 @@
+
+T15515.hs:16:10: error:
+    • Illegal type synonym family application ‘F’ in instance:
+        C D
+        Use -fprint-explicit-kinds to see the kind arguments
+    • In the instance declaration for ‘C (D :: F -> Type)’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 895721937d..64bc8cf7d2 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -477,6 +477,7 @@ test('T15067', normal, compile_fail, [''])
 test('T15330', normal, compile_fail, [''])
 test('T15361', normal, compile_fail, [''])
 test('T15438', normal, compile_fail, [''])
+test('T15515', normal, compile_fail, [''])
 test('T15523', normal, compile_fail, ['-O'])
 test('T15527', normal, compile_fail, [''])
 test('T15552', normal, compile, [''])