Add pattern TypeRep (#19691), exported by Type.Reflection.

5 files changed, 90 insertions, 5 deletions

diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 962f5b82c1..2a02ec68cb 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -59,6 +59,7 @@ module Data.Typeable.Internal (
 
     -- * TypeRep
     TypeRep,
+    pattern TypeRep,
     pattern App, pattern Con, pattern Con', pattern Fun,
     typeRep,
     typeOf,
@@ -229,6 +230,41 @@ data TypeRep a where
                , trFunRes :: !(TypeRep b) }
             -> TypeRep (FUN m a b)
 
+-- | A 'TypeableInstance' wraps up a 'Typeable' instance for explicit
+-- handling. For internal use: for defining 'TypeRep' pattern.
+type TypeableInstance :: forall k. k -> Type
+data TypeableInstance a where
+ TypeableInstance :: Typeable a => TypeableInstance a
+
+-- | Get a reified 'Typeable' instance from an explicit 'TypeRep'.
+--
+-- For internal use: for defining 'TypeRep' pattern.
+typeableInstance :: forall {k :: Type} (a :: k). TypeRep a -> TypeableInstance a
+typeableInstance rep = withTypeable rep TypeableInstance
+
+-- | A explicitly bidirectional pattern synonym to construct a
+-- concrete representation of a type.
+--
+-- As an __expression__: Constructs a singleton @TypeRep a@ given a
+-- implicit 'Typeable a' constraint:
+--
+-- @
+-- TypeRep @a :: Typeable a => TypeRep a
+-- @
+--
+-- As a __pattern__: Matches on an explicit @TypeRep a@ witness bringing
+-- an implicit @Typeable a@ constraint into scope.
+--
+-- @
+-- f :: TypeRep a -> ..
+-- f TypeRep = {- Typeable a in scope -}
+-- @
+--
+-- @since 4.17.0.0
+pattern TypeRep :: forall {k :: Type} (a :: k). () => Typeable @k a => TypeRep @k a
+pattern TypeRep <- (typeableInstance -> TypeableInstance)
+  where TypeRep = typeRep
+
 {- Note [TypeRep fingerprints]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We store a Fingerprint of each TypeRep in its constructor. This allows
@@ -433,14 +469,13 @@ mkTrAppChecked :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
                   TypeRep (a :: k1 -> k2)
                -> TypeRep (b :: k1)
                -> TypeRep (a b)
-mkTrAppChecked rep@(TrApp {trAppFun = p, trAppArg = x :: TypeRep x})
+mkTrAppChecked rep@(TrApp {trAppFun = p, trAppArg = x@TypeRep :: TypeRep x})
                (y :: TypeRep y)
   | TrTyCon {trTyCon=con} <- p
   , con == funTyCon  -- cheap check first
-  , Just (IsTYPE (rx :: TypeRep rx)) <- isTYPE (typeRepKind x)
-  , Just (IsTYPE (ry :: TypeRep ry)) <- isTYPE (typeRepKind y)
-  , Just HRefl <- withTypeable x $ withTypeable rx $ withTypeable ry
-                  $ typeRep @((->) x :: TYPE ry -> Type) `eqTypeRep` rep
+  , Just (IsTYPE TypeRep) <- isTYPE (typeRepKind x)
+  , Just (IsTYPE (TypeRep :: TypeRep ry)) <- isTYPE (typeRepKind y)
+  , Just HRefl <- typeRep @((->) x :: TYPE ry -> Type) `eqTypeRep` rep
   = mkTrFun trMany x y
 mkTrAppChecked a b = mkTrApp a b
 
@@ -493,6 +528,17 @@ splitApp (TrTyCon{trTyCon = con, trKindVars = kinds})
       Refl -> IsCon con kinds
 
 -- | Use a 'TypeRep' as 'Typeable' evidence.
+--
+-- The 'TypeRep' pattern synonym brings a 'Typeable' constraint into
+-- scope and can be used in place of 'withTypeable'.
+--
+-- @
+-- f :: TypeRep a -> ..
+-- f rep = withTypeable {- Typeable a in scope -}
+--
+-- f :: TypeRep a -> ..
+-- f TypeRep = {- Typeable a in scope -}
+-- @
 withTypeable :: forall k (a :: k) rep (r :: TYPE rep). ()
              => TypeRep a -> (Typeable a => r) -> r
 withTypeable rep k = withDict @(TypeRep a) @(Typeable a) rep k
diff --git a/libraries/base/Type/Reflection.hs b/libraries/base/Type/Reflection.hs
index be9af91772..f5f9882389 100644
--- a/libraries/base/Type/Reflection.hs
+++ b/libraries/base/Type/Reflection.hs
@@ -39,6 +39,7 @@ module Type.Reflection
       -- * Type representations
       -- ** Type-Indexed
     , I.TypeRep
+    , pattern I.TypeRep
     , I.typeOf
     , pattern I.App, pattern I.Con, pattern I.Con', pattern I.Fun
     , I.typeRepTyCon
diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md
index b258f984e4..ece5f77a75 100644
--- a/libraries/base/changelog.md
+++ b/libraries/base/changelog.md
@@ -1,5 +1,9 @@
 # Changelog for [`base` package](http://hackage.haskell.org/package/base)
 
+## 4.17.0.0 *TBA*
+
+  * Add explicitly bidirectional `pattern TypeRep` to `Type.Reflection`.
+
 ## 4.16.0.0 *TBA*
 
   * Make it possible to promote `Natural`s and remove the separate `Nat` kind.
diff --git a/testsuite/tests/lib/base/T19691.hs b/testsuite/tests/lib/base/T19691.hs
new file mode 100644
index 0000000000..0525b8b499
--- /dev/null
+++ b/testsuite/tests/lib/base/T19691.hs
@@ -0,0 +1,33 @@
+{-# Language DerivingStrategies       #-}
+{-# Language TypeApplications         #-}
+{-# Language GADTs                    #-}
+{-# Language StandaloneKindSignatures #-}
+{-# Language TypeFamilies             #-}
+
+import Data.Kind
+import Type.Reflection
+
+type Dict :: Constraint -> Type
+data Dict cls where
+ Dict :: cls => Dict cls
+
+deriving stock
+  instance Show (Dict cls)
+
+type WitnessList :: forall k. k -> Type
+data WitnessList as where
+  WitnessList :: Typeable a => WitnessList (f a)
+
+deriving stock
+  instance Show (WitnessList as)
+
+toDict :: TypeRep a -> Dict (Typeable a)
+toDict TypeRep = Dict
+
+witness :: TypeRep as -> Maybe (WitnessList as)
+witness (App _ TypeRep) = Just WitnessList
+
+main :: IO ()
+main = do
+  print (toDict  (TypeRep @[Int]))
+  print (witness (TypeRep @[Int]))
diff --git a/testsuite/tests/lib/base/all.T b/testsuite/tests/lib/base/all.T
index 6bf890c148..170bfe4d85 100644
--- a/testsuite/tests/lib/base/all.T
+++ b/testsuite/tests/lib/base/all.T
@@ -3,3 +3,4 @@ test('T16586', normal, compile_and_run, ['-O2'])
 # Event-manager not supported on Windows
 test('T16916', when(opsys('mingw32'), skip), compile_and_run, ['-O2 -threaded -with-rtsopts="-I0" -rtsopts'])
 test('T17310', normal, compile, [''])
+test('T19691', normal, compile, [''])
\ No newline at end of file