{-# 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 :: forall {k} (a :: k) (b :: k). Coercible a b => Related a b
related = 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

-- | @'Sub' a b@ implies @Related a b@.
subIsRelated :: Sub (Sub a b) (Related a b)
subIsRelated :: forall {k} (a :: k) (b :: k). Sub (Sub a b) (Related a b)
subIsRelated = 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 :: forall {k} (a :: k) (b :: k). Sub (Coercion a b) (Related a b)
coercionIsRelated = 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 :: forall {k} (a :: k) (b :: k). Related a b -> Related b a
symRelated Related a b
ab = 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 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 :: forall {k} {k} (a :: k) (b :: k) (x :: k) (y :: k).
Sub a b -> (Coercible a b => Related x y) -> Related x y
undirected Sub a b
ab = forall {k} {k} (a :: k) (b :: k) (x :: k) (y :: k).
Related a b -> (Coercible a b => Related x y) -> Related x y
informRelation (forall a b. Sub a b -> a -> b
upcastWith 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 :: 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 Coercion a b
Coercion) Coercible a b => Related x y
body = Coercible a b => Related x y
body