GitLab

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