T16473.dump-simpl

==================== Tidy Core ====================
2019-03-26 16:42:16.733069541 UTC

Result size of Tidy Core
  = {terms: 572, types: 1,423, coercions: 358, joins: 0/6}

-- RHS size: {terms: 5, types: 17, coercions: 9, joins: 0/0}
$WUnion :: forall (e :: * -> *) a. e a -> Union '[e] a
$WUnion
  = \ (@ (e :: * -> *)) (@ a) (dt :: e a) ->
      Union @ '[e] @ a @ e @~ <Co:9> dt

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
main2 :: Int
main2 = I# 0#

-- RHS size: {terms: 17, types: 78, coercions: 17, joins: 0/0}
main3
  :: forall x.
     Union '[State (Sum Int)] x -> Sum Int -> Identity (x, Sum Int)
main3
  = \ (@ x) (u :: Union '[State (Sum Int)] x) (eta :: Sum Int) ->
      case u of { Union @ e co a ->
      case a `cast` <Co:5> of {
        Get k -> (k eta, eta) `cast` <Co:6>;
        Put s k -> (k, s) `cast` <Co:6>
      }
      }

-- RHS size: {terms: 2, types: 6, coercions: 0, joins: 0/0}
lvl :: State (Sum Int) (Sum Int)
lvl = Get @ (Sum Int) @ (Sum Int) (id @ (Sum Int))

-- RHS size: {terms: 2, types: 16, coercions: 11, joins: 0/0}
lvl1 :: Union '[State (Sum Int)] (Sum Int)
lvl1
  = Union
      @ '[State (Sum Int)] @ (Sum Int) @ (State (Sum Int)) @~ <Co:11> lvl

Rec {
-- RHS size: {terms: 40, types: 80, coercions: 65, joins: 0/2}
main_$sgo
  :: Int#
     -> (forall x.
         Union '[State (Sum Int)] x -> StateT (Sum Int) Identity x)
     -> StateT (Sum Int) Identity ()
main_$sgo
  = \ (x :: Int#)
      (eta
         :: forall x1.
            Union '[State (Sum Int)] x1 -> StateT (Sum Int) Identity x1) ->
      let {
        m1 :: StateT (Sum Int) Identity (Sum Int)
        m1 = eta @ (Sum Int) lvl1 } in
      let {
        ds1 :: StateT (Sum Int) Identity ()
        ds1
          = case x of wild {
              __DEFAULT -> main_$sgo (+# wild 1#) eta;
              100# -> (\ (s1 :: Sum Int) -> ((), s1)) `cast` <Co:16>
            } } in
      (\ (s1 :: Sum Int) ->
         case ((m1 `cast` <Co:6>) s1) `cast` <Co:6> of { (a1, s') ->
         case a1 `cast` <Co:2> of { I# ipv ->
         case (((eta
                   @ ()
                   (Union
                      @ '[State (Sum Int)]
                      @ ()
                      @ (State (Sum Int))
                      @~ <Co:11>
                      (Put @ (Sum Int) @ () ((I# (+# ipv x)) `cast` <Co:3>) ())))
                `cast` <Co:5>)
                 s')
              `cast` <Co:5>
         of
         { (a2, s'1) ->
         (ds1 `cast` <Co:5>) s'1
         }
         }
         })
      `cast` <Co:6>
end Rec }

-- RHS size: {terms: 18, types: 20, coercions: 37, joins: 0/0}
main1 :: String
main1
  = case (((main_$sgo 0# (main3 `cast` <Co:22>)) `cast` <Co:5>)
            (main2 `cast` <Co:3>))
         `cast` <Co:5>
    of
    { (a1, b1) ->
    case b1 `cast` <Co:2> of { I# ww3 ->
    case $wshowSignedInt 0# ww3 ([] @ Char) of { (# ww5, ww6 #) ->
    : @ Char ww5 ww6
    }
    }
    }

-- RHS size: {terms: 4, types: 0, coercions: 0, joins: 0/0}
main :: IO ()
main = hPutStr' stdout main1 True

-- RHS size: {terms: 2, types: 1, coercions: 0, joins: 0/0}
main4 :: State# RealWorld -> (# State# RealWorld, () #)
main4 = runMainIO1 @ () main

-- RHS size: {terms: 1, types: 0, coercions: 3, joins: 0/0}
main :: IO ()
main = main4 `cast` <Co:3>

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tc'Get3 :: Addr#
$tc'Get3 = "'Get"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tc'Get2 :: TrName
$tc'Get2 = TrNameS $tc'Get3

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tc'Put3 :: Addr#
$tc'Put3 = "'Put"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tc'Put2 :: TrName
$tc'Put2 = TrNameS $tc'Put3

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tcState2 :: Addr#
$tcState2 = "State"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tcState1 :: TrName
$tcState1 = TrNameS $tcState2

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tcSemantic3 :: Addr#
$tcSemantic3 = "Semantic"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tcSemantic2 :: TrName
$tcSemantic2 = TrNameS $tcSemantic3

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tc'Union3 :: Addr#
$tc'Union3 = "'Union"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tc'Union2 :: TrName
$tc'Union2 = TrNameS $tc'Union3

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$tcUnion2 :: Addr#
$tcUnion2 = "Union"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$tcUnion1 :: TrName
$tcUnion1 = TrNameS $tcUnion2

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$krep :: KindRep
$krep = KindRepVar 0#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$krep1 :: KindRep
$krep1 = KindRepVar 1#

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep2 :: KindRep
$krep2 = KindRepFun $krep $krep1

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep3 :: KindRep
$krep3 = KindRepApp $krep $krep1

-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
$krep4 :: [KindRep]
$krep4 = : @ KindRep $krep1 ([] @ KindRep)

-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
$krep5 :: [KindRep]
$krep5 = : @ KindRep $krep $krep4

-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
$krep6 :: [KindRep]
$krep6 = : @ KindRep krep$*Arr* ([] @ KindRep)

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep7 :: KindRep
$krep7 = KindRepTyConApp $tc[] $krep6

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$tcSemantic1 :: KindRep
$tcSemantic1 = KindRepFun $krep7 krep$*Arr*

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep8 :: KindRep
$krep8 = KindRepTyConApp $tc'[] $krep6

-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
$krep9 :: [KindRep]
$krep9 = : @ KindRep $krep8 ([] @ KindRep)

-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
$krep10 :: [KindRep]
$krep10 = : @ KindRep $krep $krep9

-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
$krep11 :: [KindRep]
$krep11 = : @ KindRep krep$*Arr* $krep10

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep12 :: KindRep
$krep12 = KindRepTyConApp $tc': $krep11

-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
$krep13 :: [KindRep]
$krep13 = : @ KindRep $krep12 $krep4

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$trModule2 :: Addr#
$trModule2 = "Main"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$trModule1 :: TrName
$trModule1 = TrNameS $trModule2

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$trModule4 :: Addr#
$trModule4 = "main"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$trModule3 :: TrName
$trModule3 = TrNameS $trModule4

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$trModule :: Module
$trModule = Module $trModule3 $trModule1

-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tcUnion :: TyCon
$tcUnion
  = TyCon
      229884759504400770##
      13528229582907927977##
      $trModule
      $tcUnion1
      0#
      $tcSemantic1

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep14 :: KindRep
$krep14 = KindRepTyConApp $tcUnion $krep13

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$tc'Union1 :: KindRep
$tc'Union1 = KindRepFun $krep3 $krep14

-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tc'Union :: TyCon
$tc'Union
  = TyCon
      6632976870638181383##
      15290975553766063960##
      $trModule
      $tc'Union2
      2#
      $tc'Union1

-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tcSemantic :: TyCon
$tcSemantic
  = TyCon
      9508779775375363839##
      14545629556631013737##
      $trModule
      $tcSemantic2
      0#
      $tcSemantic1

-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tcState :: TyCon
$tcState
  = TyCon
      11500382755588220783##
      3741540518684525139##
      $trModule
      $tcState1
      0#
      krep$*->*->*

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep15 :: KindRep
$krep15 = KindRepTyConApp $tcState $krep5

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep16 :: KindRep
$krep16 = KindRepFun $krep1 $krep15

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$tc'Put1 :: KindRep
$tc'Put1 = KindRepFun $krep $krep16

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$tc'Get1 :: KindRep
$tc'Get1 = KindRepFun $krep2 $krep15

-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tc'Put :: TyCon
$tc'Put
  = TyCon
      15201137817969246407##
      1251973250185875189##
      $trModule
      $tc'Put2
      2#
      $tc'Put1

-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
$tc'Get :: TyCon
$tc'Get
  = TyCon
      4894226031785183458##
      8801726891554456039##
      $trModule
      $tc'Get2
      2#
      $tc'Get1

-- RHS size: {terms: 27, types: 61, coercions: 6, joins: 0/2}
$w$c>>
  :: forall (f :: [* -> *]) a b.
     Semantic f a
     -> Semantic f b
     -> forall (m :: * -> *).
        Applicative m =>
        (forall a1 b1. m a1 -> (a1 -> m b1) -> m b1)
        -> (forall a1 b1. m a1 -> m b1 -> m b1)
        -> (forall a1. a1 -> m a1)
        -> (forall x. Union f x -> m x)
        -> m b
$w$c>>
  = \ (@ (f :: [* -> *]))
      (@ a)
      (@ b)
      (w :: Semantic f a)
      (w1 :: Semantic f b)
      (@ (m :: * -> *))
      (ww :: Applicative m)
      (ww1 :: forall a1 b1. m a1 -> (a1 -> m b1) -> m b1)
      (ww2 :: forall a1 b1. m a1 -> m b1 -> m b1)
      (ww3 :: forall a1. a1 -> m a1)
      (w2 :: forall x. Union f x -> m x) ->
      let {
        $dMonad :: Monad m
        $dMonad = C:Monad @ m ww ww1 ww2 ww3 } in
      let {
        lvl2 :: m b
        lvl2 = (w1 `cast` <Co:3>) @ m $dMonad w2 } in
      ww1 @ a @ b ((w `cast` <Co:3>) @ m $dMonad w2) (\ _ -> lvl2)

-- RHS size: {terms: 19, types: 59, coercions: 0, joins: 0/0}
$c>>
  :: forall (f :: [* -> *]) a b.
     Semantic f a
     -> Semantic f b
     -> forall (m :: * -> *).
        Monad m =>
        (forall x. Union f x -> m x) -> m b
$c>>
  = \ (@ (f :: [* -> *]))
      (@ a)
      (@ b)
      (w :: Semantic f a)
      (w1 :: Semantic f b)
      (@ (m :: * -> *))
      (w2 :: Monad m)
      (w3 :: forall x. Union f x -> m x) ->
      case w2 of { C:Monad ww1 ww2 ww3 ww4 ->
      $w$c>> @ f @ a @ b w w1 @ m ww1 ww2 ww3 ww4 w3
      }

-- RHS size: {terms: 1, types: 0, coercions: 22, joins: 0/0}
$fMonadSemantic_$c>>
  :: forall (f :: [* -> *]) a b.
     Semantic f a -> Semantic f b -> Semantic f b
$fMonadSemantic_$c>> = $c>> `cast` <Co:22>

-- RHS size: {terms: 26, types: 60, coercions: 6, joins: 0/1}
$w$c>>=
  :: forall (f :: [* -> *]) a b.
     Semantic f a
     -> (a -> Semantic f b)
     -> forall (m :: * -> *).
        Applicative m =>
        (forall a1 b1. m a1 -> (a1 -> m b1) -> m b1)
        -> (forall a1 b1. m a1 -> m b1 -> m b1)
        -> (forall a1. a1 -> m a1)
        -> (forall x. Union f x -> m x)
        -> m b
$w$c>>=
  = \ (@ (f :: [* -> *]))
      (@ a)
      (@ b)
      (w :: Semantic f a)
      (w1 :: a -> Semantic f b)
      (@ (m :: * -> *))
      (ww :: Applicative m)
      (ww1 :: forall a1 b1. m a1 -> (a1 -> m b1) -> m b1)
      (ww2 :: forall a1 b1. m a1 -> m b1 -> m b1)
      (ww3 :: forall a1. a1 -> m a1)
      (w2 :: forall x. Union f x -> m x) ->
      let {
        $dMonad :: Monad m
        $dMonad = C:Monad @ m ww ww1 ww2 ww3 } in
      ww1
        @ a
        @ b
        ((w `cast` <Co:3>) @ m $dMonad w2)
        (\ (z1 :: a) -> ((w1 z1) `cast` <Co:3>) @ m $dMonad w2)

-- RHS size: {terms: 19, types: 60, coercions: 0, joins: 0/0}
$c>>=
  :: forall (f :: [* -> *]) a b.
     Semantic f a
     -> (a -> Semantic f b)
     -> forall (m :: * -> *).
        Monad m =>
        (forall x. Union f x -> m x) -> m b
$c>>=
  = \ (@ (f :: [* -> *]))
      (@ a)
      (@ b)
      (w :: Semantic f a)
      (w1 :: a -> Semantic f b)
      (@ (m :: * -> *))
      (w2 :: Monad m)
      (w3 :: forall x. Union f x -> m x) ->
      case w2 of { C:Monad ww1 ww2 ww3 ww4 ->
      $w$c>>= @ f @ a @ b w w1 @ m ww1 ww2 ww3 ww4 w3
      }

-- RHS size: {terms: 1, types: 0, coercions: 23, joins: 0/0}
$fMonadSemantic_$c>>=
  :: forall (f :: [* -> *]) a b.
     Semantic f a -> (a -> Semantic f b) -> Semantic f b
$fMonadSemantic_$c>>= = $c>>= `cast` <Co:23>

-- RHS size: {terms: 9, types: 21, coercions: 3, joins: 0/0}
runSemantic
  :: forall (r :: [* -> *]) a.
     Semantic r a
     -> forall (m :: * -> *).
        Monad m =>
        (forall x. Union r x -> m x) -> m a
runSemantic
  = \ (@ (r :: [* -> *]))
      (@ a)
      (dk :: Semantic r a)
      (@ (m :: * -> *))
      ($dMonad :: Monad m)
      (ds :: forall x. Union r x -> m x) ->
      (dk `cast` <Co:3>) @ m $dMonad ds

-- RHS size: {terms: 18, types: 23, coercions: 0, joins: 0/0}
$fFunctorState_$cfmap
  :: forall s a b. (a -> b) -> State s a -> State s b
$fFunctorState_$cfmap
  = \ (@ s) (@ a) (@ b) (f :: a -> b) (ds :: State s a) ->
      case ds of {
        Get a1 -> Get @ s @ b (\ (b3 :: s) -> f (a1 b3));
        Put a1 a2 -> Put @ s @ b a1 (f a2)
      }

-- RHS size: {terms: 15, types: 22, coercions: 0, joins: 0/0}
$fFunctorState_$c<$ :: forall s a b. a -> State s b -> State s a
$fFunctorState_$c<$
  = \ (@ s) (@ a) (@ b) (z1 :: a) (ds :: State s b) ->
      case ds of {
        Get a1 -> Get @ s @ a (\ _ -> z1);
        Put a1 a2 -> Put @ s @ a a1 z1
      }

-- RHS size: {terms: 4, types: 6, coercions: 0, joins: 0/0}
$fFunctorState :: forall s. Functor (State s)
$fFunctorState
  = \ (@ s) ->
      C:Functor
        @ (State s) ($fFunctorState_$cfmap @ s) ($fFunctorState_$c<$ @ s)

-- RHS size: {terms: 24, types: 42, coercions: 6, joins: 0/0}
$fApplicativeSemantic2
  :: forall (f :: [* -> *]) a b c.
     (a -> b -> c)
     -> Semantic f a
     -> Semantic f b
     -> forall (m :: * -> *).
        Monad m =>
        (forall x. Union f x -> m x) -> m c
$fApplicativeSemantic2
  = \ (@ (f :: [* -> *]))
      (@ a)
      (@ b)
      (@ c)
      (f1 :: a -> b -> c)
      (x :: Semantic f a)
      (eta :: Semantic f b)
      (@ (m :: * -> *))
      (eta1 :: Monad m)
      (eta2 :: forall x1. Union f x1 -> m x1) ->
      <*>
        @ m
        ($p1Monad @ m eta1)
        @ b
        @ c
        (fmap
           @ m
           ($p1Applicative @ m ($p1Monad @ m eta1))
           @ a
           @ (b -> c)
           f1
           ((x `cast` <Co:3>) @ m eta1 eta2))
        ((eta `cast` <Co:3>) @ m eta1 eta2)

-- RHS size: {terms: 5, types: 13, coercions: 0, joins: 0/0}
$fApplicativeSemantic1
  :: forall b a (f :: [* -> *]).
     Semantic f a
     -> Semantic f b
     -> forall (m :: * -> *).
        Monad m =>
        (forall x. Union f x -> m x) -> m a
$fApplicativeSemantic1
  = \ (@ b) (@ a) (@ (f :: [* -> *])) ->
      $fApplicativeSemantic2 @ f @ a @ b @ a (const @ a @ b)

-- RHS size: {terms: 12, types: 23, coercions: 0, joins: 0/1}
$cpure
  :: forall (f :: [* -> *]) a.
     a
     -> forall (m :: * -> *).
        Monad m =>
        (forall x. Union f x -> m x) -> m a
$cpure
  = \ (@ (f :: [* -> *]))
      (@ a)
      (a1 :: a)
      (@ (m :: * -> *))
      ($dMonad :: Monad m) ->
      let {
        ds :: m a
        ds = pure @ m ($p1Monad @ m $dMonad) @ a a1 } in
      \ _ -> ds

-- RHS size: {terms: 1, types: 0, coercions: 13, joins: 0/0}
$fApplicativeSemantic_$cpure
  :: forall (f :: [* -> *]) a. a -> Semantic f a
$fApplicativeSemantic_$cpure = $cpure `cast` <Co:13>

-- RHS size: {terms: 17, types: 32, coercions: 7, joins: 0/0}
$c<*>
  :: forall (f :: [* -> *]) a b.
     Semantic f (a -> b)
     -> Semantic f a
     -> forall (m :: * -> *).
        Monad m =>
        (forall x. Union f x -> m x) -> m b
$c<*>
  = \ (@ (f :: [* -> *]))
      (@ a)
      (@ b)
      (ds :: Semantic f (a -> b))
      (ds1 :: Semantic f a)
      (@ (m :: * -> *))
      ($dMonad :: Monad m)
      (eta :: forall x. Union f x -> m x) ->
      <*>
        @ m
        ($p1Monad @ m $dMonad)
        @ a
        @ b
        ((ds `cast` <Co:4>) @ m $dMonad eta)
        ((ds1 `cast` <Co:3>) @ m $dMonad eta)

-- RHS size: {terms: 1, types: 0, coercions: 23, joins: 0/0}
$fApplicativeSemantic_$c<*>
  :: forall (f :: [* -> *]) a b.
     Semantic f (a -> b) -> Semantic f a -> Semantic f b
$fApplicativeSemantic_$c<*> = $c<*> `cast` <Co:23>

-- RHS size: {terms: 17, types: 30, coercions: 3, joins: 0/0}
$fApplicativeSemantic4
  :: forall (f :: [* -> *]) a b.
     a
     -> Semantic f b
     -> forall (m :: * -> *).
        Monad m =>
        (forall x. Union f x -> m x) -> m a
$fApplicativeSemantic4
  = \ (@ (f :: [* -> *]))
      (@ a)
      (@ b)
      (x :: a)
      (eta :: Semantic f b)
      (@ (m :: * -> *))
      (eta1 :: Monad m)
      (eta2 :: forall x1. Union f x1 -> m x1) ->
      fmap
        @ m
        ($p1Applicative @ m ($p1Monad @ m eta1))
        @ b
        @ a
        (\ _ -> x)
        ((eta `cast` <Co:3>) @ m eta1 eta2)

-- RHS size: {terms: 16, types: 30, coercions: 3, joins: 0/0}
$cfmap
  :: forall (f :: [* -> *]) a b.
     (a -> b)
     -> Semantic f a
     -> forall (m :: * -> *).
        Monad m =>
        (forall x. Union f x -> m x) -> m b
$cfmap
  = \ (@ (f :: [* -> *]))
      (@ a)
      (@ b)
      (f1 :: a -> b)
      (ds :: Semantic f a)
      (@ (m :: * -> *))
      ($dMonad :: Monad m)
      (eta :: forall x. Union f x -> m x) ->
      fmap
        @ m
        ($p1Applicative @ m ($p1Monad @ m $dMonad))
        @ a
        @ b
        f1
        ((ds `cast` <Co:3>) @ m $dMonad eta)

-- RHS size: {terms: 1, types: 0, coercions: 21, joins: 0/0}
$fFunctorSemantic_$cfmap
  :: forall (f :: [* -> *]) a b.
     (a -> b) -> Semantic f a -> Semantic f b
$fFunctorSemantic_$cfmap = $cfmap `cast` <Co:21>

-- RHS size: {terms: 4, types: 7, coercions: 16, joins: 0/0}
$fFunctorSemantic :: forall (f :: [* -> *]). Functor (Semantic f)
$fFunctorSemantic
  = \ (@ (f :: [* -> *])) ->
      C:Functor
        @ (Semantic f)
        ($fFunctorSemantic_$cfmap @ f)
        (($fApplicativeSemantic4 @ f) `cast` <Co:16>)

-- RHS size: {terms: 19, types: 36, coercions: 3, joins: 0/0}
$fApplicativeSemantic3
  :: forall (f :: [* -> *]) a b.
     Semantic f a
     -> Semantic f b
     -> forall (m :: * -> *).
        Monad m =>
        (forall x. Union f x -> m x) -> m b
$fApplicativeSemantic3
  = \ (@ (f :: [* -> *]))
      (@ a)
      (@ b)
      (a1 :: Semantic f a)
      (a2 :: Semantic f b)
      (@ (m :: * -> *))
      (eta :: Monad m)
      (eta1 :: forall x. Union f x -> m x) ->
      <*>
        @ m
        ($p1Monad @ m eta)
        @ b
        @ b
        ($fApplicativeSemantic4
           @ f @ (b -> b) @ a (breakpoint @ b) a1 @ m eta eta1)
        ((a2 `cast` <Co:3>) @ m eta eta1)

-- RHS size: {terms: 10, types: 17, coercions: 61, joins: 0/0}
$fApplicativeSemantic
  :: forall (f :: [* -> *]). Applicative (Semantic f)
$fApplicativeSemantic
  = \ (@ (f :: [* -> *])) ->
      C:Applicative
        @ (Semantic f)
        ($fFunctorSemantic @ f)
        ($fApplicativeSemantic_$cpure @ f)
        ($fApplicativeSemantic_$c<*> @ f)
        (($fApplicativeSemantic2 @ f) `cast` <Co:25>)
        (($fApplicativeSemantic3 @ f) `cast` <Co:18>)
        ((\ (@ a) (@ b) -> $fApplicativeSemantic1 @ b @ a @ f)
         `cast` <Co:18>)

-- RHS size: {terms: 6, types: 9, coercions: 0, joins: 0/0}
$fMonadSemantic :: forall (f :: [* -> *]). Monad (Semantic f)
$fMonadSemantic
  = \ (@ (f :: [* -> *])) ->
      C:Monad
        @ (Semantic f)
        ($fApplicativeSemantic @ f)
        ($fMonadSemantic_$c>>= @ f)
        ($fMonadSemantic_$c>> @ f)
        ($fApplicativeSemantic_$cpure @ f)

note to self:

this is the diff to get SAT working after late specialize

@@ -319,7 +319,14 @@ getCoreToDo dflags
 
         runWhen late_specialise
           (CoreDoPasses [ CoreDoSpecialising
-                        , simpl_phase 0 ["post-late-spec"] max_iter]),
+                        , simpl_phase 0 ["post-late-spec"] max_iter
+                        , simpl_gently
+                        , CoreDoStaticArgs
+                        , CoreDoSpecialising
+                        , simpl_phase 0 ["post-late-spec"] max_iter
+                        , simpl_phases
+                        , simpl_gently
+                        ]),

{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DefaultSignatures     #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UnicodeSyntax         #-}

module MVP (main) where

import qualified Control.Monad.Trans.State.Strict as S
import           Data.Coerce
import           Data.Functor.Compose
import           Data.Functor.Identity
import           Data.Typeable

newtype Semantic r a = Semantic
  { runSemantic
        :: ∀ m
         . Monad m
        => (∀ x. Union r (Semantic r) x -> m x)
        -> m a
  }

usingSemantic
    :: Monad m
    => (∀ x. Union r (Semantic r) x -> m x)
    -> Semantic r a
    -> m a
usingSemantic k m = runSemantic m k
{-# INLINE usingSemantic #-}

instance Functor (Semantic f) where
  fmap f (Semantic m) = Semantic $ \k -> fmap f $ m k
  {-# INLINE fmap #-}

instance Applicative (Semantic f) where
  pure a = Semantic $ const $ pure a
  {-# INLINE pure #-}

  Semantic f <*> Semantic a = Semantic $ \k -> f k <*> a k
  {-# INLINE (<*>) #-}

instance Monad (Semantic f) where
  return = pure
  {-# INLINE return #-}

  Semantic ma >>= f = Semantic $ \k -> do
    z <- ma k
    runSemantic (f z) k
  {-# INLINE (>>=) #-}

liftSemantic :: Union r (Semantic r) a -> Semantic r a
liftSemantic u = Semantic $ \k -> k u
{-# INLINE liftSemantic #-}

hoistSemantic
    :: (∀ x. Union r (Semantic r) x -> Union r' (Semantic r') x)
    -> Semantic r a
    -> Semantic r' a
hoistSemantic nat (Semantic m) = Semantic $ \k -> m $ \u -> k $ nat u
{-# INLINE hoistSemantic #-}

raise :: forall e r a. Semantic r a -> Semantic (e ': r) a
raise = hoistSemantic $ hoist raise' . weaken
{-# INLINE raise #-}

raise' :: Semantic r a -> Semantic (e ': r) a
raise' = raise
{-# NOINLINE raise' #-}

send :: Member e r => e (Semantic r) a -> Semantic r a
send = liftSemantic . inj
{-# INLINE[3] send #-}

sendM :: Member (Lift m) r => m a -> Semantic r a
sendM = send . Lift
{-# INLINE sendM #-}

run :: Semantic '[] a -> a
run (Semantic m) = runIdentity $ m absurdU
{-# INLINE run #-}

runM :: Monad m => Semantic '[Lift m] a -> m a
runM (Semantic m) = m $ \z ->
  case extract z of
    Yo e s _ f -> do
      a <- unLift e
      pure $ f $ a <$ s
{-# INLINE runM #-}

slowBeforeSpecialization :: Member (State Int) r => Semantic r Int
slowBeforeSpecialization = do
  n <- get
  if n <= 0
     then pure n
     else do
       put $ n - 1
       slowBeforeSpecialization

main :: IO ()
main = print $ countDown 100

countDown :: Int -> Int
countDown s =
  fst . run . runState s $ slowBeforeSpecialization

data State s m a where
  Get :: State s m s
  Put :: s -> State s m ()

get :: Member (State s) r => Semantic r s
get = send Get
{-# INLINE get #-}

put :: Member (State s) r => s -> Semantic r ()
put = send . Put
{-# INLINE put #-}

gets :: Member (State s) r => (s -> a) -> Semantic r a
gets f = fmap f get
{-# INLINE gets #-}

modify :: Member (State s) r => (s -> s) -> Semantic r ()
modify f = do
  s <- get
  put $ f s
{-# INLINE modify #-}

runState :: s -> Semantic (State s ': r) a -> Semantic r (s, a)
runState = stateful $ \case
  Get   -> \s -> pure (s, s)
  Put s -> const $ pure (s, ())
{-# INLINE[3] runState #-}

{-# RULES "runState/reinterpret"
   forall s e (f :: forall m x. e m x -> Semantic (State s ': r) x).
     runState s (reinterpret f e) = stateful (\x s' -> runState s' $ f x) s e
     #-}

swap :: (a, b) -> (b, a)
swap ~(a, b) = (b, a)
{-# INLINE swap #-}

type Tactically m r x = ∀ f. Functor f => Semantic (Tactics f m r ': r) (f x)

interpretH
    :: forall e r a
     . (∀ x m . e m x -> Tactically m r x)
    -> Semantic (e ': r) a
    -> Semantic r a
interpretH f (Semantic m) = m $ \u ->
  case decomp u of
    Left  x -> liftSemantic $ hoist (interpretH f) x
    Right (Yo e s d y) -> do
      a <- runTactics s (interpretH f . d) (f e)
      pure $ y a
{-# INLINE interpretH #-}

interpret
    :: (∀ x m. e m x -> Semantic r x)
    -> Semantic (e ': r) a
    -> Semantic r a
interpret f = interpretH $ \(e :: e m x) -> toH @m $ f e
{-# INLINE interpret #-}

interpretInStateT
    :: (∀ x m. e m x -> S.StateT s (Semantic r) x)
    -> s
    -> Semantic (e ': r) a
    -> Semantic r (s, a)
interpretInStateT f s (Semantic m) = Semantic $ \k ->
  fmap swap $ flip S.runStateT s $ m $ \u ->
    case decomp u of
        Left x -> S.StateT $ \s' ->
          k . fmap swap
            . weave (s', ()) (uncurry $ interpretInStateT_b f)
            $ x
        Right (Yo e z _ y) ->
          fmap (y . (<$ z)) $ S.mapStateT (usingSemantic k) $ f e
{-# INLINE interpretInStateT #-}

interpretInStateT_b
    :: (∀ x m. e m x -> S.StateT s (Semantic r) x)
    -> s
    -> Semantic (e ': r) a
    -> Semantic r (s, a)
interpretInStateT_b = interpretInStateT
{-# NOINLINE interpretInStateT_b #-}

reinterpretH
    :: forall e2 e1 r a
     . (∀ m x. e1 m x -> Tactically m (e2 ': r) x)
    -> Semantic (e1 ': r) a
    -> Semantic (e2 ': r) a
reinterpretH f (Semantic m) = Semantic $ \k -> m $ \u ->
  case decompCoerce u of
    Left x  -> k $ hoist (reinterpretH f) $ x
    Right (Yo e s d y) -> do
      a <- usingSemantic k $ runTactics s (reinterpretH f . d) $ f e
      pure $ y a
{-# INLINE[3] reinterpretH #-}

reinterpret2H
    :: forall e2 e3 e1 r a
     . (∀ m x. e1 m x -> Tactically m (e2 ': e3 ': r) x)
    -> Semantic (e1 ': r) a
    -> Semantic (e2 ': e3 ': r) a
reinterpret2H f (Semantic m) = Semantic $ \k -> m $ \u ->
  case decompCoerce u of
    Left x  -> k $ weaken $ hoist (reinterpret2H f) $ x
    Right (Yo e s d y) -> do
      a <- usingSemantic k $ runTactics s (reinterpret2H f . d) $ f e
      pure $ y a
{-# INLINE[3] reinterpret2H #-}

interceptH
    :: forall e r a. Member e r
    => (∀ x m. e m x -> Tactically m r x)
    -> Semantic r a
    -> Semantic r a
interceptH f (Semantic m) = Semantic $ \k -> m $ \u ->
  case prj @e u of
    Just (Yo e s d y) -> usingSemantic k $ fmap y $ runTactics s d $ f e
    Nothing -> k u
{-# INLINE interceptH #-}

stateful
    :: (∀ x m. e m x -> s -> Semantic r (s, x))
    -> s
    -> Semantic (e ': r) a
    -> Semantic r (s, a)
stateful f = interpretInStateT $ \e -> S.StateT $ fmap swap . f e
{-# INLINE[3] stateful #-}

reinterpret
    :: forall e2 e1 r a
     . (∀ m x. e1 m x -> Semantic (e2 ': r) x)
    -> Semantic (e1 ': r) a
    -> Semantic (e2 ': r) a
reinterpret f = reinterpretH $ \(e :: e m x) -> toH @m $ f e
{-# INLINE[3] reinterpret #-}

reinterpret2
    :: forall e2 e3 e1 r a
     . (∀ m x. e1 m x -> Semantic (e2 ': e3 ': r) x)
    -> Semantic (e1 ': r) a
    -> Semantic (e2 ': e3 ': r) a
reinterpret2 f = reinterpret2H $ \(e :: e m x) -> toH @m $ f e
{-# INLINE[3] reinterpret2 #-}

intercept
    :: forall e r a. Member e r
    => (∀ x m. e m x -> Semantic r x)
    -> Semantic r a
    -> Semantic r a
intercept f (Semantic m) = Semantic $ \k -> m $ \u ->
  case prj @e u of
    Just (Yo e s _ y) -> usingSemantic k $ fmap (y . (<$ s)) $ f e
    Nothing -> k u
{-# INLINE intercept #-}

data Union (r :: [(* -> *) -> * -> *]) (m :: * -> *) a where
  Union
      :: SNat n
         -- ^ A proof that the effect is actually in @r@.
      -> Yo (IndexOf r n) m a
         -- ^ The effect to wrap. The functions 'prj' and 'decomp' can help
         -- retrieve this value later.
      -> Union r m a

data Yo e m a where
  Yo :: (Functor f)
     => e m a
     -> f ()
     -> (forall x. f (m x) -> n (f x))
     -> (f a -> b)
     -> Yo e n b

liftYo :: Functor m => e m a -> Yo e m a
liftYo e = Yo e (Identity ()) (fmap Identity . runIdentity) runIdentity

instance Functor (Yo e m) where
  fmap f (Yo e s d f') = Yo e s d (f . f')

instance Effect (Yo e) where
  weave s' d (Yo e s nt f) =
    Yo e (Compose $ s <$ s')
         (fmap Compose . d . fmap nt . getCompose)
         (fmap f . getCompose)
  hoist = defaultHoist

instance (Functor m) => Functor (Union r m) where
  fmap f (Union w t) = Union w $ fmap' f t
    where
      -- This is necessary to delay the interaction between the type family
      -- 'IndexOf' and the quantified superclass constraint on 'Effect'.
      fmap' :: (Functor m, Effect f) => (a -> b) -> f m a -> f m b
      fmap' = fmap
      {-# INLINE fmap' #-}
  {-# INLINE fmap #-}

instance Effect (Union r) where
  weave s f (Union w e) = Union w $ weave s f e
  {-# INLINE weave #-}

  hoist f (Union w e) = Union w $ hoist f e
  {-# INLINE hoist #-}

type Member e r =
  ( Find r e
  -- , Break (AmbiguousSend r e) (IndexOf r (Found r e))
  , e ~ IndexOf r (Found r e)
  -- , Effect e
  )

data Dict c where Dict :: c => Dict c

induceTypeable :: SNat n -> Dict (Typeable n)
induceTypeable SZ = Dict
induceTypeable (SS _) = Dict
{-# INLINE induceTypeable #-}

data Nat = Z | S Nat
  deriving Typeable

data SNat :: Nat -> * where
  SZ :: SNat 'Z
  SS :: Typeable n => SNat n -> SNat ('S n)
  deriving Typeable

type family IndexOf (ts :: [k]) (n :: Nat) :: k where
  IndexOf (k ': ks) 'Z = k
  IndexOf (k ': ks) ('S n) = IndexOf ks n

type family Found (ts :: [k]) (t :: k) :: Nat where
  Found (t ': ts) t = 'Z
  Found (u ': ts) t = 'S (Found ts t)

class Typeable (Found r t) => Find (r :: [k]) (t :: k) where
  finder :: SNat (Found r t)

instance {-# OVERLAPPING #-} Find (t ': z) t where
  finder = SZ
  {-# INLINE finder #-}

instance ( Find z t
         , Found (_1 ': z) t ~ 'S (Found z t)
         ) => Find (_1 ': z) t where
  finder = SS $ finder @_ @z @t
  {-# INLINE finder #-}

decomp :: Union (e ': r) m a -> Either (Union r m a) (Yo e m a)
decomp (Union p a) =
  case p of
    SZ   -> Right a
    SS n -> Left $ Union n a
{-# INLINE decomp #-}

extract :: Union '[e] m a -> Yo e m a
extract (Union SZ a) = a
extract _ = error "impossible"
{-# INLINE extract #-}

absurdU :: Union '[] m a -> b
absurdU = absurdU

weaken :: Union r m a -> Union (e ': r) m a
weaken (Union n a) =
  case induceTypeable n of
    Dict -> Union (SS n) a
{-# INLINE weaken #-}

inj :: forall r e a m. (Functor m , Member e r) => e m a -> Union r m a
inj e = Union (finder @_ @r @e) $ liftYo e
{-# INLINE inj #-}

prj :: forall e r a m
     . ( Member e r
       )
    => Union r m a
    -> Maybe (Yo e m a)
prj (Union (s :: SNat n) a) =
  case induceTypeable s of
    Dict ->
      case eqT @n @(Found r e) of
        Just Refl -> Just a
        Nothing -> Nothing
{-# INLINE prj #-}

decompCoerce
    :: Union (e ': r) m a
    -> Either (Union (f ': r) m a) (Yo e m a)
decompCoerce (Union p a) =
  case p of
    SZ -> Right a
    SS n -> Left (Union (SS n) a)
{-# INLINE decompCoerce #-}

class (∀ m. Functor m => Functor (e m)) => Effect e where
  weave
      :: (Functor s, Functor m, Functor n)
      => s ()
      -> (∀ x. s (m x) -> n (s x))
      -> e m a
      -> e n (s a)
  default weave
      :: ( Coercible (e m (s a)) (e n (s a))
         , Functor s
         , Functor m
         , Functor n
         )
      => s ()
      -> (∀ x. s (m x) -> n (s x))
      -> e m a
      -> e n (s a)
  weave s _ = coerce . fmap (<$ s)
  {-# INLINE weave #-}

  hoist
        :: ( Functor m
           , Functor n
           )
        => (∀ x. m x -> n x)
        -> e m a
        -> e n a

  default hoist
      :: ( Coercible (e m a) (e n a)
         , Functor m
         )
      => (∀ x. m x -> n x)
      -> e m a
      -> e n a
  hoist _ = coerce
  {-# INLINE hoist #-}

defaultHoist
      :: ( Functor m
         , Functor n
         , Effect e
         )
      => (∀ x. m x -> n x)
      -> e m a
      -> e n a
defaultHoist f
  = fmap runIdentity
  . weave (Identity ())
          (fmap Identity . f . runIdentity)
{-# INLINE defaultHoist #-}

newtype Lift m z a = Lift
  { unLift :: m a
  }

data Tactics f n r m a where
  GetInitialState     :: Tactics f n r m (f ())
  HoistInterpretation :: (a -> n b) -> Tactics f n r m (f a -> Semantic r (f b))

start
    :: forall f n r r' a
     . Member (Tactics f n r) r'
    => n a
    -> Semantic r' (Semantic r (f a))
start na = do
  istate <- send @(Tactics f n r) GetInitialState
  na'    <- continue (const na)
  pure $ na' istate

continue :: Member (Tactics f n r) r' => (a -> n b) -> Semantic r' (f a -> Semantic r (f b))
continue f = send $ HoistInterpretation f

toH
    :: forall n f r r' a e
     . ( Functor f
       , r' ~ (e : r)
       , Member (Tactics f n r) r'
       )
    => Semantic r a
    -> Semantic r' (f a)
toH m = do
  istate <- send @(Tactics f n r) GetInitialState
  raise $ fmap (<$ istate) m

runTactics
   :: Functor f
   => f ()
   -> (∀ x. f (m x) -> Semantic r (f x))
   -> Semantic (Tactics f m r ': r) a
   -> Semantic r a
runTactics s d (Semantic m) = m $ \u ->
  case decomp u of
    Left x -> liftSemantic $ hoist (runTactics s d) x
    Right (Yo GetInitialState s' _ y) ->
      pure $ y $ s <$ s'
    Right (Yo (HoistInterpretation na) s' _ y) -> do
      pure $ y $ (d . fmap na) <$ s'
{-# INLINE runTactics #-}

freer mvp

after !668, -flate-specialise -O2 -fstatic-argument-transformation -fmax-simplifier-iterations=10:

Rec {
-- RHS size: {terms: 22, types: 132, coercions: 5, joins: 0/0}
main3
  :: ((forall x.
       Union '[State Int] (Semantic '[State Int]) x
       -> Int -> Identity (x, Int))
      ~R# (forall x.
           Union '[State Int] (Semantic '[State Int]) x
           -> StateT Int Identity x))
     -> Applicative (StateT Int Identity) => Int -> Identity (Int, Int)
main3
  = \ (sg_s6rY
         :: (forall x.
             Union '[State Int] (Semantic '[State Int]) x
             -> Int -> Identity (x, Int))
            ~R# (forall x.
                 Union '[State Int] (Semantic '[State Int]) x
                 -> StateT Int Identity x))
      (sc_s6rX :: Applicative (StateT Int Identity))
      (eta_B1 :: Int) ->
      case eta_B1 of wild_a5Hp { I# x_a5Hr ->
      case <=# x_a5Hr 0# of {
        __DEFAULT -> main3 @~ <Co:1> sc_s6rX (I# (-# x_a5Hr 1#));
        1# ->
          ((pure @ (StateT Int Identity) sc_s6rX @ Int wild_a5Hp)
           `cast` <Co:4>)
            wild_a5Hp
      }
      }
end Rec }

after keeping EVERYTHING + the simplcore changes:

Rec {
-- RHS size: {terms: 18, types: 6, coercions: 8, joins: 0/0}
main2 :: Int -> Identity (Int, Int)
main2
  = \ (s1_a6pN :: Int) ->
      case s1_a6pN of wild_a5Hp { I# x_a5Hr ->
      case <=# x_a5Hr 0# of {
        __DEFAULT -> main2 (I# (-# x_a5Hr 1#));
        1# -> (wild_a5Hp, wild_a5Hp) `cast` <Co:8>
      }
      }
end Rec }

-- RHS size: {terms: 17, types: 18, coercions: 4, joins: 0/0}
main1 :: String
main1
  = case (main2 (I# 100#)) `cast` <Co:4> of { (a_a2BS, b_a2BT) ->
    case b_a2BT of { I# ww3_a5Lf ->
    case $wshowSignedInt 0# ww3_a5Lf ([] @ Char) of
    { (# ww5_a5Lj, ww6_a5Lk #) ->
    : @ Char ww5_a5Lj ww6_a5Lk
    }
    }
    }

-- RHS size: {terms: 4, types: 0, coercions: 0, joins: 0/0}
main :: IO ()
main = hPutStr' stdout main1 True

completely free abstraction :) :) :)