    {-# LANGUAGE CPP #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE Trustworthy #-}
    -----------------------------------------------------------------------------
    -- |
    -- Copyright   :  (C) 2011-2015 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    --
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  provisional
    -- Portability :  polykinds
    --
    ----------------------------------------------------------------------------

    module Data.Groupoid
      ( Groupoid(..)
      ) where

    import Data.Semigroupoid
    import Data.Semigroupoid.Dual
    import qualified Data.Type.Coercion as Co
    import qualified Data.Type.Equality as Eq

    -- | semigroupoid with inverses. This technically should be a category with inverses, except we need to use Ob to define the valid objects for the category
    class Semigroupoid k => Groupoid k where
      inv :: k a b -> k b a

    instance Groupoid k => Groupoid (Dual k) where
      inv :: forall (a :: k) (b :: k). Dual k a b -> Dual k b a
    inv (Dual k b a
    k) = k a b -> Dual k b a
    forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
    k2 b a -> Dual k2 a b
    Dual (k b a -> k a b
    forall (a :: k) (b :: k). k a b -> k b a
    forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
    Groupoid k =>
    k a b -> k b a
    inv k b a
    k)

    instance Groupoid Co.Coercion where
      inv :: forall (a :: k) (b :: k). Coercion a b -> Coercion b a
    inv = Coercion a b -> Coercion b a
    forall k (a :: k) (b :: k). Coercion a b -> Coercion b a
    Co.sym

    instance Groupoid (Eq.:~:) where
      inv :: forall (a :: k) (b :: k). (a :~: b) -> b :~: a
    inv = (a :~: b) -> b :~: a
    forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
    Eq.sym

    #if MIN_VERSION_base(4,10,0)
    instance Groupoid (Eq.:~~:) where
      inv :: forall (a :: k) (b :: k). (a :~~: b) -> b :~~: a
    inv a :~~: b
    Eq.HRefl = b :~~: a
    b :~~: b
    forall {k1} (a :: k1). a :~~: a
    Eq.HRefl
    #endif