{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeOperators #-}
module Newtype.Intersection(
  module Data.Type.Coercion.Related,
  IsIntersection(..),
  withIntersection,
  
  unique, lesser, idemp, commutative, associative
) where

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

-- | @IsIntersection x y z@ witnesses the fact:
--
--   * All @x, y, z@ share the same runtime representation
--   * @z@ is an intersection type of @x@ and @y@. In other words, the following three holds:
--
--       * @'Sub' z x@
--       * @Sub z y@
--       * For any type @s@ satisfying both of @(Sub s x, Sub s y)@, @Sub s z@.
data IsIntersection x y z = IsIntersection
  {
    IsIntersection x y z -> Sub z x
proj1 :: !(Sub z x),
    IsIntersection x y z -> Sub z y
proj2 :: !(Sub z y),
    IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct :: forall s. Sub s x -> Sub s y -> Sub s z
  }

-- | For a pair of 'Related' types @x@ and @y@, make some (existentially quantified)
--   type @xy@ where @xy@ is an intersection type of @x, y@.
withIntersection :: Related x y -> (forall xy. IsIntersection x y xy -> r) -> r
withIntersection :: Related x y -> (forall xy. IsIntersection x y xy -> r) -> r
withIntersection (Related Coercion x y
Coercion) forall xy. IsIntersection x y xy -> r
body =
    IsIntersection x y y -> r
forall xy. IsIntersection x y xy -> r
body IsIntersection :: forall x y z.
Sub z x
-> Sub z y
-> (forall s. Sub s x -> Sub s y -> Sub s z)
-> IsIntersection x y z
IsIntersection{ proj1 :: Sub y x
proj1 = Sub y x
forall k (a :: k) (b :: k). Coercible a b => Sub a b
sub, proj2 :: Sub y y
proj2 = Sub y y
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id, conjunct :: forall s. Sub s x -> Sub s y -> Sub s y
conjunct = forall s. Sub s x -> Sub s y -> Sub s y
seq }

-- | Two intersection types @z,z'@ of the same pair of types @x,y@ may be different,
--   but they are equivalent in terms of coercibility.
unique :: IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
unique :: IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
unique IsIntersection x y z
xy IsIntersection 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 (IsIntersection x y z' -> Sub z x -> Sub z y -> Sub z z'
forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection x y z'
xy' (IsIntersection x y z -> Sub z x
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y z
xy) (IsIntersection x y z -> Sub z y
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y z
xy)) (IsIntersection x y z -> Sub z' x -> Sub z' y -> Sub z' z
forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection x y z
xy (IsIntersection x y z' -> Sub z' x
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y z'
xy') (IsIntersection x y z' -> Sub z' y
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y z'
xy'))

-- | When @Sub x y@, @x@ itself is an intersection type of @x, y@.
lesser :: Sub x y -> IsIntersection x y x
lesser :: Sub x y -> IsIntersection x y x
lesser Sub x y
l = IsIntersection :: forall x y z.
Sub z x
-> Sub z y
-> (forall s. Sub s x -> Sub s y -> Sub s z)
-> IsIntersection x y z
IsIntersection{ proj1 :: Sub x x
proj1=Sub x x
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id, proj2 :: Sub x y
proj2=Sub x y
l, conjunct :: forall s. Sub s x -> Sub s y -> Sub s x
conjunct= \Sub s x
sx !Sub s y
_ -> Sub s x
sx }


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

-- | Intersection is commutative.
--
--   Note: combining @commutative@ and 'unique', @IsIntersection x x z -> Coercible x z@ holds.
commutative :: IsIntersection x y z -> IsIntersection y x z
commutative :: IsIntersection x y z -> IsIntersection y x z
commutative IsIntersection x y z
xyz = IsIntersection :: forall x y z.
Sub z x
-> Sub z y
-> (forall s. Sub s x -> Sub s y -> Sub s z)
-> IsIntersection x y z
IsIntersection{ proj1 :: Sub z y
proj1 = IsIntersection x y z -> Sub z y
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y z
xyz, proj2 :: Sub z x
proj2 = IsIntersection x y z -> Sub z x
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y z
xyz, conjunct :: forall s. Sub s y -> Sub s x -> Sub s z
conjunct = (Sub s x -> Sub s y -> Sub s z) -> Sub s y -> Sub s x -> Sub s z
forall a b c. (a -> b -> c) -> b -> a -> c
flip (IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection x y z
xyz)}

-- | Intersection is associative.
associative :: IsIntersection x y xy -> IsIntersection xy z xy'z -> IsIntersection y z yz -> IsIntersection x yz x'yz -> Coercion xy'z x'yz
associative :: IsIntersection x y xy
-> IsIntersection xy z xy'z
-> IsIntersection y z yz
-> IsIntersection x yz x'yz
-> Coercion xy'z x'yz
associative IsIntersection x y xy
xy IsIntersection xy z xy'z
xy'z IsIntersection y z yz
yz IsIntersection 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 (IsIntersection x yz x'yz
-> Sub xy'z x -> Sub xy'z yz -> Sub xy'z x'yz
forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection x yz x'yz
x'yz (IsIntersection x y xy -> Sub xy x
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y xy
xy Sub xy x -> Sub xy'z xy -> Sub xy'z x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsIntersection xy z xy'z -> Sub xy'z xy
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection xy z xy'z
xy'z) (IsIntersection y z yz -> Sub xy'z y -> Sub xy'z z -> Sub xy'z yz
forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection y z yz
yz (IsIntersection x y xy -> Sub xy y
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y xy
xy Sub xy y -> Sub xy'z xy -> Sub xy'z y
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsIntersection xy z xy'z -> Sub xy'z xy
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection xy z xy'z
xy'z) (IsIntersection xy z xy'z -> Sub xy'z z
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection xy z xy'z
xy'z)))
          (IsIntersection xy z xy'z
-> Sub x'yz xy -> Sub x'yz z -> Sub x'yz xy'z
forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection xy z xy'z
xy'z (IsIntersection x y xy -> Sub x'yz x -> Sub x'yz y -> Sub x'yz xy
forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection x y xy
xy (IsIntersection x yz x'yz -> Sub x'yz x
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x yz x'yz
x'yz) (IsIntersection y z yz -> Sub yz y
forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection y z yz
yz Sub yz y -> Sub x'yz yz -> Sub x'yz y
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsIntersection x yz x'yz -> Sub x'yz yz
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x yz x'yz
x'yz)) (IsIntersection y z yz -> Sub yz z
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection y z yz
yz Sub yz z -> Sub x'yz yz -> Sub x'yz z
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsIntersection x yz x'yz -> Sub x'yz yz
forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x yz x'yz
x'yz))