TestEquality instance for Compose
authorLangston Barrett <langston.barrett@gmail.com>
Fri, 1 Feb 2019 20:33:38 +0000 (12:33 -0800)
committerMarge Bot <ben+marge-bot@smart-cactus.org>
Fri, 8 Feb 2019 16:00:19 +0000 (11:00 -0500)
libraries/base/Data/Functor/Compose.hs

index 4ddd12c..97d4a35 100644 (file)
@@ -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