Synchronize ClsInst.doTyConApp with TcTypeable validity checks (#15862)

Issue #15862 demonstrated examples of type constructors on which
`TcTypeable.tyConIsTypeable` would return `False`, but the `Typeable`
constraint solver in `ClsInst` (in particular, `doTyConApp`) would
try to generate `Typeable` evidence for anyway, resulting in
disaster. This incongruity was caused by the fact that `doTyConApp`
was using a weaker validity check than `tyConIsTypeable` to determine
if a type constructor warrants `Typeable` evidence or not. The
solution, perhaps unsurprisingly, is to use `tyConIsTypeable` in
`doTyConApp` instead.

To avoid import cycles between `ClsInst` and `TcTypeable`, I factored
out `tyConIsTypeable` into its own module, `TcTypeableValidity`.

Fixes #15862.

7 files changed, 116 insertions, 35 deletions

diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index e1f0bec2b0..d380d96707 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -525,6 +525,7 @@ Library
         TcTyClsDecls
         TcTyDecls
         TcTypeable
+        TcTypeableValidity
         TcType
         TcEvidence
         TcEvTerm
diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs
index 58b9734b05..420cbaebd0 100644
--- a/compiler/typecheck/ClsInst.hs
+++ b/compiler/typecheck/ClsInst.hs
@@ -16,6 +16,7 @@ import TcRnMonad
 import TcType
 import TcMType
 import TcEvidence
+import TcTypeableValidity
 import RnEnv( addUsedGRE )
 import RdrName( lookupGRE_FieldLabel )
 import InstEnv
@@ -432,7 +433,7 @@ doFunTy clas ty arg_ty ret_ty
 -- of monomorphic kind (e.g. all kind variables have been instantiated).
 doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcM ClsInstResult
 doTyConApp clas ty tc kind_args
-  | Just _ <- tyConRepName_maybe tc
+  | tyConIsTypeable tc
   = return $ OneInst { cir_new_theta = (map (mk_typeable_pred clas) kind_args)
                      , cir_mk_ev     = mk_ev
                      , cir_what      = BuiltinInstance }
diff --git a/compiler/typecheck/TcTypeable.hs b/compiler/typecheck/TcTypeable.hs
index 3488957366..eb679e6daf 100644
--- a/compiler/typecheck/TcTypeable.hs
+++ b/compiler/typecheck/TcTypeable.hs
@@ -17,10 +17,11 @@ import GhcPrelude
 import BasicTypes ( Boxity(..), neverInlinePragma, SourceText(..) )
 import TcBinds( addTypecheckedBinds )
 import IfaceEnv( newGlobalBinder )
-import TyCoRep( Type(..), TyLit(..), isLiftedTypeKind )
+import TyCoRep( Type(..), TyLit(..) )
 import TcEnv
 import TcEvidence ( mkWpTyApps )
 import TcRnMonad
+import TcTypeableValidity
 import HscTypes ( lookupId )
 import PrelNames
 import TysPrim ( primTyCons )
@@ -45,7 +46,6 @@ import FastString ( FastString, mkFastString, fsLit )
 
 import Control.Monad.Trans.State
 import Control.Monad.Trans.Class (lift)
-import Data.Maybe ( isJust )
 import Data.Word( Word64 )
 
 {- Note [Grand plan for Typeable]
@@ -412,38 +412,6 @@ mkTyConRepBinds stuff todo (TypeableTyCon {..})
            tycon_rep_bind = mkVarBind tycon_rep_id tycon_rep_rhs
        return $ unitBag tycon_rep_bind
 
--- | Here is where we define the set of Typeable types. These exclude type
--- families and polytypes.
-tyConIsTypeable :: TyCon -> Bool
-tyConIsTypeable tc =
-       isJust (tyConRepName_maybe tc)
-    && typeIsTypeable (dropForAlls $ tyConKind tc)
-      -- Ensure that the kind of the TyCon, with its initial foralls removed,
-      -- is representable (e.g. has no higher-rank polymorphism or type
-      -- synonyms).
-
--- | Is a particular 'Type' representable by @Typeable@? Here we look for
--- polytypes and types containing casts (which may be, for instance, a type
--- family).
-typeIsTypeable :: Type -> Bool
--- We handle types of the form (TYPE LiftedRep) specifically to avoid
--- looping on (tyConIsTypeable RuntimeRep). We used to consider (TYPE rr)
--- to be typeable without inspecting rr, but this exhibits bad behavior
--- when rr is a type family.
-typeIsTypeable ty
-  | Just ty' <- coreView ty         = typeIsTypeable ty'
-typeIsTypeable ty
-  | isLiftedTypeKind ty             = True
-typeIsTypeable (TyVarTy _)          = True
-typeIsTypeable (AppTy a b)          = typeIsTypeable a && typeIsTypeable b
-typeIsTypeable (FunTy _ a b)        = typeIsTypeable a && typeIsTypeable b
-typeIsTypeable (TyConApp tc args)   = tyConIsTypeable tc
-                                   && all typeIsTypeable args
-typeIsTypeable (ForAllTy{})         = False
-typeIsTypeable (LitTy _)            = True
-typeIsTypeable (CastTy{})           = False
-typeIsTypeable (CoercionTy{})       = False
-
 -- | Maps kinds to 'KindRep' bindings. This binding may either be defined in
 -- some other module (in which case the @Maybe (LHsExpr Id@ will be 'Nothing')
 -- or a binding which we generated in the current module (in which case it will
diff --git a/compiler/typecheck/TcTypeableValidity.hs b/compiler/typecheck/TcTypeableValidity.hs
new file mode 100644
index 0000000000..9e30be3589
--- /dev/null
+++ b/compiler/typecheck/TcTypeableValidity.hs
@@ -0,0 +1,46 @@
+{-
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 1992-1999
+-}
+
+-- | This module is separate from "TcTypeable" because the functions in this
+-- module are used in "ClsInst", and importing "TcTypeable" from "ClsInst"
+-- would lead to an import cycle.
+module TcTypeableValidity (tyConIsTypeable, typeIsTypeable) where
+
+import GhcPrelude
+
+import TyCoRep
+import TyCon
+import Type
+
+import Data.Maybe (isJust)
+
+-- | Is a particular 'TyCon' representable by @Typeable@?. These exclude type
+-- families and polytypes.
+tyConIsTypeable :: TyCon -> Bool
+tyConIsTypeable tc =
+       isJust (tyConRepName_maybe tc)
+    && typeIsTypeable (dropForAlls $ tyConKind tc)
+
+-- | Is a particular 'Type' representable by @Typeable@? Here we look for
+-- polytypes and types containing casts (which may be, for instance, a type
+-- family).
+typeIsTypeable :: Type -> Bool
+-- We handle types of the form (TYPE LiftedRep) specifically to avoid
+-- looping on (tyConIsTypeable RuntimeRep). We used to consider (TYPE rr)
+-- to be typeable without inspecting rr, but this exhibits bad behavior
+-- when rr is a type family.
+typeIsTypeable ty
+  | Just ty' <- coreView ty         = typeIsTypeable ty'
+typeIsTypeable ty
+  | isLiftedTypeKind ty             = True
+typeIsTypeable (TyVarTy _)          = True
+typeIsTypeable (AppTy a b)          = typeIsTypeable a && typeIsTypeable b
+typeIsTypeable (FunTy _ a b)        = typeIsTypeable a && typeIsTypeable b
+typeIsTypeable (TyConApp tc args)   = tyConIsTypeable tc
+                                   && all typeIsTypeable args
+typeIsTypeable (ForAllTy{})         = False
+typeIsTypeable (LitTy _)            = True
+typeIsTypeable (CastTy{})           = False
+typeIsTypeable (CoercionTy{})       = False
diff --git a/testsuite/tests/typecheck/should_fail/T15862.hs b/testsuite/tests/typecheck/should_fail/T15862.hs
new file mode 100644
index 0000000000..c98b5939d1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15862.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UnboxedSums #-}
+module Bug where
+
+import Data.Kind
+import Type.Reflection
+
+newtype Foo = MkFoo (forall a. a)
+
+foo :: TypeRep MkFoo
+foo = typeRep @MkFoo
+
+type family F a
+type instance F Int = Type
+
+data Bar = forall (a :: F Int). MkBar a
+
+bar :: TypeRep (MkBar True)
+bar = typeRep
+
+data Quux = MkQuux (# Bool | Int #)
+
+quux :: TypeRep MkQuux
+quux = typeRep
+
+data Quuz :: (Type ~ Type) => Type where
+  MkQuuz :: Quuz
+
+quuz :: TypeRep MkQuuz
+quuz = typeRep
diff --git a/testsuite/tests/typecheck/should_fail/T15862.stderr b/testsuite/tests/typecheck/should_fail/T15862.stderr
new file mode 100644
index 0000000000..97fbfab166
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15862.stderr
@@ -0,0 +1,28 @@
+
+T15862.hs:17:7: error:
+    • No instance for (Typeable 'MkFoo) arising from a use of ‘typeRep’
+        GHC can't yet do polykinded
+          Typeable ('MkFoo :: (forall a. a) -> Foo)
+    • In the expression: typeRep @MkFoo
+      In an equation for ‘foo’: foo = typeRep @MkFoo
+
+T15862.hs:25:7: error:
+    • No instance for (Typeable 'MkBar) arising from a use of ‘typeRep’
+        GHC can't yet do polykinded Typeable ('MkBar :: Bool -> Bar)
+    • In the expression: typeRep
+      In an equation for ‘bar’: bar = typeRep
+
+T15862.hs:30:8: error:
+    • No instance for (Typeable 'MkQuux)
+        arising from a use of ‘typeRep’
+        GHC can't yet do polykinded
+          Typeable ('MkQuux :: (# Bool | Int #) -> Quux)
+    • In the expression: typeRep
+      In an equation for ‘quux’: quux = typeRep
+
+T15862.hs:36:8: error:
+    • No instance for (Typeable 'MkQuuz)
+        arising from a use of ‘typeRep’
+        GHC can't yet do polykinded Typeable ('MkQuuz :: Quuz)
+    • In the expression: typeRep
+      In an equation for ‘quuz’: quuz = typeRep
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 7ee15ebc4c..0b0ae59391 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -503,6 +503,7 @@ test('T15797', normal, compile_fail, [''])
 test('T15799', normal, compile_fail, [''])
 test('T15801', normal, compile_fail, [''])
 test('T15816', normal, compile_fail, [''])
+test('T15862', normal, compile_fail, [''])
 test('T16059a', normal, compile_fail, [''])
 test('T16059c', [extra_files(['T16059b.hs'])], multimod_compile_fail,
     ['T16059c', '-v0'])