module Bluefin.Internal.Examples where

import Bluefin.Internal
import Data.Proxy (Proxy (Proxy))

-- Fails to compile unless '(e <: es) => e <: (x :& es)' is incoherent
-- (otherwise I guess it "commits to it too soon")
example :: ()
example :: ()
example = (forall (es :: Effects). Eff es ()) -> ()
forall a. (forall (es :: Effects). Eff es a) -> a
runPureEff ((forall (es :: Effects). Eff es ()) -> ())
-> (forall (es :: Effects). Eff es ()) -> ()
forall a b. (a -> b) -> a -> b
$
  ()
-> (forall (e :: Effects). State () e -> Eff ('Union e es) ())
-> Eff es ()
forall s (es :: Effects) a.
s
-> (forall (e :: Effects). Modify s e -> Eff (e :& es) a)
-> Eff es a
evalModify () ((forall (e :: Effects). State () e -> Eff ('Union e es) ())
 -> Eff es ())
-> (forall (e :: Effects). State () e -> Eff ('Union e es) ())
-> Eff es ()
forall a b. (a -> b) -> a -> b
$ \Modify () e
st1 ->
    ()
-> (forall (e :: Effects).
    State () e -> Eff ('Union e (e :& es)) ())
-> Eff (e :& es) ()
forall s (es :: Effects) a.
s
-> (forall (e :: Effects). Modify s e -> Eff (e :& es) a)
-> Eff es a
evalModify () ((forall (e :: Effects). State () e -> Eff ('Union e (e :& es)) ())
 -> Eff (e :& es) ())
-> (forall (e :: Effects).
    State () e -> Eff ('Union e (e :& es)) ())
-> Eff (e :& es) ()
forall a b. (a -> b) -> a -> b
$ \Modify () e
st2 -> do
      Proxy :: Proxy es <- Eff (e :& (e :& es)) (Proxy (e :& (e :& es)))
forall (es :: Effects). Eff es (Proxy es)
effTag
      satisfied @(es <: es)

      Proxy :: Proxy e1 <- handleTag st1
      Proxy :: Proxy e2 <- handleTag st2

      satisfied @(e1 <: e1)
      satisfied @(e2 <: e2)
      satisfied @(e1 <: (e1 :& e2))
      satisfied @(e2 <: (e1 :& e2))

      satisfied @((e1 :& e2) <: (e1 :& e2))