Created
May 2, 2019 18:09
-
-
Save googleson78/434d70bbe62b666019245755382e7d15 to your computer and use it in GitHub Desktop.
Fusion failure
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Fusion | |
| fusion | |
| Union proofs should simplify FAILED [1] | |
| internal uses of StateT should simplify | |
| internal uses of ExceptT should simplify | |
| `runState . reinterpret` should fuse | |
| who needs Sematic even? | |
| Output | |
| runBatchOutput | |
| should return nothing at batch size 0 | |
| should batch at size 1 | |
| should batch at size 5 | |
| should batch at size 6 | |
| should batch at size 7 | |
| should batch at size 8 | |
| should batch at size 9 | |
| should batch at size 10 | |
| should batch at size 11 | |
| should batch at size 12 | |
| should batch at size 13 | |
| should batch at size 99 | |
| should batch at size 100 | |
| should batch at size 101 | |
| Failures: | |
| test/FusionSpec.hs:23:25: | |
| 1) Fusion.fusion Union proofs should simplify | |
| uncaught exception: ErrorCall | |
| test/FusionSpec.hs:33:23: countDown `hasNoType` Polysemy.Internal.Union.SNat failed: | |
| poly_f2_scZj | |
| :: forall x3 (f1 :: * -> *). | |
| (Identity (f1 x3), Int) -> (Compose Identity f1 x3, Int) | |
| [LclId, | |
| Arity=1, | |
| Str=<L,U(1*U,1*U)>m, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [40] 30 30}] | |
| poly_f2_scZj | |
| = \ (@ x3) | |
| (@ (f1_scZ6 :: * -> *)) | |
| (ds1 [Dmd=<L,U(1*U,1*U)>] :: (Identity (f1 x3), Int)) -> | |
| (case ds1 of { (a3 [Dmd=<S,1*U>], s' [Dmd=<L,A>]) -> | |
| a3 | |
| `cast` (Sym (N:Compose[0] <*>_N <*>_N <Identity>_R <f1>_N <x3>_N) | |
| :: Coercible (Identity (f1 x3)) (Compose Identity f1 x3)) | |
| }, | |
| case ds1 of { (a3 [Dmd=<L,A>], s' [Dmd=<S,1*U>]) -> s' }) | |
| poly_f4_scZh | |
| :: forall x3 (f1 :: * -> *). | |
| (f1 x3, Int) -> (Identity (f1 x3), Int) | |
| [LclId, | |
| Arity=1, | |
| Str=<L,U(1*U,1*U)>m, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [40] 30 30}] | |
| poly_f4_scZh | |
| = \ (@ x3) | |
| (@ (f1_scZ6 :: * -> *)) | |
| (ds1 [Dmd=<L,U(1*U,1*U)>] :: (f1 x3, Int)) -> | |
| (case ds1 of { (a3 [Dmd=<S,1*U>], s' [Dmd=<L,A>]) -> | |
| a3 | |
| `cast` (Sym (N:Identity[0] <f1 x3>_R) | |
| :: Coercible (f1 x3) (Identity (f1 x3))) | |
| }, | |
| case ds1 of { (a3 [Dmd=<L,A>], s' [Dmd=<S,1*U>]) -> s' }) | |
| poly_f7_scZf | |
| :: forall x3 (f1 :: * -> *). | |
| (Int, Compose Identity f1 x3) -> (Int, Compose Identity f1 x3) | |
| [LclId, | |
| Arity=1, | |
| Str=<S,1*U(U,U)>m, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, | |
| Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}] | |
| poly_f7_scZf | |
| = \ (@ x3) | |
| (@ (f1_scZ6 :: * -> *)) | |
| (v [Dmd=<S,1*U(U,U)>] :: (Int, Compose Identity f1 x3)) -> | |
| v | |
| lvl_scZk | |
| :: forall x1. | |
| Union '[State Int] (Sem '[State Int]) x1 | |
| -> Int -> Sem '[] (x1, Int) | |
| [LclId, | |
| Arity=2, | |
| Str=<S,1*U><L,U>, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=NEVER}] | |
| lvl_scZk | |
| = \ (@ x1) | |
| (u [Dmd=<S,1*U>] :: Union '[State Int] (Sem '[State Int]) x1) | |
| (eta_X63 :: Int) -> | |
| case u of { Union @ n_ib2H p [Dmd=<S,1*U>] a1 [Dmd=<S,1*U>] -> | |
| case p of { | |
| SZ co -> | |
| case a1 | |
| `cast` ((Yo | |
| ((IndexOf | |
| <(* -> *) -> * -> *>_N <'[State Int]>_N co)_R ; Sub (D:R:IndexOf[0] | |
| <(* -> *) | |
| -> * -> *>_N | |
| <State Int>_N | |
| <'[]>_N)) | |
| <Sem '[State Int]>_R | |
| <x1>_R)_R | |
| :: Coercible | |
| (Yo (IndexOf '[State Int] n) (Sem '[State Int]) x1) | |
| (Yo (State Int) (Sem '[State Int]) x1)) | |
| of | |
| { Yo @ f1_scYS @ m1_scYT @ a2_scYU | |
| $dFunctor [Dmd=<L,U(A,C(C1(U)))>] ds1 [Dmd=<S,1*U>] z | |
| ds2 [Dmd=<L,A>] y [Dmd=<L,C(U)>] -> | |
| let { | |
| lvl_scZ0 :: (a2, Int) -> (x1, Int) | |
| [LclId, | |
| Arity=1, | |
| Str=<L,U(1*U,1*U)>m {scYV-><L,1*U(A,1*C1(C1(U)))> | |
| scYZ-><L,1*C1(U)>}, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [40] 90 30}] | |
| lvl_scZ0 | |
| = \ (ds3 [Dmd=<L,U(1*U,1*U)>] :: (a2, Int)) -> | |
| (y (<$ | |
| @ f1 | |
| $dFunctor | |
| @ a2 | |
| @ () | |
| (case ds3 of { (a3 [Dmd=<S,1*U>], s' [Dmd=<L,A>]) -> a3 }) | |
| z), | |
| case ds3 of { (a3 [Dmd=<L,A>], s' [Dmd=<S,1*U>]) -> s' }) } in | |
| case ds1 of { | |
| Get co1 -> | |
| let { | |
| lvl_scZ1 :: (a2, a2) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}] | |
| lvl_scZ1 | |
| = (eta_X63 `cast` (Sub (Sym co1) :: Coercible Int a2), | |
| eta_X63 `cast` (Sub (Sym co1) :: Coercible Int a2)) } in | |
| (\ (@ (m :: * -> *)) | |
| (eta_B2 [Dmd=<L,U(U(U(C(C1(U)),A),C(U),A,A,A,A),A,A,A,A)>] | |
| :: Monad m) | |
| _ [Occ=Dead, Dmd=<L,A>] -> | |
| fmap | |
| @ m | |
| ($p1Applicative @ m ($p1Monad @ m eta_B2)) | |
| @ (a2, Int) | |
| @ (x1, Int) | |
| lvl_scZ0 | |
| ((pure @ m ($p1Monad @ m eta_B2) @ (a2, a2) lvl_scZ1) | |
| `cast` (<m>_R ((,) <a2>_N co1)_N | |
| :: Coercible (m (a2, a2)) (m (a2, Int))))) | |
| `cast` (Sym (N:Sem[0] <'[]>_N <(x1, Int)>_N) | |
| :: Coercible | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) -> m (x1, Int)) | |
| (Sem '[] (x1, Int))); | |
| Put co1 s2 -> | |
| let { | |
| lvl_scZ3 :: ((), Int) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}] | |
| lvl_scZ3 = ((), s2) } in | |
| (\ (@ (m :: * -> *)) | |
| (eta_B2 [Dmd=<L,U(U(U(C(C1(U)),A),C(U),A,A,A,A),A,A,A,A)>] | |
| :: Monad m) | |
| _ [Occ=Dead, Dmd=<L,A>] -> | |
| fmap | |
| @ m | |
| ($p1Applicative @ m ($p1Monad @ m eta_B2)) | |
| @ (a2, Int) | |
| @ (x1, Int) | |
| lvl_scZ0 | |
| ((pure @ m ($p1Monad @ m eta_B2) @ ((), Int) lvl_scZ3) | |
| `cast` (<m>_R ((,) (Sym co1) <Int>_N)_N | |
| :: Coercible (m ((), Int)) (m (a2, Int))))) | |
| `cast` (Sym (N:Sem[0] <'[]>_N <(x1, Int)>_N) | |
| :: Coercible | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) -> m (x1, Int)) | |
| (Sem '[] (x1, Int))) | |
| } | |
| }; | |
| SS @ n1_ibhZ co $dTypeable [Dmd=<L,A>] n2 -> | |
| case a1 | |
| `cast` ((Yo | |
| ((IndexOf | |
| <(* -> *) -> * -> *>_N <'[State Int]>_N co)_R ; Sub (D:R:IndexOf[1] | |
| <(* -> *) | |
| -> * -> *>_N | |
| <State Int>_N | |
| <'[]>_N | |
| <n1>_N)) | |
| <Sem '[State Int]>_R | |
| <x1>_R)_R | |
| :: Coercible | |
| (Yo (IndexOf '[State Int] n) (Sem '[State Int]) x1) | |
| (Yo (IndexOf '[] n1) (Sem '[State Int]) x1)) | |
| of | |
| { Yo @ f1_scZ6 @ m1_scZ7 @ a2_scZ8 $dFunctor2 [Dmd=<L,U(C(U),A)>] | |
| e1 s3 nt [Dmd=<L,C(C1(C1(U)))>] f3 [Dmd=<L,C(U)>] -> | |
| let { | |
| u1_sd0P [Dmd=<L,U(C(U),A)>] :: Functor (Compose Identity f1) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=True, | |
| WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 30 0}] | |
| u1_sd0P | |
| = $fFunctorCompose | |
| @ Identity @ f1 $fFunctorIdentity $dFunctor2 } in | |
| let { | |
| u1_sd0Q :: Functor (Compose ((,) Int) (Compose Identity f1)) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=True, | |
| WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 30 0}] | |
| u1_sd0Q | |
| = $fFunctorCompose | |
| @ ((,) Int) | |
| @ (Compose Identity f1) | |
| ($fFunctor(,) @ Int) | |
| u1_sd0P } in | |
| let { | |
| u1_sd0R :: (Int, Compose Identity f1 ()) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}] | |
| u1_sd0R | |
| = (eta_X63, | |
| s3 | |
| `cast` (Sym (N:Identity[0] <f1 ()>_R) ; Sym (N:Compose[0] | |
| <*>_N | |
| <*>_N | |
| <Identity>_R | |
| <f1>_N | |
| <()>_N) | |
| :: Coercible (f1 ()) (Compose Identity f1 ()))) } in | |
| let { | |
| u1_sd0S | |
| :: forall x3. | |
| Compose ((,) Int) (Compose Identity f1) (m1 x3) | |
| -> Sem '[] (Compose ((,) Int) (Compose Identity f1) x3) | |
| [LclId, | |
| Arity=1, | |
| Str=<L,1*U(U,U)> {scZc-><L,1*C1(C1(C1(U)))>}, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [20] 500 60}] | |
| u1_sd0S | |
| = \ (@ x3) | |
| (x4 [Dmd=<L,1*U(U,U)>] | |
| :: Compose ((,) Int) (Compose Identity f1) (m1 x3)) -> | |
| let { | |
| ds1 [Dmd=<L,C(C1(U))>] :: Sem '[] (Int, Compose Identity f1 x3) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False, | |
| WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 360 60}] | |
| ds1 | |
| = case x4 | |
| `cast` (N:Compose[0] | |
| <*>_N <*>_N <(,) Int>_R <Compose Identity f1>_N <m1 x3>_N | |
| :: Coercible | |
| (Compose ((,) Int) (Compose Identity f1) (m1 x3)) | |
| (Int, Compose Identity f1 (m1 x3))) | |
| of | |
| { (x5, y) -> | |
| let { | |
| ds1 [Dmd=<L,C(C1(U))>] :: Sem '[] (f1 x3, Int) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False, | |
| WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 50 0}] | |
| ds1 | |
| = ((hoistStateIntoStateT_b | |
| @ Int | |
| @ '[] | |
| @ (f1 x3) | |
| (nt | |
| @ x3 | |
| (y | |
| `cast` (N:Compose[0] | |
| <*>_N | |
| <*>_N | |
| <Identity>_R | |
| <f1>_N | |
| <m1 x3>_N ; N:Identity[0] <f1 (m1 x3)>_R | |
| :: Coercible | |
| (Compose Identity f1 (m1 x3)) (f1 (m1 x3)))))) | |
| `cast` (N:StateT[0] <Int>_N <Sem '[]>_R <f1 x3>_N | |
| :: Coercible | |
| (StateT Int (Sem '[]) (f1 x3)) | |
| (Int -> Sem '[] (f1 x3, Int)))) | |
| x5 } in | |
| (\ (@ (m :: * -> *)) | |
| ($dMonad [Dmd=<L,U(U(U(U,U),U,U,U,U,U),U,U,U,U)>] :: Monad m) | |
| (eta_Xz [OS=OneShot] | |
| :: forall x6. Union '[] (Sem '[]) x6 -> m x6) -> | |
| fmap | |
| @ m | |
| ($p1Applicative @ m ($p1Monad @ m $dMonad)) | |
| @ (Compose Identity f1 x3, Int) | |
| @ (Int, Compose Identity f1 x3) | |
| (swap @ (Compose Identity f1 x3) @ Int) | |
| (fmap | |
| @ m | |
| ($p1Applicative @ m ($p1Monad @ m $dMonad)) | |
| @ (Identity (f1 x3), Int) | |
| @ (Compose Identity f1 x3, Int) | |
| (poly_f2_scZj @ x3 @ f1) | |
| (fmap | |
| @ m | |
| ($p1Applicative @ m ($p1Monad @ m $dMonad)) | |
| @ (f1 x3, Int) | |
| @ (Identity (f1 x3), Int) | |
| (poly_f4_scZh @ x3 @ f1) | |
| ((ds1 | |
| `cast` (N:Sem[0] <'[]>_N <(f1 x3, Int)>_N | |
| :: Coercible | |
| (Sem '[] (f1 x3, Int)) | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) | |
| -> m (f1 x3, Int)))) | |
| @ m $dMonad eta_Xz)))) | |
| `cast` (Sym (N:Sem[0] <'[]>_N <(Int, Compose Identity f1 x3)>_N) | |
| :: Coercible | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) | |
| -> m (Int, Compose Identity f1 x3)) | |
| (Sem '[] (Int, Compose Identity f1 x3))) | |
| } } in | |
| (\ (@ (m :: * -> *)) | |
| ($dMonad [Dmd=<L,U(U(U(U,U),U,U,U,U,U),U,U,U,U)>] :: Monad m) | |
| (eta_Xv :: forall x5. Union '[] (Sem '[]) x5 -> m x5) -> | |
| fmap | |
| @ m | |
| ($p1Applicative @ m ($p1Monad @ m $dMonad)) | |
| @ (Int, Compose Identity f1 x3) | |
| @ (Compose ((,) Int) (Compose Identity f1) x3) | |
| ((poly_f7_scZf @ x3 @ f1) | |
| `cast` (<(Int, Compose Identity f1 x3)>_R | |
| ->_R Sym (N:Compose[0] | |
| <*>_N | |
| <*>_N | |
| <(,) Int>_R | |
| <Compose Identity f1>_N | |
| <x3>_N) | |
| :: Coercible | |
| ((Int, Compose Identity f1 x3) | |
| -> (Int, Compose Identity f1 x3)) | |
| ((Int, Compose Identity f1 x3) | |
| -> Compose ((,) Int) (Compose Identity f1) x3))) | |
| ((ds1 | |
| `cast` (N:Sem[0] <'[]>_N <(Int, Compose Identity f1 x3)>_N | |
| :: Coercible | |
| (Sem '[] (Int, Compose Identity f1 x3)) | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) | |
| -> m (Int, Compose Identity f1 x3)))) | |
| @ m $dMonad eta_Xv)) | |
| `cast` (Sym (N:Sem[0] | |
| <'[]>_N <Compose ((,) Int) (Compose Identity f1) x3>_N) | |
| :: Coercible | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) | |
| -> m (Compose ((,) Int) (Compose Identity f1) x3)) | |
| (Sem '[] (Compose ((,) Int) (Compose Identity f1) x3))) } in | |
| let { | |
| u1_sd0T :: Compose ((,) Int) (Compose Identity f1) a2 -> (x1, Int) | |
| [LclId, | |
| Arity=1, | |
| Str=<S,1*U(U,U)>m {scZd-><L,1*C1(U)>}, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [20] 40 30}] | |
| u1_sd0T | |
| = \ (x3 [Dmd=<S,1*U(U,U)>] | |
| :: Compose ((,) Int) (Compose Identity f1) a2) -> | |
| case x3 | |
| `cast` (N:Compose[0] | |
| <*>_N <*>_N <(,) Int>_R <Compose Identity f1>_N <a2>_N | |
| :: Coercible | |
| (Compose ((,) Int) (Compose Identity f1) a2) | |
| (Int, Compose Identity f1 a2)) | |
| of | |
| { (x4, y) -> | |
| (f3 | |
| (y | |
| `cast` (N:Compose[0] | |
| <*>_N <*>_N <Identity>_R <f1>_N <a2>_N ; N:Identity[0] <f1 a2>_R | |
| :: Coercible (Compose Identity f1 a2) (f1 a2))), | |
| x4) | |
| } } in | |
| let { | |
| u1_sd0U :: Yo (IndexOf '[] n1) (Sem '[]) (x1, Int) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 60}] | |
| u1_sd0U | |
| = Yo | |
| @ (IndexOf '[] n1) | |
| @ (Sem '[]) | |
| @ (x1, Int) | |
| @ (Compose ((,) Int) (Compose Identity f1)) | |
| @ m1 | |
| @ a2 | |
| u1_sd0Q | |
| e1 | |
| (u1_sd0R | |
| `cast` (Sym (N:Compose[0] | |
| <*>_N <*>_N <(,) Int>_R <Compose Identity f1>_N <()>_N) | |
| :: Coercible | |
| (Int, Compose Identity f1 ()) | |
| (Compose ((,) Int) (Compose Identity f1) ()))) | |
| u1_sd0S | |
| u1_sd0T } in | |
| let { | |
| u1 :: Union '[] (Sem '[]) (x1, Int) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}] | |
| u1 = Union @ '[] @ (Sem '[]) @ (x1, Int) @ n1 n2 u1_sd0U } in | |
| (\ (@ (m :: * -> *)) | |
| _ [Occ=Dead, Dmd=<L,A>] | |
| (k [Dmd=<C(S),1*C1(U)>] | |
| :: forall x3. Union '[] (Sem '[]) x3 -> m x3) -> | |
| k @ (x1, Int) u1) | |
| `cast` (Sym (N:Sem[0] <'[]>_N <(x1, Int)>_N) | |
| :: Coercible | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) -> m (x1, Int)) | |
| (Sem '[] (x1, Int))) | |
| } | |
| } | |
| } | |
| lvl_scYO :: Applicative (StateT Int (Sem '[])) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=True, | |
| WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 30 0}] | |
| lvl_scYO | |
| = $fApplicativeStateT | |
| @ (Sem '[]) @ Int ($fFunctorSem @ '[]) ($fMonadSem @ '[]) | |
| lvl_sd0w :: State Int (Sem '[State Int]) Int | |
| [LclId, | |
| Str=m1, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 0 10}] | |
| lvl_sd0w | |
| = Get | |
| @ (* -> *) | |
| @ Int | |
| @ (Sem '[State Int]) | |
| @ Int | |
| @~ (<Int>_N :: Int ~ Int) | |
| lvl_sd0k :: SNat 'Z | |
| [LclId, | |
| Str=m1, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 0 10}] | |
| lvl_sd0k = SZ @ 'Z @~ (<'Z>_N :: 'Z ~ 'Z) | |
| poly_f_scwI :: forall x1. x1 -> x1 | |
| [LclId, | |
| Arity=1, | |
| Str=<S,1*U>, | |
| Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, | |
| Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True) | |
| Tmpl= \ (@ x1) (v [Occ=Once] :: x1) -> v}] | |
| poly_f_scwI = \ (@ x1) (v [Dmd=<S,1*U>] :: x1) -> v | |
| lvl_scBU | |
| :: forall x1. | |
| Identity (Sem '[State Int] x1) | |
| -> forall (m :: * -> *). | |
| Monad m => | |
| (forall x3. Union '[State Int] (Sem '[State Int]) x3 -> m x3) | |
| -> m (Identity x1) | |
| [LclId, | |
| Arity=3, | |
| Str=<L,1*C1(C1(U))><S(S(S(C(C(S))L)LLLLL)LLLL),U(U(U(U,U),U,U,U,U,U),U,U,U,U)><L,U>, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [60 30 0] 110 0}] | |
| lvl_scBU | |
| = \ (@ x1) | |
| (x2 [Dmd=<L,1*C1(C1(U))>] :: Identity (Sem '[State Int] x1)) | |
| (@ (m :: * -> *)) | |
| ($dMonad [Dmd=<S(S(S(C(C(S))L)LLLLL)LLLL),U(U(U(U,U),U,U,U,U,U),U,U,U,U)>] | |
| :: Monad m) | |
| (eta_X5L | |
| :: forall x3. Union '[State Int] (Sem '[State Int]) x3 -> m x3) -> | |
| fmap | |
| @ m | |
| ($p1Applicative @ m ($p1Monad @ m $dMonad)) | |
| @ x1 | |
| @ (Identity x1) | |
| ((poly_f_scwI @ x1) | |
| `cast` (<x1>_R ->_R Sym (N:Identity[0] <x1>_R) | |
| :: Coercible (x1 -> x1) (x1 -> Identity x1))) | |
| ((x2 | |
| `cast` (N:Identity[0] (N:Sem[0] <'[State Int]>_N <x1>_N) | |
| :: Coercible | |
| (Identity (Sem '[State Int] x1)) | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[State Int] (Sem '[State Int]) x -> m x) | |
| -> m x1))) | |
| @ m $dMonad eta_X5L) | |
| lvl_scYI :: Yo (State Int) (Sem '[State Int]) Int | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 60}] | |
| lvl_scYI | |
| = Yo | |
| @ (State Int) | |
| @ (Sem '[State Int]) | |
| @ Int | |
| @ Identity | |
| @ (Sem '[State Int]) | |
| @ Int | |
| $fFunctorIdentity | |
| lvl_sd0w | |
| (() | |
| `cast` (Sym (N:Identity[0] <()>_R) :: Coercible () (Identity ()))) | |
| (lvl_scBU | |
| `cast` (forall (x1 :: <*>_N). | |
| <Identity (Sem '[State Int] x1)>_R | |
| ->_R Sym (N:Sem[0] <'[State Int]>_N <Identity x1>_N) | |
| :: Coercible | |
| (forall x1. | |
| Identity (Sem '[State Int] x1) | |
| -> forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[State Int] (Sem '[State Int]) x -> m x) | |
| -> m (Identity x1)) | |
| (forall x1. | |
| Identity (Sem '[State Int] x1) -> Sem '[State Int] (Identity x1)))) | |
| (($fFoldableIdentity2 @ Int) | |
| `cast` (<Identity Int>_R ->_R N:Identity[0] <Int>_R | |
| :: Coercible (Identity Int -> Identity Int) (Identity Int -> Int))) | |
| lvl_scYJ :: Union '[State Int] (Sem '[State Int]) Int | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}] | |
| lvl_scYJ | |
| = Union | |
| @ '[State Int] | |
| @ (Sem '[State Int]) | |
| @ Int | |
| @ (Found '[State Int] (State Int)) | |
| (lvl_sd0k | |
| `cast` ((SNat | |
| (Sym (D:R:Found[1] | |
| <(* -> *) -> * -> *>_N <State Int>_N <'[]>_N)))_R | |
| :: Coercible (SNat 'Z) (SNat (Found '[State Int] (State Int))))) | |
| (lvl_scYI | |
| `cast` ((Yo | |
| (Sub (Sym (D:R:IndexOf[0] | |
| <(* -> *) -> * -> *>_N <State Int>_N <'[]>_N)) ; (IndexOf | |
| <(* -> *) | |
| -> * -> *>_N | |
| <'[State | |
| Int]>_N | |
| (Sym (D:R:Found[1] | |
| <(* | |
| -> *) | |
| -> * | |
| -> *>_N | |
| <State | |
| Int>_N | |
| <'[]>_N)))_R) | |
| <Sem '[State Int]>_R | |
| <Int>_R)_R | |
| :: Coercible | |
| (Yo (State Int) (Sem '[State Int]) Int) | |
| (Yo | |
| (IndexOf '[State Int] (Found '[State Int] (State Int))) | |
| (Sem '[State Int]) | |
| Int))) | |
| $s$wgo_sd3f [Occ=LoopBreaker] | |
| :: (Coercible | |
| (forall x1. | |
| Union '[State Int] (Sem '[State Int]) x1 | |
| -> Int -> Sem '[] (x1, Int)) | |
| (forall x1. | |
| Union '[State Int] (Sem '[State Int]) x1 | |
| -> StateT Int (Sem '[]) x1), | |
| Applicative (StateT Int (Sem '[]))) => | |
| Int -> Sem '[] (Int, Int) | |
| [LclId, | |
| Arity=3, | |
| Str=<L,U><L,U(A,C(C1(C1(C1(U)))),A,A,A,A)><L,U>, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [0 30 0] 442 60}] | |
| $s$wgo_sd3f | |
| = \ (sg_sd1M | |
| :: Coercible | |
| (forall x1. | |
| Union '[State Int] (Sem '[State Int]) x1 | |
| -> Int -> Sem '[] (x1, Int)) | |
| (forall x1. | |
| Union '[State Int] (Sem '[State Int]) x1 | |
| -> StateT Int (Sem '[]) x1)) | |
| (sc_sd1L [Dmd=<L,U(A,C(C1(C1(C1(U)))),A,A,A,A)>] | |
| :: Applicative (StateT Int (Sem '[]))) | |
| (eta_B1 :: Int) -> | |
| let { | |
| ds [Dmd=<L,C(C1(U))>] :: Sem '[] (Int, Int) | |
| [LclId, | |
| Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False, | |
| WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 30 0}] | |
| ds = lvl_scZk @ Int lvl_scYJ eta_B1 } in | |
| (\ (@ (m :: * -> *)) | |
| ($dMonad [Dmd=<L,U(U,U,U,U,U)>] :: Monad m) | |
| (k :: forall x. Union '[] (Sem '[]) x -> m x) -> | |
| >>= | |
| @ m | |
| $dMonad | |
| @ (Int, Int) | |
| @ (Int, Int) | |
| ((ds | |
| `cast` (N:Sem[0] <'[]>_N <(Int, Int)>_N | |
| :: Coercible | |
| (Sem '[] (Int, Int)) | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) -> m (Int, Int)))) | |
| @ m $dMonad k) | |
| (\ (z [Dmd=<S(S(S)L),1*U(1*U(U),U)>] :: (Int, Int)) -> | |
| case z of { (a1 [Dmd=<S(S),1*U(U)>], s') -> | |
| case a1 of wild { I# x [Dmd=<S,U>] -> | |
| case <=# x 0# of { | |
| __DEFAULT -> | |
| >>= | |
| @ m | |
| $dMonad | |
| @ ((), Int) | |
| @ (Int, Int) | |
| (((lvl_scZk | |
| @ () | |
| (Union | |
| @ '[State Int] | |
| @ (Sem '[State Int]) | |
| @ () | |
| @ (Found '[State Int] (State Int)) | |
| (lvl_sd0k | |
| `cast` ((SNat | |
| (Sym (D:R:Found[1] | |
| <(* -> *) -> * -> *>_N <State Int>_N <'[]>_N)))_R | |
| :: Coercible | |
| (SNat 'Z) (SNat (Found '[State Int] (State Int))))) | |
| ((Yo | |
| @ (State Int) | |
| @ (Sem '[State Int]) | |
| @ () | |
| @ Identity | |
| @ (Sem '[State Int]) | |
| @ () | |
| $fFunctorIdentity | |
| (Put | |
| @ (* -> *) | |
| @ Int | |
| @ (Sem '[State Int]) | |
| @ () | |
| @~ (<()>_N :: () ~ ()) | |
| (I# (-# x 1#))) | |
| (() | |
| `cast` (Sym (N:Identity[0] <()>_R) :: Coercible () (Identity ()))) | |
| (lvl_scBU | |
| `cast` (forall (x1 :: <*>_N). | |
| <Identity (Sem '[State Int] x1)>_R | |
| ->_R Sym (N:Sem[0] <'[State Int]>_N <Identity x1>_N) | |
| :: Coercible | |
| (forall x1. | |
| Identity (Sem '[State Int] x1) | |
| -> forall (m :: * -> *). | |
| Monad m => | |
| (forall x. | |
| Union '[State Int] (Sem '[State Int]) x -> m x) | |
| -> m (Identity x1)) | |
| (forall x1. | |
| Identity (Sem '[State Int] x1) | |
| -> Sem '[State Int] (Identity x1)))) | |
| (($fFoldableIdentity2 @ ()) | |
| `cast` (<Identity ()>_R ->_R N:Identity[0] <()>_R | |
| :: Coercible | |
| (Identity () -> Identity ()) (Identity () -> ())))) | |
| `cast` ((Yo | |
| (Sub (Sym (D:R:IndexOf[0] | |
| <(* -> *) -> * -> *>_N | |
| <State Int>_N | |
| <'[]>_N)) ; (IndexOf | |
| <(* -> *) -> * -> *>_N | |
| <'[State Int]>_N | |
| (Sym (D:R:Found[1] | |
| <(* -> *) | |
| -> * -> *>_N | |
| <State Int>_N | |
| <'[]>_N)))_R) | |
| <Sem '[State Int]>_R | |
| <()>_R)_R | |
| :: Coercible | |
| (Yo (State Int) (Sem '[State Int]) ()) | |
| (Yo | |
| (IndexOf '[State Int] (Found '[State Int] (State Int))) | |
| (Sem '[State Int]) | |
| ())))) | |
| s') | |
| `cast` (N:Sem[0] <'[]>_N <((), Int)>_N | |
| :: Coercible | |
| (Sem '[] ((), Int)) | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) -> m ((), Int)))) | |
| @ m $dMonad k) | |
| (\ (z [Dmd=<L,1*U(A,1*U)>] :: ((), Int)) -> | |
| (($s$wgo_sd3f | |
| @~ (sg | |
| :: Coercible | |
| (forall x1. | |
| Union '[State Int] (Sem '[State Int]) x1 | |
| -> Int -> Sem '[] (x1, Int)) | |
| (forall x1. | |
| Union '[State Int] (Sem '[State Int]) x1 | |
| -> StateT Int (Sem '[]) x1)) | |
| sc_sd1L | |
| (case z of { (a1 [Dmd=<L,A>], s' [Dmd=<S,1*U>]) -> s' })) | |
| `cast` (N:Sem[0] <'[]>_N <(Int, Int)>_N | |
| :: Coercible | |
| (Sem '[] (Int, Int)) | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) -> m (Int, Int)))) | |
| @ m $dMonad k); | |
| 1# -> | |
| ((((pure @ (StateT Int (Sem '[])) sc_sd1L @ Int wild) | |
| `cast` (N:StateT[0] <Int>_N <Sem '[]>_R <Int>_N | |
| :: Coercible | |
| (StateT Int (Sem '[]) Int) (Int -> Sem '[] (Int, Int)))) | |
| s') | |
| `cast` (N:Sem[0] <'[]>_N <(Int, Int)>_N | |
| :: Coercible | |
| (Sem '[] (Int, Int)) | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) -> m (Int, Int)))) | |
| @ m $dMonad k | |
| } | |
| } | |
| })) | |
| `cast` (Sym (N:Sem[0] <'[]>_N <(Int, Int)>_N) | |
| :: Coercible | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) -> m (Int, Int)) | |
| (Sem '[] (Int, Int))) | |
| countDown :: Int -> Int | |
| [LclIdX, | |
| Arity=1, | |
| Str=<L,U>, | |
| Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, | |
| WorkFree=True, Expandable=True, Guidance=IF_ARGS [0] 60 0}] | |
| countDown | |
| = \ (start :: Int) -> | |
| case ((($s$wgo_sd3f | |
| @~ (forall (x1 :: <*>_N). | |
| <Union '[State Int] (Sem '[State Int]) x1>_R | |
| ->_R Sym (N:StateT[0] <Int>_N <Sem '[]>_R <x1>_N) | |
| :: Coercible | |
| (forall x1. | |
| Union '[State Int] (Sem '[State Int]) x1 | |
| -> Int -> Sem '[] (x1, Int)) | |
| (forall x1. | |
| Union '[State Int] (Sem '[State Int]) x1 | |
| -> StateT Int (Sem '[]) x1)) | |
| lvl_scYO | |
| start) | |
| `cast` (N:Sem[0] <'[]>_N <(Int, Int)>_N | |
| :: Coercible | |
| (Sem '[] (Int, Int)) | |
| (forall (m :: * -> *). | |
| Monad m => | |
| (forall x. Union '[] (Sem '[]) x -> m x) -> m (Int, Int)))) | |
| @ Identity | |
| $fMonadIdentity | |
| (\ (@ x) -> absurdU @ (Sem '[]) @ x @ (Identity x))) | |
| `cast` (N:Identity[0] <(Int, Int)>_R | |
| :: Coercible (Identity (Int, Int)) (Int, Int)) | |
| of | |
| { (x [Dmd=<L,A>], y [Dmd=<S,1*U(U)>]) -> | |
| y | |
| } | |
| CallStack (from HasCallStack): | |
| error, called at test/FusionSpec.hs:23:25 in main:FusionSpec | |
| To rerun use: --match "/Fusion/fusion/Union proofs should simplify/" | |
| Randomized with seed 489679891 | |
| Finished in 0.0150 seconds | |
| 19 examples, 1 failure |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment