    {-|
    Description : utilities for working with "Data.Functor.Compose"
    Copyright   : (c) Galois, Inc 2014-2019
    Maintainer  : Langston Barrett <langston@galois.com>

    Utilities for working with "Data.Functor.Compose".

    NB: This module contains an orphan instance. It will be included in GHC 8.10,
    see https://gitlab.haskell.org/ghc/ghc/merge_requests/273 and also
    https://github.com/haskell-compat/base-orphans/issues/49.
    -}

    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE Safe #-}
    module Data.Parameterized.Compose
      ( testEqualityComposeBare
      ) where

    import Data.Functor.Compose
    import Data.Kind
    import Data.Orphans () -- For the TestEquality (Compose f g) instance
    import Data.Type.Equality

    -- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.
    --
    -- See https://gitlab.haskell.org/ghc/ghc/merge_requests/273.
    testEqualityComposeBare :: forall k l (f :: k -> Type) (g :: l -> k) x y.
                               (forall w z. f w -> f z -> Maybe (w :~: z))
                            -> Compose f g x
                            -> Compose f g y
                            -> Maybe (x :~: y)
    testEqualityComposeBare :: forall k l (f :: k -> *) (g :: l -> k) (x :: l) (y :: l).
    (forall (w :: k) (z :: k). f w -> f z -> Maybe (w :~: z))
    -> Compose f g x -> Compose f g y -> Maybe (x :~: y)
    testEqualityComposeBare forall (w :: k) (z :: k). f w -> f z -> Maybe (w :~: z)
    testEquality_ (Compose f (g x)
    x) (Compose f (g y)
    y) =
      case (f (g x) -> f (g y) -> Maybe (g x :~: g y)
    forall (w :: k) (z :: k). f w -> f z -> Maybe (w :~: z)
    testEquality_ f (g x)
    x f (g y)
    y :: Maybe (g x :~: g y)) of
        Just g x :~: g y
    Refl -> (x :~: y) -> Maybe (x :~: y)
    forall a. a -> Maybe a
    Just (x :~: x
    x :~: y
    forall {k} (a :: k). a :~: a
    Refl :: x :~: y)
        Maybe (g x :~: g y)
    Nothing   -> Maybe (x :~: y)
    forall a. Maybe a
    Nothing