{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE StandaloneDeriving #-}
{- |

This module exposes internals of "Data.Type.Coercion.Related".

Using this module allows to violate the premises 'Related' type provides.
It is advisable not to import this module if there is another way,
and to limit the amount of code accesible to this module.

-}
module Data.Type.Coercion.Related.Internal where

import           Control.Category
import           Prelude                    hiding (id, (.))

import           Data.Coerce
import           Data.Type.Coercion

-- | @Related a b@ witnesses @a@ and @b@ shares the same runtime representation,
--   but nothing about whether @a@ can be safely coerced to or from @b@.
-- 
-- You can make 'Related' witnesses by using combinators in this module, or the methods of
-- the @'Category' Related@ instance: 'id' and @('.')@.
newtype Related (a :: k) (b :: k) = Related { forall k (a :: k) (b :: k). Related a b -> Coercion a b
getRelated :: Coercion a b }
  deriving stock (Related a b -> Related a b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k) (b :: k). Related a b -> Related a b -> Bool
/= :: Related a b -> Related a b -> Bool
$c/= :: forall k (a :: k) (b :: k). Related a b -> Related a b -> Bool
== :: Related a b -> Related a b -> Bool
$c== :: forall k (a :: k) (b :: k). Related a b -> Related a b -> Bool
Eq, Related a b -> Related a b -> Bool
Related a b -> Related a b -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (a :: k) (b :: k). Eq (Related a b)
forall k (a :: k) (b :: k). Related a b -> Related a b -> Bool
forall k (a :: k) (b :: k). Related a b -> Related a b -> Ordering
forall k (a :: k) (b :: k).
Related a b -> Related a b -> Related a b
min :: Related a b -> Related a b -> Related a b
$cmin :: forall k (a :: k) (b :: k).
Related a b -> Related a b -> Related a b
max :: Related a b -> Related a b -> Related a b
$cmax :: forall k (a :: k) (b :: k).
Related a b -> Related a b -> Related a b
>= :: Related a b -> Related a b -> Bool
$c>= :: forall k (a :: k) (b :: k). Related a b -> Related a b -> Bool
> :: Related a b -> Related a b -> Bool
$c> :: forall k (a :: k) (b :: k). Related a b -> Related a b -> Bool
<= :: Related a b -> Related a b -> Bool
$c<= :: forall k (a :: k) (b :: k). Related a b -> Related a b -> Bool
< :: Related a b -> Related a b -> Bool
$c< :: forall k (a :: k) (b :: k). Related a b -> Related a b -> Bool
compare :: Related a b -> Related a b -> Ordering
$ccompare :: forall k (a :: k) (b :: k). Related a b -> Related a b -> Ordering
Ord, Int -> Related a b -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k) (b :: k). Int -> Related a b -> ShowS
forall k (a :: k) (b :: k). [Related a b] -> ShowS
forall k (a :: k) (b :: k). Related a b -> String
showList :: [Related a b] -> ShowS
$cshowList :: forall k (a :: k) (b :: k). [Related a b] -> ShowS
show :: Related a b -> String
$cshow :: forall k (a :: k) (b :: k). Related a b -> String
showsPrec :: Int -> Related a b -> ShowS
$cshowsPrec :: forall k (a :: k) (b :: k). Int -> Related a b -> ShowS
Show)
-- It is intentional to omit the 'TestCoercion' instance, existing for @Coercion@.
-- Knowing @Related a b@ and @Related a c@ should not conclude
-- @Coercible b c@.

deriving stock instance Coercible a b => Read (Related a b)
deriving newtype instance Coercible a b => Enum (Related a b)
deriving newtype instance Coercible a b => Bounded (Related a b)

instance Category Related where
  id :: Related a a
  id :: forall k (a :: k). Related a a
id = forall k (a :: k) (b :: k). Coercion a b -> Related a b
Related forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

  (.) :: Related b c -> Related a b -> Related a c
  Related Coercion b c
Coercion . :: forall k (b :: k) (c :: k) (a :: k).
Related b c -> Related a b -> Related a c
. Related Coercion a b
Coercion = forall k (a :: k) (b :: k). Coercion a b -> Related a b
Related forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion