{-# 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) = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Dual k a b
Dual (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 = 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 = 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 = forall {k1} (a :: k1). a :~~: a
Eq.HRefl
#endif