{-|
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 (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 -> forall a. a -> Maybe a
Just (forall {k} (a :: k). a :~: a
Refl :: x :~: y)
    Maybe (g x :~: g y)
Nothing   -> forall a. Maybe a
Nothing