{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
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), TestCoercion(..) )

-- | @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
  {
    forall x y z. IsIntersection x y z -> Sub z x
proj1 :: !(Sub z x),
    forall x y z. IsIntersection x y z -> Sub z y
proj2 :: !(Sub z y),
    forall x y z.
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
  }

instance Eq (IsIntersection x y z) where
  IsIntersection x y z
_ == :: IsIntersection x y z -> IsIntersection x y z -> Bool
== IsIntersection x y z
_ = Bool
True
instance Ord (IsIntersection x y z) where
  compare :: IsIntersection x y z -> IsIntersection x y z -> Ordering
compare IsIntersection x y z
_ IsIntersection x y z
_ = Ordering
EQ

instance TestCoercion (IsIntersection x y) where
  testCoercion :: forall a b.
IsIntersection x y a
-> IsIntersection x y b -> Maybe (Coercion a b)
testCoercion IsIntersection x y a
u1 IsIntersection x y b
u2 = forall a. a -> Maybe a
Just (forall x y z z'.
IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
unique IsIntersection x y a
u1 IsIntersection x y b
u2)

-- | 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 :: forall x y r.
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 =
    forall xy. IsIntersection x y xy -> r
body IsIntersection{ proj1 :: Sub y x
proj1 = forall {k} (a :: k) (b :: k). Coercible a b => Sub a b
sub, proj2 :: Sub y y
proj2 = 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 = seq :: forall a b. a -> b -> b
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 :: forall x y z z'.
IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
unique IsIntersection x y z
xy IsIntersection x y z'
xy' = forall {k} (a :: k) (b :: k). Sub a b -> Sub b a -> Coercion a b
equiv (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' (forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y z
xy) (forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y z
xy)) (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 (forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y z'
xy') (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 :: forall x y. Sub x y -> IsIntersection x y x
lesser Sub x y
l = IsIntersection{ proj1 :: Sub x x
proj1=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 -> Coercion x z@ holds.
idemp :: IsIntersection x x x
idemp :: forall x. IsIntersection x x x
idemp = forall x y. Sub x y -> IsIntersection x y x
lesser forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

-- | Intersection is commutative.
--
--   Note: combining @commutative@ and 'unique', @IsIntersection x y xy -> IsIntersection y x yx -> Coercion xy yx@ holds.
commutative :: IsIntersection x y z -> IsIntersection y x z
commutative :: forall x y z. IsIntersection x y z -> IsIntersection y x z
commutative IsIntersection x y z
xyz = IsIntersection{ proj1 :: Sub z y
proj1 = forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y z
xyz, proj2 :: Sub z x
proj2 = 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip (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.
--
--   Note: combining @associative@ and 'unique', the following holds.
--   
--   >    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 xyz -> IsIntersection y z yz -> IsIntersection x yz xyz
associative :: forall x y xy z xyz yz.
IsIntersection x y xy
-> IsIntersection xy z xyz
-> IsIntersection y z yz
-> IsIntersection x yz xyz
associative IsIntersection x y xy
xy IsIntersection xy z xyz
xy'z IsIntersection y z yz
yz =
    IsIntersection {
       proj1 :: Sub xyz x
proj1 = forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection x y xy
xy forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection xy z xyz
xy'z
     , proj2 :: Sub xyz yz
proj2 = 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 (forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection x y xy
xy forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection xy z xyz
xy'z) (forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection xy z xyz
xy'z)
     , conjunct :: forall s. Sub s x -> Sub s yz -> Sub s xyz
conjunct = \Sub s x
s_x Sub s yz
s_yz -> forall x y z.
IsIntersection x y z -> forall s. Sub s x -> Sub s y -> Sub s z
conjunct IsIntersection xy z xyz
xy'z (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 Sub s x
s_x (forall x y z. IsIntersection x y z -> Sub z x
proj1 IsIntersection y z yz
yz forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Sub s yz
s_yz)) (forall x y z. IsIntersection x y z -> Sub z y
proj2 IsIntersection y z yz
yz forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Sub s yz
s_yz)
    }