TestEquality instance for Compose

1 files changed, 13 insertions, 1 deletions

diff --git a/libraries/base/Data/Functor/Compose.hs b/libraries/base/Data/Functor/Compose.hs
index 4ddd12cb2f..97d4a35317 100644
--- a/libraries/base/Data/Functor/Compose.hs
+++ b/libraries/base/Data/Functor/Compose.hs
@@ -1,8 +1,10 @@
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeOperators #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Functor.Compose
@@ -27,6 +29,7 @@ import Data.Functor.Classes
 import Control.Applicative
 import Data.Coerce (coerce)
 import Data.Data (Data)
+import Data.Type.Equality (TestEquality(..), (:~:)(..))
 import GHC.Generics (Generic, Generic1)
 import Text.Read (Read(..), readListDefault, readListPrecDefault)
 
@@ -118,3 +121,12 @@ instance (Alternative f, Applicative g) => Alternative (Compose f g) where
     empty = Compose empty
     (<|>) = coerce ((<|>) :: f (g a) -> f (g a) -> f (g a))
       :: forall a . Compose f g a -> Compose f g a -> Compose f g a
+
+-- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.
+--
+-- @since 4.13.0.0
+instance (TestEquality f) => TestEquality (Compose f g) where
+  testEquality (Compose x) (Compose y) =
+    case testEquality x y of -- :: Maybe (g x :~: g y)
+      Just Refl -> Just Refl -- :: Maybe (x :~: y)
+      Nothing   -> Nothing