content: {-|
  Description : Classes for working with type of kind @k -> *@
  Copyright   : (c) Galois, Inc 2014-2019
  Maintainer  : Joe Hendrix <jhendrix@galois.com>
  
  This module declares classes for working with types with the kind
  @k -> *@ for any kind @k@.  These are generalizations of the
  "Data.Functor.Classes" types as they work with any kind @k@, and are
  not restricted to '*'.
  -}
  {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE DefaultSignatures #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE Safe #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  module Data.Parameterized.Classes
    ( -- * Equality exports
      Equality.TestEquality(..)
    , (Equality.:~:)(..)
    , EqF(..)
    , PolyEq(..)
      -- * Ordering generalization
    , OrdF(..)
    , lexCompareF
    , OrderingF(..)
    , joinOrderingF
    , orderingF_refl
    , toOrdering
    , fromOrdering
    , ordFCompose
      -- * Typeclass generalizations
    , ShowF(..)
    , showsF
    , HashableF(..)
    , CoercibleF(..)
      -- * Type function application constructor
    , TypeAp(..)
      -- * Optics generalizations
    , IndexF
    , IxValueF
    , IxedF(..)
    , IxedF'(..)
    , AtF(..)
      -- * KnownRepr
    , KnownRepr(..)
      -- * Re-exports
    , Data.Hashable.Hashable(..)
    , Data.Maybe.isJust
    ) where
  
  import Data.Functor.Const
  import Data.Functor.Compose (Compose(..))
  import Data.Kind
  import Data.Hashable
  import Data.Maybe (isJust)
  import Data.Proxy
  import Data.Type.Equality as Equality
  
  import Data.Parameterized.Compose ()
  
  -- We define these type alias here to avoid importing Control.Lens
  -- modules, as this apparently causes problems with the safe Hasekll
  -- checking.
  type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
  type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s
  
  ------------------------------------------------------------------------
  -- CoercibleF
  
  -- | An instance of 'CoercibleF' gives a way to coerce between
  --   all the types of a family.  We generally use this to witness
  --   the fact that the type parameter to @rtp@ is a phantom type
  --   by giving an implementation in terms of Data.Coerce.coerce.
  class CoercibleF (rtp :: k -> Type) where
    coerceF :: rtp a -> rtp b
  
  instance CoercibleF (Const x) where
    coerceF (Const x) = Const x
  
  ------------------------------------------------------------------------
  -- EqF
  
  -- | @EqF@ provides a method @eqF@ for testing whether two parameterized
  -- types are equal.
  --
  -- Unlike 'TestEquality', this only works when the type arguments are
  -- the same, and does not provide a proof that the types have the same
  -- type when they are equal. Thus this can be implemented over
  -- parameterized types that are unable to provide evidence that their
  -- type arguments are equal.
  class EqF (f :: k -> Type) where
    eqF :: f a -> f a -> Bool
  
  instance Eq a => EqF (Const a) where
    eqF (Const x) (Const y) = x == y
  
  instance EqF Proxy where
    eqF _ _ = True
  
  ------------------------------------------------------------------------
  -- PolyEq
  
  -- | A polymorphic equality operator that generalizes 'TestEquality'.
  class PolyEq u v where
    polyEqF :: u -> v -> Maybe (u :~: v)
  
    polyEq :: u -> v -> Bool
    polyEq x y = isJust (polyEqF x y)
  
  ------------------------------------------------------------------------
  -- Ordering
  
  -- | Ordering over two distinct types with a proof they are equal.
  data OrderingF x y where
    LTF :: OrderingF x y
    EQF :: OrderingF x x
    GTF :: OrderingF x y
  
  orderingF_refl :: OrderingF x y -> Maybe (x :~: y)
  orderingF_refl o =
    case o of
      LTF -> Nothing
      EQF -> Just Refl
      GTF -> Nothing
  
  -- | Convert 'OrderingF' to standard ordering.
  toOrdering :: OrderingF x y -> Ordering
  toOrdering LTF = LT
  toOrdering EQF = EQ
  toOrdering GTF = GT
  
  -- | Convert standard ordering to 'OrderingF'.
  fromOrdering :: Ordering -> OrderingF x x
  fromOrdering LT = LTF
  fromOrdering EQ = EQF
  fromOrdering GT = GTF
  
  -- | @joinOrderingF x y@ first compares on @x@, returning an
  -- equivalent value if it is not `EQF`.  If it is `EQF`, it returns @y@.
  joinOrderingF :: forall j k (a :: j) (b :: j) (c :: k) (d :: k)
                .  OrderingF a b
                -> (a ~ b => OrderingF c d)
                -> OrderingF c d
  joinOrderingF EQF y = y
  joinOrderingF LTF _ = LTF
  joinOrderingF GTF _ = GTF
  
  ------------------------------------------------------------------------
  -- OrdF
  
  -- | The `OrdF` class is a total ordering over parameterized types so
  -- that types with different parameters can be compared.
  --
  -- Instances of `OrdF` are expected to satisfy the following laws:
  --
  -- [__Transitivity__]: if @leqF x y && leqF y z@ = 'True', then @leqF x = z@ = @True@
  -- [__Reflexivity__]: @leqF x x@ = @True@
  -- [__Antisymmetry__]: if @leqF x y && leqF y x@ = 'True', then @testEquality x y@ = @Just Refl@
  --
  -- Note that the following operator interactions are expected to hold:
  --
  -- * @geqF x y@ iff @leqF y x@
  -- * @ltF  x y@ iff @leqF x y && testEquality x y = Nothing@
  -- * @gtF  x y@ iff @ltF y x@
  -- * @ltF  x y@ iff @compareF x y == LTF@
  -- * @gtF  x y@ iff @compareF x y == GTF@
  -- * @isJust (testEquality x y)@ iff @compareF x y == EQF@
  --
  -- Furthermore, when @x@ and @y@ both have type @(k tp)@, we expect:
  --
  -- * @toOrdering (compareF x y)@ equals @compare x y@ when @Ord (k tp)@ has an instance.
  -- * @isJust (testEquality x y)@ equals @x == y@ when @Eq (k tp)@ has an instance.
  --
  -- Minimal complete definition: either 'compareF' or 'leqF'.
  -- Using 'compareF' can be more efficient for complex types.
  class TestEquality ktp => OrdF (ktp :: k -> Type) where
    {-# MINIMAL compareF | leqF #-}
  
    compareF :: ktp x -> ktp y -> OrderingF x y
    compareF x y =
      case testEquality x y of
        Just Refl -> EQF
        Nothing | leqF x y -> LTF
                | otherwise -> GTF
  
    leqF :: ktp x -> ktp y -> Bool
    leqF x y =
      case compareF x y of
        LTF -> True
        EQF -> True
        GTF -> False
  
    ltF :: ktp x -> ktp y -> Bool
    ltF x y =
      case compareF x y of
        LTF -> True
        EQF -> False
        GTF -> False
  
    geqF :: ktp x -> ktp y -> Bool
    geqF x y =
      case compareF x y of
        LTF -> False
        EQF -> True
        GTF -> True
  
    gtF :: ktp x -> ktp y -> Bool
    gtF x y =
      case compareF x y of
        LTF -> False
        EQF -> False
        GTF -> True
  
  -- | Compare two values, and if they are equal compare the next values,
  -- otherwise return LTF or GTF
  lexCompareF :: forall j k (f :: j -> Type) (a :: j) (b :: j) (c :: k) (d :: k)
               .  OrdF f
              => f a
              -> f b
              -> (a ~ b => OrderingF c d)
              -> OrderingF c d
  lexCompareF x y = joinOrderingF (compareF x y)
  
  -- | If the \"outer\" functor has an 'OrdF' instance, then one can be generated
  -- for the \"inner\" functor. The type-level evidence of equality is deduced
  -- via generativity of @g@, e.g. the inference @g x ~ g y@ implies @x ~ y@.
  ordFCompose :: forall k l (f :: k -> Type) (g :: l -> k) x y.
                  (forall w z. f w -> f z -> OrderingF w z)
              -> Compose f g x
              -> Compose f g y
              -> OrderingF x y
  ordFCompose ordF_ (Compose x) (Compose y) =
    case ordF_ x y of
      LTF -> LTF
      GTF -> GTF
      EQF -> EQF
  
  instance OrdF f => OrdF (Compose f g) where
    compareF x y = ordFCompose compareF x y
  
  ------------------------------------------------------------------------
  -- ShowF
  
  -- | A parameterized type that can be shown on all instances.
  --
  -- To implement @'ShowF' g@, one should implement an instance @'Show'
  -- (g tp)@ for all argument types @tp@, then write an empty instance
  -- @instance 'ShowF' g@.
  class ShowF (f :: k -> Type) where
    -- | Provides a show instance for each type.
    withShow :: p f -> q tp -> (Show (f tp) => a) -> a
  
    default withShow :: Show (f tp) => p f -> q tp -> (Show (f tp) => a) -> a
    withShow _ _ x = x
  
    showF :: forall tp . f tp -> String
    showF x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (show x)
  
    -- | Like 'showsPrec', the precedence argument is /one more/ than the
    -- precedence of the enclosing context.
    showsPrecF :: forall tp. Int -> f tp -> String -> String
    showsPrecF p x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (showsPrec p x)
  
  showsF :: ShowF f => f tp -> String -> String
  showsF x = showsPrecF 0 x
  
  instance Show x => ShowF (Const x)
  
  instance ShowF Proxy
  
  ------------------------------------------------------------------------
  -- IxedF
  
  type family IndexF       (m :: Type) :: k -> Type
  type family IxValueF     (m :: Type) :: k -> Type
  
  -- | Parameterized generalization of the lens @Ixed@ class.
  class IxedF k m where
    -- | Given an index into a container, build a traversal that visits
    --   the given element in the container, if it exists.
    ixF :: forall (x :: k). IndexF m x -> Traversal' m (IxValueF m x)
  
  -- | Parameterized generalization of the lens @Ixed@ class,
  --   but with the guarantee that indexes exist in the container.
  class IxedF k m => IxedF' k m where
    -- | Given an index into a container, build a lens that
    --   points into the given element in the container.
    ixF' :: forall (x :: k). IndexF m x -> Lens' m (IxValueF m x)
  
  ------------------------------------------------------------------------
  -- AtF
  
  -- | Parameterized generalization of the lens @At@ class.
  class IxedF k m => AtF k m where
    -- | Given an index into a container, build a lens that points into
    --   the given position in the container, whether or not it currently
    --   exists.  Setting values of @atF@ to a @Just@ value will insert
    --   the value if it does not already exist.
    atF :: forall (x :: k). IndexF m x -> Lens' m (Maybe (IxValueF m x))
  
  ------------------------------------------------------------------------
  -- HashableF
  
  -- | A default salt used in the implementation of 'hash'.
  defaultSalt :: Int
  #if WORD_SIZE_IN_BITS == 64
  defaultSalt = 0xdc36d1615b7400a4
  #else
  defaultSalt = 0x087fc72c
  #endif
  {-# INLINE defaultSalt #-}
  
  -- | A parameterized type that is hashable on all instances.
  class HashableF (f :: k -> Type) where
    hashWithSaltF :: Int -> f tp -> Int
  
    -- | Hash with default salt.
    hashF :: f tp -> Int
    hashF = hashWithSaltF defaultSalt
  
  instance Hashable a => HashableF (Const a) where
    hashWithSaltF s (Const x) = hashWithSalt s x
  
  ------------------------------------------------------------------------
  -- TypeAp
  
  -- | Captures the value obtained from applying a type to a function so
  -- that we can use parameterized class instance to provide unparameterized
  -- instances for specific types.
  --
  -- This is the same as `Ap` from @Control.Applicative@, but we introduce
  -- our own new type to avoid orphan instances.
  newtype TypeAp (f :: k -> Type) (tp :: k) = TypeAp (f tp)
  
  instance TestEquality f => Eq (TypeAp f tp) where
    TypeAp x == TypeAp y = isJust $ testEquality x y
  
  instance OrdF f => Ord (TypeAp f tp) where
    compare (TypeAp x) (TypeAp y) = toOrdering (compareF x y)
  
  instance ShowF f => Show (TypeAp f tp) where
    showsPrec p (TypeAp x) = showsPrecF p x
  
  instance (HashableF f, TestEquality f) => Hashable (TypeAp f tp) where
    hashWithSalt s (TypeAp x) = hashWithSaltF s x
  
  ------------------------------------------------------------------------
  -- KnownRepr
  
  -- | This class is parameterized by a kind @k@ (typically a data
  -- kind), a type constructor @f@ of kind @k -> *@ (typically a GADT of
  -- singleton types indexed by @k@), and an index parameter @ctx@ of
  -- kind @k@.
  class KnownRepr (f :: k -> Type) (ctx :: k) where
    knownRepr :: f ctx
  
  instance KnownRepr Proxy ctx where
    knownRepr = Proxy
  