For functors, the problem can be solved without wrapping data in the Dyn1 constructor.
{-# Language GADTs #-}
import Data.Dynamic
import Data.Type.Equality
import Type.Reflection
unwrap :: Functor f => TypeRep f -> Dynamic -> Maybe (f Dynamic)
unwrap rep (Dynamic (App rep' a) x) = fmap
(\HRefl -> Dynamic a <$> x)
(eqTypeRep rep rep')
unwrap _ _ = Nothing
or even
unwrap :: TypeRep f -> Dynamic -> (forall a. f a -> f a) -> Maybe Dynamic
unwrap rep (Dynamic r@(App rep' a) x) f =
do HRefl <- eqTypeRep rep rep'
pure (Dynamic r (f x))
unwrap _ _ _ = Nothing
For functors, the problem can be solved without wrapping data in the
Dyn1
constructor.or even