Commit 5b8bb4c8 authored by Langston Barrett's avatar Langston Barrett

TestEquality instance for Compose

parent ef6b2833
Pipeline #1735 passed with stages
in 539 minutes and 20 seconds
{-# 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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment