{-|
Description : Classes for working with type of kind @(k -> *) -> *@
Copyright   : (c) Galois, Inc 2014-2019
Maintainer  : Langston Barrett <langston@galois.com>

This module declares classes for working with types with the kind
@(k -> *) -> *@ for any kind @k@.

These classes generally require type-level evidence for operations
on their subterms, but don't actually provide it themselves (because
their types are not themselves parameterized, unlike those in
"Data.Parameterized.TraversableFC").

Note that there is still some ambiguity around naming conventions, see
<https://github.com/GaloisInc/parameterized-utils/issues/23 issue 23>.
-}

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE TypeOperators #-}

module Data.Parameterized.ClassesC
  ( TestEqualityC(..)
  , OrdC(..)
  ) where

import Data.Type.Equality ((:~:)(..))
import Data.Kind
import Data.Maybe (isJust)
import Data.Parameterized.Classes (OrderingF, toOrdering)
import Data.Parameterized.Some (Some(..))

class TestEqualityC (t :: (k -> Type) -> Type) where
  testEqualityC :: (forall x y. f x -> f y -> Maybe (x :~: y))
                -> t f
                -> t f
                -> Bool

class TestEqualityC t => OrdC (t :: (k -> Type) -> Type) where
  compareC :: (forall x y. f x -> g y -> OrderingF x y)
           -> t f
           -> t g
           -> Ordering

-- | This instance demonstrates where the above class is useful: namely, in
-- types with existential quantification.
instance TestEqualityC Some where
  testEqualityC :: forall (f :: k -> *).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Some f -> Some f -> Bool
testEqualityC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
subterms (Some f x
someone) (Some f x
something) =
    forall a. Maybe a -> Bool
isJust (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
subterms f x
someone f x
something)

instance OrdC Some where
  compareC :: forall (f :: k -> *) (g :: k -> *).
(forall (x :: k) (y :: k). f x -> g y -> OrderingF x y)
-> Some f -> Some g -> Ordering
compareC forall (x :: k) (y :: k). f x -> g y -> OrderingF x y
subterms (Some f x
someone) (Some g x
something) =
    forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (forall (x :: k) (y :: k). f x -> g y -> OrderingF x y
subterms f x
someone g x
something)