TestEquality.hs

{-# LANGUAGE CPP       #-}
{-# LANGUAGE MagicHash #-}

-- | Utilities for writing 'Eq' instances for GADTs
module C.Expr.Util.TestEquality (
    equals1
  , equals2
  ) where

import Data.GADT.Compare
import Data.Kind
import Data.Type.Equality
import GHC.Exts
import Unsafe.Coerce (unsafeCoerce)

-- $setup
-- >>> :seti -XDataKinds -XGADTs

{-------------------------------------------------------------------------------
  Utilities for writing 'Eq' instances for GADTs
-------------------------------------------------------------------------------}

infixr 4 `equals1`
infixr 4 `equals2`

-- | Check whether two GADT values of type @k ->Type@ are equal.
--
-- If so, also return a proof that the tags were equal.
--
-- NB: this is stricter than 'testEquality', as 'testEquality' is supposed
-- to return @Just Refl@ whenever the tags are equal, even when the values
-- themselves are different.
--
-- NB: Doesn't work for types with type indices not-directly implied by
-- constructor "tags":
--
-- >>> data SBool (b :: Bool) where STrue :: SBool True; SFalse :: SBool False
-- >>> instance Eq (SBool b) where STrue == STrue = True; SFalse == SFalse = False
-- >>> data Foo b = Foo1 (SBool b) | Foo2 (SBool b) deriving Eq
-- >>>  equals1 (Foo1 STrue) (Foo1 SFalse)
-- *** Exception: ...Non-exhaustive patterns in function ==
-- ...
--
-- The GHC generated Eq instance for SBool would have default case, so this example *could* work.
-- If you want to be safe, use 'Data.GADT.Compare.geq' from @some@ package.
--
equals1 :: forall a tag1 tag2.
  ( forall tag. Eq ( a tag )
#if MIN_VERSION_base(4,20,0)
  , forall tag. DataToTag ( a tag )
#endif
  ) => a tag1 -> a tag2 -> Maybe ( tag1 :~: tag2 )
equals1 k1 k2
  | -- Fail-fast: comparing the tag first.
    isTrue# ( dataToTag# k1 ==# dataToTag# k2 )
    -- Assume the types are the same; this allows us to use the 'Eq' instance.
  , Refl <- ( unsafeCoerce Refl :: tag1 :~: tag2 )
  , k1 == k2
  -- The values are equal (according to the 'Eq' instance): this justifies the
  -- unsafe coercion above, assuming that the 'Eq' instance is lawful.
  = Just $ unsafeCoerce Refl
  | otherwise
  = Nothing

-- | Check whether two GADT values of type @k -> l ->Type@ are equal.
--
-- If so, also return a proof that the tags were equal.
--
-- NB: this is stricter than 'testEquality', as 'testEquality' is supposed
-- to return @Just Refl@ whenever the tags are equal, even when the values
-- themselves are different.
equals2 :: forall a k1 k2 l1 l2.
  ( forall k l. Eq ( a k l)
#if MIN_VERSION_base(4,20,0)
  , forall k l. DataToTag ( a k l )
#endif
  ) => a k1 l1 -> a k2 l2 -> Maybe ( '( k1, l1 ) :~: '( k2, l2 ) )
equals2 k1 k2
  | -- Fail-fast: comparing the tag first.
    isTrue# ( dataToTag# k1 ==# dataToTag# k2 )
    -- Assume the types are the same; this allows us to use the 'Eq' instance.
  , Refl <- ( unsafeCoerce Refl :: '( k1, l1 ) :~: '( k2, l2 ) )
  , k1 == k2
  -- The values are equal (according to the 'Eq' instance): this justifies the
  -- unsafe coercion above, assuming that the 'Eq' instance is lawful.
  = Just $ unsafeCoerce Refl
  | otherwise
  = Nothing

{-------------------------------------------------------------------------------
  Internal auxiliary
-------------------------------------------------------------------------------}

-- | Wrapper that provides a 'GEq' instance definition using 'equals1'
type ApEq :: ( k -> Type ) -> k -> Type
newtype ApEq f a = ApEq ( f a )

instance forall f.
  ( forall tag. Eq ( f tag )
#if MIN_VERSION_base(4,20,0)
  , forall tag. DataToTag (f tag )
#endif
  ) => GEq ( ApEq f ) where
  geq ( ApEq k1 ) ( ApEq k2 ) = equals1 k1 k2