{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeOperators #-}
module Newtype.Union(
  module Data.Type.Coercion.Related,
  IsUnion(..),

  withUnion,
  
  unique, greater, idemp, commutative, associative
) where

import Prelude hiding (id, (.))
import Control.Category
import Data.Type.Coercion.Sub (sub, equiv)
import Data.Type.Coercion.Sub.Internal
import Data.Type.Coercion.Related
import Data.Type.Coercion.Related.Internal
import Data.Type.Coercion ( Coercion(Coercion))

-- | @IsUnion x y z@ witnesses the fact:
--
--   * All @x, y, z@ share the same runtime representation
--   * @z@ is a union type of @x@ and @y@. In other words, the following three holds:
--
--     * @'Sub' x z@
--     * @Sub y z@
--     * For any type @r@ satisfying both of @(Sub x r, Sub y r)@, @Sub z r@.
data IsUnion x y z = IsUnion
  {
    IsUnion x y z -> Sub x z
inl :: !(Sub x z), -- ^ @x@ can be safely coerced to @z@
    IsUnion x y z -> Sub y z
inr :: !(Sub y z), -- ^ @y@ can be safely coerced to @z@
    IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim :: forall r. Sub x r -> Sub y r -> Sub z r
      -- ^ Given both @x@ and @y@ can be safely coerced to @r@, too @z@ can.
  }

-- | For a pair of 'Related' types @x@ and @y@, make some (existentially quantified)
--   type @xy@ where @xy@ is a union type of @x, y@.
withUnion :: Related x y -> (forall xy. IsUnion x y xy -> r) -> r
withUnion :: Related x y -> (forall xy. IsUnion x y xy -> r) -> r
withUnion (Related Coercion x y
Coercion) forall xy. IsUnion x y xy -> r
body =
    IsUnion x y y -> r
forall xy. IsUnion x y xy -> r
body IsUnion :: forall x y z.
Sub x z
-> Sub y z
-> (forall r. Sub x r -> Sub y r -> Sub z r)
-> IsUnion x y z
IsUnion{ inl :: Sub x y
inl = Sub x y
forall k (a :: k) (b :: k). Coercible a b => Sub a b
sub, inr :: Sub y y
inr = Sub y y
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id, elim :: forall r. Sub x r -> Sub y r -> Sub y r
elim = forall r. Sub x r -> Sub y r -> Sub y r
seq }

-- | Two union types @z,z'@ of the same pair of types @x,y@ may be different,
--   but they are equivalent in terms of coercibility.
unique :: IsUnion x y z -> IsUnion x y z' -> Coercion z z'
unique :: IsUnion x y z -> IsUnion x y z' -> Coercion z z'
unique IsUnion x y z
xy IsUnion x y z'
xy' = Sub z z' -> Sub z' z -> Coercion z z'
forall k (a :: k) (b :: k). Sub a b -> Sub b a -> Coercion a b
equiv (IsUnion x y z -> Sub x z' -> Sub y z' -> Sub z z'
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion x y z
xy (IsUnion x y z' -> Sub x z'
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y z'
xy') (IsUnion x y z' -> Sub y z'
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y z'
xy')) (IsUnion x y z' -> Sub x z -> Sub y z -> Sub z' z
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion x y z'
xy' (IsUnion x y z -> Sub x z
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y z
xy) (IsUnion x y z -> Sub y z
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y z
xy))

-- | When @Sub x y@, @y@ itself is a union type of @x, y@.
greater :: Sub x y -> IsUnion x y y
greater :: Sub x y -> IsUnion x y y
greater Sub x y
l = IsUnion :: forall x y z.
Sub x z
-> Sub y z
-> (forall r. Sub x r -> Sub y r -> Sub z r)
-> IsUnion x y z
IsUnion{ inl :: Sub x y
inl = Sub x y
l, inr :: Sub y y
inr = Sub y y
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id, elim :: forall r. Sub x r -> Sub y r -> Sub y r
elim=forall r. Sub x r -> Sub y r -> Sub y r
seq }

-- | Union is idempotent.
--
--   Note: combining @idemp@ and 'unique', @IsUnion x x z -> Coercible x z@ holds.
idemp :: IsUnion x x x
idemp :: IsUnion x x x
idemp = Sub x x -> IsUnion x x x
forall x y. Sub x y -> IsUnion x y y
greater Sub x x
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

-- | Union is commutative.
--
--   Note: combining @commutative@ and 'unique', @IsUnion x y xy -> IsUnion y x yx -> Coercible xy yx@ holds.
commutative :: IsUnion x y z -> IsUnion y x z
commutative :: IsUnion x y z -> IsUnion y x z
commutative IsUnion x y z
xyz = IsUnion :: forall x y z.
Sub x z
-> Sub y z
-> (forall r. Sub x r -> Sub y r -> Sub z r)
-> IsUnion x y z
IsUnion{ inl :: Sub y z
inl = IsUnion x y z -> Sub y z
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y z
xyz, inr :: Sub x z
inr = IsUnion x y z -> Sub x z
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y z
xyz, elim :: forall r. Sub y r -> Sub x r -> Sub z r
elim = (Sub x r -> Sub y r -> Sub z r) -> Sub y r -> Sub x r -> Sub z r
forall a b c. (a -> b -> c) -> b -> a -> c
flip (IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion x y z
xyz) }

-- | Union is associative.
associative :: IsUnion x y xy -> IsUnion xy z xy'z -> IsUnion y z yz -> IsUnion x yz x'yz -> Coercion xy'z x'yz
associative :: IsUnion x y xy
-> IsUnion xy z xy'z
-> IsUnion y z yz
-> IsUnion x yz x'yz
-> Coercion xy'z x'yz
associative IsUnion x y xy
xy IsUnion xy z xy'z
xy'z IsUnion y z yz
yz IsUnion x yz x'yz
x'yz =
    Sub xy'z x'yz -> Sub x'yz xy'z -> Coercion xy'z x'yz
forall k (a :: k) (b :: k). Sub a b -> Sub b a -> Coercion a b
equiv (IsUnion xy z xy'z -> Sub xy x'yz -> Sub z x'yz -> Sub xy'z x'yz
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion xy z xy'z
xy'z (IsUnion x y xy -> Sub x x'yz -> Sub y x'yz -> Sub xy x'yz
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion x y xy
xy (IsUnion x yz x'yz -> Sub x x'yz
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x yz x'yz
x'yz) (IsUnion x yz x'yz -> Sub yz x'yz
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x yz x'yz
x'yz Sub yz x'yz -> Sub y yz -> Sub y x'yz
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsUnion y z yz -> Sub y yz
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion y z yz
yz)) (IsUnion x yz x'yz -> Sub yz x'yz
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x yz x'yz
x'yz Sub yz x'yz -> Sub z yz -> Sub z x'yz
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsUnion y z yz -> Sub z yz
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion y z yz
yz))
          (IsUnion x yz x'yz -> Sub x xy'z -> Sub yz xy'z -> Sub x'yz xy'z
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion x yz x'yz
x'yz (IsUnion xy z xy'z -> Sub xy xy'z
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion xy z xy'z
xy'z Sub xy xy'z -> Sub x xy -> Sub x xy'z
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsUnion x y xy -> Sub x xy
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y xy
xy) (IsUnion y z yz -> Sub y xy'z -> Sub z xy'z -> Sub yz xy'z
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion y z yz
yz (IsUnion xy z xy'z -> Sub xy xy'z
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion xy z xy'z
xy'z Sub xy xy'z -> Sub y xy -> Sub y xy'z
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsUnion x y xy -> Sub y xy
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y xy
xy) (IsUnion xy z xy'z -> Sub z xy'z
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion xy z xy'z
xy'z)))