https://github.com/ghc/ghc/blob/4bb54a4522d44a81b2c47233f482 52bd73c38279/testsuite/tests/polykinds/T14270.hs https://github.com/sweirich/dth/blob/2bb0c9aa9adb514b787ea56 295419fae55dc3734/examples/dynamic/DataDynamic.hs This is a pattern synonym to construct but more importantly to deconstruct an explicit `TypeRep a` into a `Typeable a` constraint

asTypeable :: TypeRep a -> Dict (Typeable a) asTypeable rep = withTypeable rep Dict

pattern Typeable :: () => Typeable a => TypeRep a pattern Typeable <- (asTypeable -> Dict) where Typeable = typeRep

Similar discussion for SingI [1], same benefits: + (Nice) direct alternative to CPS `withTypeable` + Reusable in other pattern synonyms [1] https://github.com/goldfirere/singletons/issues/273