module Singleraeh.Equality where

import Data.Type.Equality

-- | Do one thing if @a@ and @b@ are equal, else do something else.
--
-- Handy for chaining 'testEquality's e.g. when singling type family equation
-- lists.
--
-- Use like so:
--
-- > testEqN sn sm1 _ $ testEqN sn sm2 _ $ ...
--
-- TODO really handy. give a larger, concrete example
testEqElse
    :: forall f a b r. TestEquality f
    => f a -> f b -> (a ~ b => r) -> r -> r
testEqElse :: forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse f a
sa f b
sb (a ~ b) => r
rEq r
rNEq =
    case f a -> f b -> Maybe (a :~: b)
forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f a
sa f b
sb of
      Just a :~: b
Refl -> (Any :~: Any) -> ((Any ~ Any) => r) -> r
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith Any :~: Any
forall {k} (a :: k). a :~: a
Refl r
(a ~ b) => r
(Any ~ Any) => r
rEq
      Maybe (a :~: b)
Nothing   -> r
rNEq