TypeInType prevents Typeable from being resolved from a given
The following program is accepted without TypeInType
by GHC 8.10.2:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Dynamic
import Type.Reflection
data Liveness
= forall t. Live t
data IOA (l :: Liveness) where
IOE :: IOA (Live t)
data LTag (l :: Liveness) where
LLive :: Typeable t => TypeRep t -> LTag (Live t)
reconstruct :: Dynamic -> LTag l -> ()
reconstruct dyn l@LLive{} =
case l of
(LLive tr :: LTag (Live t)) ->
undefined $ withTypeable tr $
(fromDynamic dyn :: Maybe (IOA (Live t)))
main :: IO ()
main = undefined
It is, however, rejected with TypeInType
, as follows:
common/src/Dom/Pipe/IOA.hs:26:17: error:
• Could not deduce (Typeable t) arising from a use of ‘fromDynamic’
from the context: (l ~ 'Live t1, Typeable t1)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 -> LTag ('Live t2),
in an equation for ‘reconstruct’
at common/src/Dom/Pipe/IOA.hs:22:19-25
or from: ('Live t1 ~ 'Live t3, Typeable t3)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 -> LTag ('Live t2),
in a case alternative
at common/src/Dom/Pipe/IOA.hs:24:10-17
or from: Typeable t3
bound by a type expected by the context:
Typeable t3 => Maybe (IOA ('Live t1))
at common/src/Dom/Pipe/IOA.hs:26:16-56
• In the second argument of ‘($)’, namely
‘(fromDynamic dyn :: Maybe (IOA (Live t)))’
In the second argument of ‘($)’, namely
‘withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))’
In the expression:
undefined
$ withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))
|
26 | (fromDynamic dyn :: Maybe (IOA (Live t)))
| ^^^^^^^^^^^^^^^
Potentially related to #16627