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 CastTy
s 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 CastTy
s also works without issue.
In light of this, why should we explicitly disallow CastTy
s 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
.