{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{- |
  'Related' type to witness that two types @a@ and @b@ shares the same runtime representation,
  but nothing about whether @a@ can be safely coerced to or from @b@.

  Unlike 'Coercion' or 'Sub', having a value of @Related a b@ does not allow to
  touch values of @a@ or @b@.

  This module is used alonside "Newtype.Union" and "Newtype.Intersection"
  to define union and intersection types of two 'Related' types.
-}
module Data.Type.Coercion.Related(
    Related(),
    related,
    subIsRelated, coercionIsRelated,
    symRelated, undirected, informRelation
) where

import Data.Coerce
import Data.Type.Coercion
import Data.Type.Coercion.Sub
import Data.Type.Coercion.Sub.Internal
import Data.Type.Coercion.Related.Internal

-- | @'Coercible' a b@ implies @Related a b@.
related :: Coercible a b => Related a b
related :: Related a b
related = Coercion a b -> Related a b
forall k (a :: k) (b :: k). Coercion a b -> Related a b
Related Coercion a b
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

-- | @'Sub' a b@ implies @Related a b@.
subIsRelated :: Sub (Sub a b) (Related a b)
subIsRelated :: Sub (Sub a b) (Related a b)
subIsRelated = Sub (Sub a b) (Related a b)
forall k (a :: k) (b :: k). Coercible a b => Sub a b
sub

-- | @'Coercion' a b@ implies @'Sub' a b@, which implies @Related a b@.
coercionIsRelated :: Sub (Coercion a b) (Related a b)
coercionIsRelated :: Sub (Coercion a b) (Related a b)
coercionIsRelated = Sub (Coercion a b) (Related a b)
forall k (a :: k) (b :: k). Coercible a b => Sub a b
sub

-- | @Related@ is a symmetric relation.
symRelated :: Related a b -> Related b a
symRelated :: Related a b -> Related b a
symRelated Related a b
ab = Related a b -> (Coercible a b => Related b a) -> Related b a
forall k k (a :: k) (b :: k) (x :: k) (y :: k).
Related a b -> (Coercible a b => Related x y) -> Related x y
informRelation Related a b
ab Coercible a b => Related b a
forall k (a :: k) (b :: k). Coercible a b => Related a b
related

-- | A direct consequence of 'informRelation' and 'subIsRelated'.
undirected :: Sub a b -> (Coercible a b => Related x y) -> Related x y
undirected :: Sub a b -> (Coercible a b => Related x y) -> Related x y
undirected Sub a b
ab = Related a b -> (Coercible a b => Related x y) -> Related x y
forall k k (a :: k) (b :: k) (x :: k) (y :: k).
Related a b -> (Coercible a b => Related x y) -> Related x y
informRelation (Sub (Sub a b) (Related a b) -> Sub a b -> Related a b
forall a b. Sub a b -> a -> b
upcastWith Sub (Sub a b) (Related a b)
forall k (a :: k) (b :: k). Sub (Sub a b) (Related a b)
subIsRelated Sub a b
ab)

-- | Given @Related a b@, you can assume @Coercible a b@ for the purpose of proving
--   another @Related@ relation.
informRelation :: Related a b -> (Coercible a b => Related x y) -> Related x y
informRelation :: Related a b -> (Coercible a b => Related x y) -> Related x y
informRelation (Related Coercion a b
Coercion) Coercible a b => Related x y
body = Related x y
Coercible a b => Related x y
body