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}. Modify () e -> Eff (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}. Modify () e -> Eff (e :& es) ())
 -> Eff es ())
-> (forall {e :: Effects}. Modify () e -> Eff (e :& es) ())
-> Eff es ()
forall a b. (a -> b) -> a -> b
$ \Modify () e
st1 ->
    ()
-> (forall {e :: Effects}. Modify () e -> Eff (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}. Modify () e -> Eff (e :& (e :& es)) ())
 -> Eff (e :& es) ())
-> (forall {e :: Effects}. Modify () e -> Eff (e :& (e :& es)) ())
-> Eff (e :& es) ()
forall a b. (a -> b) -> a -> b
$ \Modify () e
st2 -> do
      Proxy (e :& (e :& es))
Proxy :: Proxy es <- Eff (e :& (e :& es)) (Proxy (e :& (e :& es)))
forall (es :: Effects). Eff es (Proxy es)
effTag
      forall (c :: Constraint) (m :: * -> *). (Monad m, c) => m ()
satisfied @(es <: es)

      Proxy e
Proxy :: Proxy e1 <- Modify () e -> Eff (e :& (e :& es)) (Proxy e)
forall {k} (h :: k -> *) (e :: k) (es :: Effects).
h e -> Eff es (Proxy e)
handleTag Modify () e
st1
      Proxy e
Proxy :: Proxy e2 <- Modify () e -> Eff (e :& (e :& es)) (Proxy e)
forall {k} (h :: k -> *) (e :: k) (es :: Effects).
h e -> Eff es (Proxy e)
handleTag Modify () e
st2

      forall (c :: Constraint) (m :: * -> *). (Monad m, c) => m ()
satisfied @(e1 <: e1)
      forall (c :: Constraint) (m :: * -> *). (Monad m, c) => m ()
satisfied @(e2 <: e2)
      forall (c :: Constraint) (m :: * -> *). (Monad m, c) => m ()
satisfied @(e1 <: (e1 :& e2))
      forall (c :: Constraint) (m :: * -> *). (Monad m, c) => m ()
satisfied @(e2 <: (e1 :& e2))

      forall (c :: Constraint) (m :: * -> *). (Monad m, c) => m ()
satisfied @((e1 :& e2) <: (e1 :& e2))