Consider supporting Typeable instances for data types containing casts

Consider this piece of code, inspired by #15862 (comment 163375):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind
import Type.Reflection

type family F a
type instance F Int = Type

data D = forall (a :: F Int). MkD a

tr :: TypeRep (MkD Bool)
tr = typeRep

Currently (on GHC HEAD, which has a fix for #15862 (closed)), this fails with:

[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:17:6: error:
    • No instance for (Typeable 'MkD) arising from a use of ‘typeRep’
        GHC can't yet do polykinded Typeable ('MkD :: * -> D)
    • In the expression: typeRep
      In an equation for ‘tr’: tr = typeRep
   |
17 | tr = typeRep
   |      ^^^^^^^

Let's try making a very small change to MkD (note the lack of an explicit a field):

data D' = forall (a :: F Int). MkD'

Accordingly, let's also update tr:

tr :: TypeRep (MkD' @Bool)
tr = typeRep

After these changes, the program now compiles! This is very strange. Why is GHC able to conjure up a Typeable instance for MkD, but not for MkD'?

Some digging revealed the immediate cause of why this is happening. In the bowels of TcTypeable, we only generate Typeable information for type constructors whose kinds don't contain any casts (e.g., the cast implied by the use of F Int), as revealed in this line of code:

typeIsTypeable (CastTy{})           = False

But that clearly isn't the full story, since both MkD and MkD' contain casts. The other piece of the puzzle is this line of code:

tyConIsTypeable tc =
       isJust (tyConRepName_maybe tc)
    && typeIsTypeable (dropForAlls $ tyConKind tc)

The use of dropForAlls means that GHC won't catch the CastTy in the type of MkD', since it's only found in a forall. On the other hand, MkD has a CastTy that's outside of a forall, so GHC does flag that one.

---

Initially, my reaction was to change GHC to make both MkD and MkD' an error. But then I had a thought: why are CastTys disallowed in typeIsTypeable in the first place? If I compile the version of the program that contains MkD', I get this perfectly sensible-looking Core:

-- RHS size: {terms: 3, types: 4, coercions: 0, joins: 0/0}
$dTypeable_r1Mi :: TypeRep @* Bool
[GblId]
$dTypeable_r1Mi
  = base-4.13.0.0:Data.Typeable.Internal.mkTrCon
      @ * @ Bool GHC.Types.$tcBool (GHC.Types.[] @ SomeTypeRep)

-- RHS size: {terms: 6, types: 12, coercions: 9, joins: 0/0}
$dTypeable1_r1Mj
  :: TypeRep @D' ('MkD' @(Bool |> Sym (Bug.D:R:FInt[0])))
[GblId]
$dTypeable1_r1Mj
  = base-4.13.0.0:Data.Typeable.Internal.mkTrCon
      @ D'
      @ ('MkD' @(Bool |> Sym (Bug.D:R:FInt[0])))
      Bug.$tc'MkD'
      (GHC.Types.:
         @ SomeTypeRep
         (base-4.13.0.0:Data.Typeable.Internal.SomeTypeRep
            @ (F Int)
            @ (Bool |> Sym (Bug.D:R:FInt[0]))
            ($dTypeable_r1Mi
             `cast` ((TypeRep
                        (Sym (Bug.D:R:FInt[0]))
                        (Sym (GRefl nominal (Bool |> Sym (Bug.D:R:FInt[0]))
                                  (Bug.D:R:FInt[0]))))_R
                     :: (TypeRep @* Bool :: *)
                        ~R# (TypeRep @(F Int) (Bool |> Sym (Bug.D:R:FInt[0])) :: *))))
         (GHC.Types.[] @ SomeTypeRep))

-- RHS size: {terms: 2, types: 5, coercions: 7, joins: 0/0}
tr :: TypeRep @D' ('MkD' @(Bool |> Sym (Bug.D:R:FInt[0])))
[GblId]
tr
  = break<0>()
    typeRep
      @ D'
      @ ('MkD' @(Bool |> Sym (Bug.D:R:FInt[0])))
      ($dTypeable1_r1Mj
       `cast` (Sym (base-4.13.0.0:Data.Typeable.Internal.N:Typeable[0]) <D'>_N <'MkD'
                                                                                  @(Bool |> Sym (Bug.D:R:FInt[0]))>_N
               :: (TypeRep @D' ('MkD' @(Bool |> Sym (Bug.D:R:FInt[0]))) :: *)
                  ~R# (Typeable
                         @D' ('MkD' @(Bool |> Sym (Bug.D:R:FInt[0]))) :: Constraint)))

Indeed, this passes -dcore-lint. Every other attempt I've tried at generating Typeable instances for things containing CastTys also works without issue.

In light of this, why should we explicitly disallow CastTys in typeIsTypeable? Why not change this line to be:

typeIsTypeable (CastTy t _) = typeIsTypeable t

Note that this is a separate question from #13933, which is about CoercionTy, not CastTy.