Don't look for TypeError in type family arguments

Changes checkUserTypeError to no longer look for custom type errors
inside type family arguments.

This means that a program such as

foo :: F xyz (TypeError (Text "blah")) -> bar

does not throw a type error at definition site.
This means that more programs can be accepted, as the custom type error
might disappear upon reducing the above type family F.

This applies only to user-written type signatures, which are checked
within checkValidType. Custom type errors in type family arguments
continue to be reported when they occur in unsolved Wanted constraints.

Fixes #20241

6 files changed, 90 insertions, 11 deletions

diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 4c141ce082..9ba071bc78 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -241,10 +241,16 @@ wantAmbiguityCheck ctxt
       StandaloneKindSigCtxt{} -> False
       _            -> True
 
-checkUserTypeError :: UserTypeCtxt -> Type -> TcM ()
--- Check to see if the type signature mentions "TypeError blah"
--- anywhere in it, and fail if so.
+-- | Check whether the type signature contains custom type errors,
+-- and fail if so.
+--
+-- Note that some custom type errors are acceptable:
 --
+--   - in the RHS of a type synonym, e.g. to allow users to define
+--     type synonyms for custom type errors with large messages (#20181),
+--   - inside a type family application, as a custom type error
+--     might evaporate after performing type family reduction (#20241).
+checkUserTypeError :: UserTypeCtxt -> Type -> TcM ()
 -- Very unsatisfactorily (#11144) we need to tidy the type
 -- because it may have come from an /inferred/ signature, not a
 -- user-supplied one.  This is really only a half-baked fix;
@@ -258,12 +264,14 @@ checkUserTypeError ctxt ty
   = check ty
   where
   check ty
-    | Just msg     <- userTypeError_maybe ty      = fail_with msg
-    | Just (_,ts)  <- splitTyConApp_maybe ty      = mapM_ check ts
-    | Just (t1,t2) <- splitAppTy_maybe ty         = check t1 >> check t2
-    | Just (_,t1)  <- splitForAllTyCoVar_maybe ty = check t1
-    | otherwise                                   = return ()
-
+    | Just msg    <- userTypeError_maybe ty      = fail_with msg
+    | Just (_,t1) <- splitForAllTyCoVar_maybe ty = check t1
+    | let (_,tys) =  splitAppTys ty              = mapM_ check tys
+    -- splitAppTys keeps type family applications saturated.
+    -- This means we don't go looking for user type errors
+    -- inside type family arguments (see #20241).
+
+  fail_with :: Type -> TcM ()
   fail_with msg = do { env0 <- tcInitTidyEnv
                      ; let (env1, tidy_msg) = tidyOpenType env0 msg
                      ; failWithTcM (env1
diff --git a/testsuite/tests/typecheck/should_compile/T20241.hs b/testsuite/tests/typecheck/should_compile/T20241.hs
new file mode 100644
index 0000000000..54c2356477
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20241.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+import Data.Kind
+  ( Type, Constraint )
+import Data.Proxy
+  ( Proxy(..) )
+import GHC.TypeLits
+  ( TypeError, ErrorMessage(..) )
+
+type Assert :: Bool -> Constraint -> Constraint
+type family Assert check errMsg where
+  Assert 'True _      = ()
+  Assert _     errMsg = errMsg
+
+foo_sym :: Assert 'True (TypeError (Text "Boom")) => Proxy a -> ()
+foo_sym Proxy = ()
+
+type IsInt :: Type -> Bool
+type family IsInt a where
+  IsInt Int = True
+
+bar_sym :: Assert (IsInt a) (TypeError (Text "Boom")) => Proxy a -> ()
+bar_sym Proxy = ()
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 7498e23a8e..72105683a5 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -795,4 +795,4 @@ test('T17817b', normal, compile, [''])
 test('T20033', normal, compile, [''])
 test('TypeRepCon', normal, compile, ['-Woverlapping-patterns'])
 test('T20181', normal, compile, [''])
-
+test('T20241', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T20241b.hs b/testsuite/tests/typecheck/should_fail/T20241b.hs
new file mode 100644
index 0000000000..ced85b29d0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20241b.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+import Data.Kind
+  ( Type, Constraint )
+import Data.Proxy
+  ( Proxy(..) )
+import GHC.TypeLits
+  ( TypeError, ErrorMessage(..) )
+
+-- Check that custom type errors are still detected when they are
+-- used at different kinds and applied to many arguments.
+
+foo :: ( ( TypeError (Text "Boom") :: (Type -> Type) -> Type -> Constraint ) IO ) a
+    => Proxy a -> ()
+foo Proxy = ()
+
+bar :: ( ( c :: Constraint -> Type -> Constraint )
+           ( ( ( TypeError (Text "Boom") :: (Type -> Type) -> Type -> Constraint )
+              IO
+             )
+             a
+           )
+       ) a
+    => Proxy a -> ()
+bar Proxy = ()
diff --git a/testsuite/tests/typecheck/should_fail/T20241b.stderr b/testsuite/tests/typecheck/should_fail/T20241b.stderr
new file mode 100644
index 0000000000..7b742e7905
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20241b.stderr
@@ -0,0 +1,16 @@
+
+T20241b.hs:16:8: error:
+    • Boom
+    • In the type signature:
+        foo :: ((TypeError (Text "Boom") :: (Type -> Type)
+                                            -> Type -> Constraint) IO) a =>
+               Proxy a -> ()
+
+T20241b.hs:20:8: error:
+    • Boom
+    • In the type signature:
+        bar :: ((c :: Constraint
+                      -> Type -> Constraint) (((TypeError (Text "Boom") :: (Type -> Type)
+                                                                           -> Type
+                                                                              -> Constraint) IO) a)) a =>
+               Proxy a -> ()
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index b573f9b7f6..155500ab9f 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -633,4 +633,5 @@ test('T19615', normal, compile_fail, [''])
 test('T17817', normal, compile_fail, [''])
 test('T17817_elab', normal, compile_fail, ['-fprint-typechecker-elaboration'])
 test('T19978', normal, compile_fail, [''])
-test('T20122', normal, compile_fail, [''])
\ No newline at end of file
+test('T20122', normal, compile_fail, [''])
+test('T20241b', normal, compile_fail, [''])