diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,4 @@
+# Changes
+
+## Version 0.1.0.0
+Initial release.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2021-2022, Sirui Lu (siruilu@cs.washington.edu)
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of the developer (Sirui Lu) nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,3 @@
+# grisette-monad-coroutine
+
+This package provides support for the [monad-coroutine](https://hackage.haskell.org/package/monad-coroutine) package with [Grisette](https://hackage.haskell.org/package/grisette).
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+
+main = defaultMain
diff --git a/grisette-monad-coroutine.cabal b/grisette-monad-coroutine.cabal
new file mode 100644
--- /dev/null
+++ b/grisette-monad-coroutine.cabal
@@ -0,0 +1,80 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.35.1.
+--
+-- see: https://github.com/sol/hpack
+
+name:           grisette-monad-coroutine
+version:        0.1.0.0
+synopsis:       Support for monad-coroutine package with Grisette
+description:    Orphan instances and wrappers for monad-coroutine package with Grisette.
+category:       Formal Methods, Theorem Provers, Symbolic Computation, SMT
+homepage:       https://github.com/lsrcz/grisette-monad-coroutine#readme
+bug-reports:    https://github.com/lsrcz/grisette-monad-coroutine/issues
+author:         Sirui Lu
+maintainer:     Sirui Lu (siruilu@cs.washington.edu)
+copyright:      2021-2023 Sirui Lu
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    CHANGELOG.md
+
+source-repository head
+  type: git
+  location: https://github.com/lsrcz/grisette-monad-coroutine
+
+flag fast
+  description: Compile with O2 optimization
+  manual: False
+  default: True
+
+library
+  exposed-modules:
+      Grisette.Lib.Control.Monad.Coroutine
+      Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctors
+      Grisette.Lib.MonadCoroutine
+  other-modules:
+      Paths_grisette_monad_coroutine
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -ferror-spans
+  build-depends:
+      base >4.14 && <5
+    , grisette >=0.1.0 && <0.2
+    , monad-coroutine >=0.9.0.4 && <9.3
+    , mtl >=2.2.2 && <2.3
+    , transformers >=0.5.6.2 && <0.6
+  default-language: Haskell2010
+  if flag(fast)
+    ghc-options: -O2
+  else
+    ghc-options: -O0
+
+test-suite spec
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctorsTests
+      Grisette.Lib.Control.Monad.CoroutineTests
+      Paths_grisette_monad_coroutine
+  hs-source-dirs:
+      test
+  ghc-options: -Wall -ferror-spans
+  build-depends:
+      base >4.14 && <5
+    , grisette >=0.1.0 && <0.2
+    , grisette-monad-coroutine
+    , monad-coroutine >=0.9.0.4 && <9.3
+    , mtl >=2.2.2 && <2.3
+    , tasty >=1.1.0.3 && <1.5
+    , tasty-hunit ==0.10.*
+    , tasty-quickcheck >=0.10.1 && <0.11
+    , tasty-test-reporter >=0.1.1.2 && <0.2
+    , transformers >=0.5.6.2 && <0.6
+  default-language: Haskell2010
+  if flag(fast)
+    ghc-options: -O2
+  else
+    ghc-options: -O0
diff --git a/src/Grisette/Lib/Control/Monad/Coroutine.hs b/src/Grisette/Lib/Control/Monad/Coroutine.hs
new file mode 100644
--- /dev/null
+++ b/src/Grisette/Lib/Control/Monad/Coroutine.hs
@@ -0,0 +1,260 @@
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+-- |
+-- Module      :   Grisette.Lib.Control.Monad.Coroutine
+-- Copyright   :   (c) Sirui Lu 2021-2023
+-- License     :   BSD-3-Clause (see the LICENSE file)
+--
+-- Maintainer  :   siruilu@cs.washington.edu
+-- Stability   :   Experimental
+-- Portability :   GHC only
+module Grisette.Lib.Control.Monad.Coroutine
+  ( mrgSuspend,
+    mrgMapMonad,
+    mrgMapSuspension,
+    mrgMapFirstSuspension,
+    mrgRunCoroutine,
+    mrgBounce,
+    mrgPogoStick,
+    mrgPogoStickM,
+    mrgFoldRun,
+    MrgPairBinder,
+    mrgSequentialBinder,
+  )
+where
+
+import Control.Monad.Coroutine hiding (merge)
+import Grisette.Core
+import Grisette.Lib.Control.Monad
+
+liftCoroEitherMergingStrategy ::
+  (Mergeable1 s, Mergeable1 m) =>
+  MergingStrategy x ->
+  MergingStrategy (Either (s (Coroutine s m x)) x)
+liftCoroEitherMergingStrategy ms =
+  liftRootStrategy2 (liftRootStrategy (liftRootStrategy ms)) ms
+
+coroEitherMergingStrategy ::
+  (Mergeable1 s, Mergeable1 m, Mergeable x) =>
+  MergingStrategy (Either (s (Coroutine s m x)) x)
+coroEitherMergingStrategy = liftRootStrategy2 rootStrategy1 rootStrategy
+
+instance
+  (Mergeable1 m, Mergeable a, Mergeable1 sus) =>
+  Mergeable (Coroutine sus m a)
+  where
+  rootStrategy =
+    wrapStrategy
+      (liftRootStrategy coroEitherMergingStrategy)
+      Coroutine
+      (\(Coroutine v) -> v)
+
+instance (Mergeable1 m, Mergeable1 sus) => Mergeable1 (Coroutine sus m) where
+  liftRootStrategy m =
+    wrapStrategy
+      (liftRootStrategy $ liftCoroEitherMergingStrategy m)
+      Coroutine
+      (\(Coroutine v) -> v)
+
+instance
+  (UnionLike m, Mergeable a, Mergeable1 sus) =>
+  SimpleMergeable (Coroutine sus m a)
+  where
+  mrgIte = mrgIf
+
+instance
+  (UnionLike m, Mergeable1 sus) =>
+  SimpleMergeable1 (Coroutine sus m)
+  where
+  liftMrgIte m = mrgIfWithStrategy (SimpleStrategy m)
+
+instance
+  (UnionLike m, Mergeable1 sus) =>
+  UnionLike (Coroutine sus m)
+  where
+  mergeWithStrategy s ((Coroutine v) :: Coroutine sus m a) =
+    Coroutine $ mergeWithStrategy (liftCoroEitherMergingStrategy s) v
+  mrgIfWithStrategy s cond (Coroutine t) (Coroutine f) =
+    Coroutine $ mrgIfWithStrategy (liftCoroEitherMergingStrategy s) cond t f
+  single x = Coroutine $ single $ Right x
+  unionIf cond (Coroutine t) (Coroutine f) =
+    Coroutine $ unionIf cond t f
+
+instance
+  (ExtractSymbolics (m (Either (sus (Coroutine sus m a)) a))) =>
+  ExtractSymbolics (Coroutine sus m a)
+  where
+  extractSymbolics (Coroutine v) = extractSymbolics v
+
+-- | Symbolic version of 'Control.Monad.Coroutine.suspend',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgSuspend ::
+  forall m s x.
+  (Functor s, MonadUnion m, Mergeable x, Mergeable1 s) =>
+  s (Coroutine s m x) ->
+  Coroutine s m x
+mrgSuspend s =
+  Coroutine
+    $ mergeWithStrategy
+      coroEitherMergingStrategy
+    $ return (Left s)
+{-# INLINEABLE mrgSuspend #-}
+
+-- | Symbolic version of 'Control.Monad.Coroutine.mapMonad',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgMapMonad ::
+  forall s m m' x.
+  (Functor s, Mergeable1 s, Mergeable x, Monad m, MonadUnion m') =>
+  (forall y. m y -> m' y) ->
+  Coroutine s m x ->
+  Coroutine s m' x
+mrgMapMonad f (Coroutine r) =
+  Coroutine
+    { resume =
+        f r >>= \x ->
+          mergeWithStrategy
+            coroEitherMergingStrategy
+            $ return
+            $ map' x
+    }
+  where
+    map' :: Either (s (Coroutine s m x)) x -> Either (s (Coroutine s m' x)) x
+    map' (Right r1) = Right r1
+    map' (Left s) = Left $ mrgMapMonad f <$> s
+{-# INLINEABLE mrgMapMonad #-}
+
+-- | Symbolic version of 'Control.Monad.Coroutine.mapSuspension',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgMapSuspension ::
+  forall s m x s'.
+  (Functor s, MonadUnion m, Mergeable x, Mergeable1 s') =>
+  (forall y. s y -> s' y) ->
+  Coroutine s m x ->
+  Coroutine s' m x
+mrgMapSuspension f (Coroutine r) =
+  Coroutine
+    { resume =
+        r >>= \x ->
+          mergeWithStrategy coroEitherMergingStrategy $ return $ map' x
+    }
+  where
+    map' :: Either (s (Coroutine s m x)) x -> Either (s' (Coroutine s' m x)) x
+    map' (Right r1) = Right r1
+    map' (Left s) = Left $ f $ mrgMapSuspension f <$> s
+{-# INLINEABLE mrgMapSuspension #-}
+
+-- | Symbolic version of 'Control.Monad.Coroutine.mapFirstSuspension',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgMapFirstSuspension ::
+  forall s m x.
+  (Functor s, Mergeable1 s, MonadUnion m, Mergeable x) =>
+  (forall y. s y -> s y) ->
+  Coroutine s m x ->
+  Coroutine s m x
+mrgMapFirstSuspension f (Coroutine r) =
+  Coroutine
+    { resume =
+        r >>= \s -> mrgReturnWithStrategy coroEitherMergingStrategy $
+          case s of
+            Right x -> Right x
+            Left x -> Left $ f x
+    }
+
+instance Mergeable (Naught x) where
+  rootStrategy = SimpleStrategy mrgIte
+
+instance Mergeable1 Naught where
+  liftRootStrategy _ = SimpleStrategy mrgIte
+
+instance SimpleMergeable (Naught x) where
+  mrgIte _ x _ = x
+
+instance SimpleMergeable1 Naught where
+  liftMrgIte _ _ x _ = x
+
+-- | Symbolic version of 'Control.Monad.Coroutine.mapFirstSuspension',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgRunCoroutine ::
+  (MonadUnion m, Mergeable x) =>
+  Coroutine Naught m x ->
+  m x
+mrgRunCoroutine (Coroutine r) = do
+  v <- r
+  case v of
+    Left _ -> error "Won't happen"
+    Right x -> mrgReturn x
+
+-- | Symbolic version of 'Control.Monad.Coroutine.bounce',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgBounce ::
+  (Functor s, Mergeable1 s, MonadUnion m, Mergeable x) =>
+  (s (Coroutine s m x) -> Coroutine s m x) ->
+  Coroutine s m x ->
+  Coroutine s m x
+mrgBounce f (Coroutine r) = Coroutine $ mergeWithStrategy coroEitherMergingStrategy $ do
+  r1 <- r
+  case r1 of
+    Left s -> resume $ f s
+    Right x -> return $ Right x
+
+-- | Symbolic version of 'Control.Monad.Coroutine.pogoStick',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgPogoStick ::
+  (MonadUnion m, Mergeable x) =>
+  (s (Coroutine s m x) -> Coroutine s m x) ->
+  Coroutine s m x ->
+  m x
+mrgPogoStick f (Coroutine r) = do
+  r1 <- r
+  case r1 of
+    Left h -> mrgPogoStick f $ f h
+    Right v -> mrgReturn v
+
+-- | Symbolic version of 'Control.Monad.Coroutine.pogoStickM',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgPogoStickM ::
+  (MonadUnion m, Mergeable x) =>
+  (s (Coroutine s m x) -> m (Coroutine s m x)) ->
+  Coroutine s m x ->
+  m x
+mrgPogoStickM f (Coroutine r) = do
+  r1 <- r
+  case r1 of
+    Left h -> do
+      cs <- f h
+      mrgPogoStickM f cs
+    Right v -> mrgReturn v
+
+-- | Symbolic version of 'Control.Monad.Coroutine.foldRun',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgFoldRun ::
+  (MonadUnion m, Mergeable x, Mergeable a) =>
+  (a -> s (Coroutine s m x) -> (a, Coroutine s m x)) ->
+  a ->
+  Coroutine s m x ->
+  m (a, x)
+mrgFoldRun f a (Coroutine r) = do
+  r1 <- r
+  case r1 of
+    Left s -> case f a s of
+      (a1, c1) -> mrgFoldRun f a1 c1
+    Right v -> mrgReturn (a, v)
+
+-- | Type of functions that can bind two monadic values together, used to
+-- combine two coroutines' step results. The result type needs to be mergeable.
+type MrgPairBinder bool m =
+  forall x y r. (Mergeable r) => (x -> y -> m r) -> m x -> m y -> m r
+
+-- | Symbolic version of 'Control.Monad.Coroutine.sequentialBinder',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgSequentialBinder :: (MonadUnion m) => MrgPairBinder bool m
+mrgSequentialBinder f ma mb = merge $ do
+  a <- ma
+  b <- mb
+  f a b
diff --git a/src/Grisette/Lib/Control/Monad/Coroutine/SuspensionFunctors.hs b/src/Grisette/Lib/Control/Monad/Coroutine/SuspensionFunctors.hs
new file mode 100644
--- /dev/null
+++ b/src/Grisette/Lib/Control/Monad/Coroutine/SuspensionFunctors.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+-- |
+-- Module      :   Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctors
+-- Copyright   :   (c) Sirui Lu 2021-2023
+-- License     :   BSD-3-Clause (see the LICENSE file)
+--
+-- Maintainer  :   siruilu@cs.washington.edu
+-- Stability   :   Experimental
+-- Portability :   GHC only
+module Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctors
+  ( mrgYield,
+    mrgAwait,
+    mrgRequest,
+  )
+where
+
+import Control.Monad.Coroutine
+import Control.Monad.Coroutine.SuspensionFunctors
+import Grisette.Core
+import Grisette.Lib.Control.Monad
+import Grisette.Lib.Control.Monad.Coroutine
+
+instance (Mergeable x, Mergeable y) => Mergeable (Yield x y) where
+  rootStrategy = product2Strategy Yield (\(Yield x y) -> (x, y)) rootStrategy rootStrategy
+
+instance (Mergeable x) => Mergeable1 (Yield x) where
+  liftRootStrategy = product2Strategy Yield (\(Yield x y) -> (x, y)) rootStrategy
+
+instance (Mergeable x, Mergeable y) => Mergeable (Await x y) where
+  rootStrategy = wrapStrategy rootStrategy Await (\(Await x) -> x)
+
+instance (Mergeable x) => Mergeable1 (Await x) where
+  liftRootStrategy m = wrapStrategy (liftRootStrategy m) Await (\(Await x) -> x)
+
+instance
+  (Mergeable req, Mergeable res, Mergeable x) =>
+  Mergeable (Request req res x)
+  where
+  rootStrategy = product2Strategy Request (\(Request x y) -> (x, y)) rootStrategy rootStrategy
+
+instance (Mergeable req, Mergeable res) => Mergeable1 (Request req res) where
+  liftRootStrategy m = product2Strategy Request (\(Request x y) -> (x, y)) rootStrategy (liftRootStrategy m)
+
+-- | Symbolic version of 'Control.Monad.Coroutine.SuspensionFunctors.yield',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgYield :: (MonadUnion m, Mergeable x) => x -> Coroutine (Yield x) m ()
+mrgYield x = mrgSuspend (Yield x $ mrgReturn ())
+{-# INLINEABLE mrgYield #-}
+
+-- | Symbolic version of 'Control.Monad.Coroutine.SuspensionFunctors.await',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgAwait :: (MonadUnion m, Mergeable x) => Coroutine (Await x) m x
+mrgAwait = mrgSuspend (Await mrgReturn)
+{-# INLINEABLE mrgAwait #-}
+
+-- | Symbolic version of 'Control.Monad.Coroutine.SuspensionFunctors.request',
+-- the result would be merged and propagate the mergeable knowledge.
+mrgRequest :: (MonadUnion m, Mergeable x, Mergeable y) => x -> Coroutine (Request x y) m y
+mrgRequest x = mrgSuspend (Request x mrgReturn)
+{-# INLINEABLE mrgRequest #-}
diff --git a/src/Grisette/Lib/MonadCoroutine.hs b/src/Grisette/Lib/MonadCoroutine.hs
new file mode 100644
--- /dev/null
+++ b/src/Grisette/Lib/MonadCoroutine.hs
@@ -0,0 +1,16 @@
+-- |
+-- Module      :   Grisette.Lib.MonadCoroutine
+-- Copyright   :   (c) Sirui Lu 2021-2023
+-- License     :   BSD-3-Clause (see the LICENSE file)
+--
+-- Maintainer  :   siruilu@cs.washington.edu
+-- Stability   :   Experimental
+-- Portability :   GHC only
+module Grisette.Lib.MonadCoroutine
+  ( module Grisette.Lib.Control.Monad.Coroutine,
+    module Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctors,
+  )
+where
+
+import Grisette.Lib.Control.Monad.Coroutine
+import Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctors
diff --git a/test/Grisette/Lib/Control/Monad/Coroutine/SuspensionFunctorsTests.hs b/test/Grisette/Lib/Control/Monad/Coroutine/SuspensionFunctorsTests.hs
new file mode 100644
--- /dev/null
+++ b/test/Grisette/Lib/Control/Monad/Coroutine/SuspensionFunctorsTests.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
+
+module Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctorsTests where
+
+import Control.Monad.Coroutine.SuspensionFunctors
+import Grisette
+import Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctors ()
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck
+
+testMergeableSimpleEquivClass ::
+  (HasCallStack, Mergeable x, Show x, Eq x) => x -> [DynamicSortedIdx] -> [(SymBool, x, x, x)] -> Assertion
+testMergeableSimpleEquivClass x idxs cases = do
+  let (idxsT, s) = resolveStrategy rootStrategy x
+  case s of
+    SimpleStrategy m -> do
+      idxsT @=? idxs
+      go cases
+      where
+        go [] = return ()
+        go ((c, t, f, r) : xs) = do
+          fst (resolveStrategy rootStrategy t) @=? idxs
+          fst (resolveStrategy rootStrategy f) @=? idxs
+          fst (resolveStrategy rootStrategy r) @=? idxs
+          m c t f @=? r
+          go xs
+    _ -> assertFailure $ "Bad strategy type for " ++ show x
+
+testMergeableSimpleEquivClass' ::
+  (HasCallStack, Mergeable x, Show y, Eq y) => (x -> y) -> x -> [DynamicSortedIdx] -> [(SymBool, x, x, x)] -> Assertion
+testMergeableSimpleEquivClass' vis x idxs cases = do
+  let (idxsT, s) = resolveStrategy rootStrategy x
+  case s of
+    SimpleStrategy m -> do
+      idxsT @=? idxs
+      go cases
+      where
+        go [] = return ()
+        go ((c, t, f, r) : xs) = do
+          fst (resolveStrategy rootStrategy t) @=? idxs
+          fst (resolveStrategy rootStrategy f) @=? idxs
+          fst (resolveStrategy rootStrategy r) @=? idxs
+          vis (m c t f) @=? vis r
+          go xs
+    _ -> assertFailure $ "Bad strategy type for " ++ show (vis x)
+
+suspensionFunctorsTests :: TestTree
+suspensionFunctorsTests =
+  testGroup
+    "SuspensionFunctorsSpec"
+    [ testGroup
+        "Mergeable for suspension functors"
+        $ let visYield (Yield a b) = (a, b)
+           in [ testProperty "Yield Integer Integer" $
+                  ioProperty . \(x :: Integer, y :: Integer) -> do
+                    let (idxs, SimpleStrategy s) = resolveStrategy rootStrategy (Yield x y)
+                    idxs @=? [DynamicSortedIdx x, DynamicSortedIdx y]
+                    visYield (s "a" (Yield x y) (Yield x y)) @=? visYield (Yield x y),
+                testCase "Yield SymBool SymBool" $ do
+                  testMergeableSimpleEquivClass'
+                    (\(Yield a b) -> (a, b))
+                    (Yield "a" "b" :: Yield SymBool SymBool)
+                    []
+                    [ ( "a",
+                        Yield "b" "c",
+                        Yield "d" "e",
+                        Yield (ites "a" "b" "d") (ites "a" "c" "e")
+                      )
+                    ],
+                testCase "Await SymBool SymBool" $ do
+                  let SimpleStrategy s = rootStrategy :: MergingStrategy (Await SymBool SymBool)
+                  let a1 = Await nots
+                  let a2 = Await ("a" &&~)
+                  let Await a3 = s "b" a1 a2
+                  a3 "c" @=? ites "b" (nots "c") ("a" &&~ "c"),
+                testCase "Request SymBool SymBool SymBool" $ do
+                  let SimpleStrategy s = rootStrategy :: MergingStrategy (Request SymBool SymBool SymBool)
+                  let a1 = Request "a" nots
+                  let a2 = Request "b" ("c" &&~)
+                  let Request v3 a3 = s "d" a1 a2
+                  v3 @=? ites "d" "a" "b"
+                  a3 "e" @=? ites "d" (nots "e") ("c" &&~ "e")
+              ]
+    ]
diff --git a/test/Grisette/Lib/Control/Monad/CoroutineTests.hs b/test/Grisette/Lib/Control/Monad/CoroutineTests.hs
new file mode 100644
--- /dev/null
+++ b/test/Grisette/Lib/Control/Monad/CoroutineTests.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
+
+module Grisette.Lib.Control.Monad.CoroutineTests where
+
+import Control.Monad.Coroutine hiding (merge)
+import Control.Monad.Coroutine.SuspensionFunctors
+import Grisette
+import Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctors ()
+import Test.Tasty
+import Test.Tasty.HUnit
+
+coroutineTests :: TestTree
+coroutineTests =
+  testGroup
+    "CoroutineTests"
+    [ testGroup
+        "MonadUnion for Coroutine"
+        [ testCase "merge" $ do
+            let Coroutine v =
+                  merge
+                    ( Coroutine $
+                        unionIf
+                          "a"
+                          (single $ Left $ Yield "b" $ Coroutine $ single $ Right "c")
+                          (single $ Left $ Yield "d" $ Coroutine $ single $ Right "e") ::
+                        Coroutine (Yield SymBool) UnionM SymBool
+                    )
+            case v of
+              SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
+                x @=? ites "a" "b" "d"
+                y @=? ites "a" "c" "e"
+              _ -> assertFailure "Failed to merge Coroutine",
+          testCase "mrgReturn" $ do
+            case (mrgReturn 1 :: Coroutine (Yield SymBool) UnionM Integer) of
+              Coroutine (SingleU (Right 1)) -> return ()
+              _ -> assertFailure "mrgReturn for Coroutine is not working",
+          testCase "mrgIf" $ do
+            let Coroutine v =
+                  mrgIf
+                    "a"
+                    (Coroutine $ single $ Left $ Yield "b" $ Coroutine $ single $ Right "c")
+                    (Coroutine $ single $ Left $ Yield "d" $ Coroutine $ single $ Right "e") ::
+                    Coroutine (Yield SymBool) UnionM SymBool
+            case v of
+              SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
+                x @=? ites "a" "b" "d"
+                y @=? ites "a" "c" "e"
+              _ -> assertFailure "Failed to merge Coroutine"
+        ],
+      testCase "Mergeable for Coroutine" $ do
+        let SimpleStrategy s = rootStrategy :: MergingStrategy (Coroutine (Yield SymBool) UnionM SymBool)
+        let a1 :: Coroutine (Yield SymBool) UnionM SymBool =
+              Coroutine (mrgReturn (Left (Yield "a" (Coroutine (mrgReturn (Right "b"))))))
+        let a2 :: Coroutine (Yield SymBool) UnionM SymBool =
+              Coroutine (mrgReturn (Left (Yield "c" (Coroutine (mrgReturn (Right "d"))))))
+        let Coroutine r = s "e" a1 a2
+        case r of
+          SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
+            x @=? ites "e" "a" "c"
+            y @=? ites "e" "b" "d"
+          _ -> assertFailure "Bad shape",
+      testCase "SimpleMergeable for Coroutine" $ do
+        let a1 :: Coroutine (Yield SymBool) UnionM SymBool =
+              Coroutine (mrgReturn (Left (Yield "a" (Coroutine (mrgReturn (Right "b"))))))
+        let a2 :: Coroutine (Yield SymBool) UnionM SymBool =
+              Coroutine (mrgReturn (Left (Yield "c" (Coroutine (mrgReturn (Right "d"))))))
+        let Coroutine r = mrgIte "e" a1 a2
+        let Coroutine r1 = mrgIte1 "e" a1 a2
+        let Coroutine ru1 = mrgIf "e" a1 a2
+        case r of
+          SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
+            x @=? ites "e" "a" "c"
+            y @=? ites "e" "b" "d"
+          _ -> assertFailure "Bad shape"
+        case r1 of
+          SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
+            x @=? ites "e" "a" "c"
+            y @=? ites "e" "b" "d"
+          _ -> assertFailure "Bad shape"
+        case ru1 of
+          SingleU (Left (Yield x (Coroutine (SingleU (Right y))))) -> do
+            x @=? ites "e" "a" "c"
+            y @=? ites "e" "b" "d"
+          _ -> assertFailure "Bad shape"
+    ]
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,24 @@
+module Main where
+
+import Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctorsTests
+import Grisette.Lib.Control.Monad.CoroutineTests
+import Test.Tasty
+import Test.Tasty.Ingredients
+import qualified Test.Tasty.Ingredients.ConsoleReporter as ConsoleReporter
+import qualified Test.Tasty.Runners.Reporter as Reporter
+
+main :: IO ()
+main = defaultMainWithIngredients [composeReporters Reporter.ingredient ConsoleReporter.consoleTestReporter] tests
+
+tests :: TestTree
+tests =
+  testGroup
+    "grisette-monad-coroutine"
+    [ testGroup
+        "Grisette.Lib.Control.Monad"
+        [ testGroup
+            "Coroutine"
+            [suspensionFunctorsTests],
+          coroutineTests
+        ]
+    ]