    {-# LANGUAGE CPP #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE PolyKinds #-}
    module Data.GADT.Compare.Monad
        ( GComparing
        , runGComparing
        , geq'
        , compare'
        ) where

    import Control.Applicative
    import Control.Monad
    import Data.GADT.Compare
    import Data.Type.Equality ((:~:) (..))

    -- A monad allowing gcompare to be defined in the same style as geq
    newtype GComparing a b t = GComparing (Either (GOrdering a b) t)

    instance Functor (GComparing a b) where fmap :: forall a b. (a -> b) -> GComparing a b a -> GComparing a b b
    fmap a -> b
    f (GComparing Either (GOrdering a b) a
    x) = Either (GOrdering a b) b -> GComparing a b b
    forall {k} (a :: k) (b :: k) t.
    Either (GOrdering a b) t -> GComparing a b t
    GComparing ((GOrdering a b -> Either (GOrdering a b) b)
    -> (a -> Either (GOrdering a b) b)
    -> Either (GOrdering a b) a
    -> Either (GOrdering a b) b
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either GOrdering a b -> Either (GOrdering a b) b
    forall a b. a -> Either a b
    Left (b -> Either (GOrdering a b) b
    forall a b. b -> Either a b
    Right (b -> Either (GOrdering a b) b)
    -> (a -> b) -> a -> Either (GOrdering a b) b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> b
    f) Either (GOrdering a b) a
    x)
    instance Monad (GComparing a b) where
        return :: forall a. a -> GComparing a b a
    return = a -> GComparing a b a
    forall a. a -> GComparing a b a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
        GComparing (Left  GOrdering a b
    x) >>= :: forall a b.
    GComparing a b a -> (a -> GComparing a b b) -> GComparing a b b
    >>= a -> GComparing a b b
    f = Either (GOrdering a b) b -> GComparing a b b
    forall {k} (a :: k) (b :: k) t.
    Either (GOrdering a b) t -> GComparing a b t
    GComparing (GOrdering a b -> Either (GOrdering a b) b
    forall a b. a -> Either a b
    Left GOrdering a b
    x)
        GComparing (Right a
    x) >>= a -> GComparing a b b
    f = a -> GComparing a b b
    f a
    x
    instance Applicative (GComparing a b) where
        pure :: forall a. a -> GComparing a b a
    pure = Either (GOrdering a b) a -> GComparing a b a
    forall {k} (a :: k) (b :: k) t.
    Either (GOrdering a b) t -> GComparing a b t
    GComparing (Either (GOrdering a b) a -> GComparing a b a)
    -> (a -> Either (GOrdering a b) a) -> a -> GComparing a b a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Either (GOrdering a b) a
    forall a b. b -> Either a b
    Right
        <*> :: forall a b.
    GComparing a b (a -> b) -> GComparing a b a -> GComparing a b b
    (<*>) = GComparing a b (a -> b) -> GComparing a b a -> GComparing a b b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    geq' :: GCompare t => t a -> t b -> GComparing x y (a :~: b)
    geq' :: forall {k} {k} (t :: k -> *) (a :: k) (b :: k) (x :: k) (y :: k).
    GCompare t =>
    t a -> t b -> GComparing x y (a :~: b)
    geq' t a
    x t b
    y = Either (GOrdering x y) (a :~: b) -> GComparing x y (a :~: b)
    forall {k} (a :: k) (b :: k) t.
    Either (GOrdering a b) t -> GComparing a b t
    GComparing (case t a -> t b -> GOrdering a b
    forall (a :: k) (b :: k). t a -> t b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare t a
    x t b
    y of
        GOrdering a b
    GLT -> GOrdering x y -> Either (GOrdering x y) (a :~: b)
    forall a b. a -> Either a b
    Left GOrdering x y
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
        GOrdering a b
    GEQ -> (a :~: b) -> Either (GOrdering x y) (a :~: b)
    forall a b. b -> Either a b
    Right a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
        GOrdering a b
    GGT -> GOrdering x y -> Either (GOrdering x y) (a :~: b)
    forall a b. a -> Either a b
    Left GOrdering x y
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT)

    compare' :: a -> a -> GComparing a b ()
    compare' a
    x a
    y = Either (GOrdering a b) () -> GComparing a b ()
    forall {k} (a :: k) (b :: k) t.
    Either (GOrdering a b) t -> GComparing a b t
    GComparing (Either (GOrdering a b) () -> GComparing a b ())
    -> Either (GOrdering a b) () -> GComparing a b ()
    forall a b. (a -> b) -> a -> b
    $ case a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    x a
    y of
        Ordering
    LT -> GOrdering a b -> Either (GOrdering a b) ()
    forall a b. a -> Either a b
    Left GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
        Ordering
    EQ -> () -> Either (GOrdering a b) ()
    forall a b. b -> Either a b
    Right ()
        Ordering
    GT -> GOrdering a b -> Either (GOrdering a b) ()
    forall a b. a -> Either a b
    Left GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT

    runGComparing :: GComparing a b (GOrdering a b) -> GOrdering a b
    runGComparing (GComparing Either (GOrdering a b) (GOrdering a b)
    x) = (GOrdering a b -> GOrdering a b)
    -> (GOrdering a b -> GOrdering a b)
    -> Either (GOrdering a b) (GOrdering a b)
    -> GOrdering a b
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either GOrdering a b -> GOrdering a b
    forall a. a -> a
    id GOrdering a b -> GOrdering a b
    forall a. a -> a
    id Either (GOrdering a b) (GOrdering a b)
    x