diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,4 +1,19 @@
 
+# 0.8.1
+
+20230410
+
+Thank you to Skyfold (Martin P.)
+
+- Generalized KnownVal instances
+- Initialized the HSpec use and test directory organization
+- Added flake definitions
+- Updated stack version (not tested with stack)
+- Removed shell.nix
+- Fcf.Data.Set doctests removed and replaced with Test.Data.Set
+- Fcf.Alg.List doctests removed and replaced with Test.Alg.List
+
+
 # 0.8.0
 
 20230226
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -64,6 +64,10 @@
 
 ## Example
 
+The  
+[test directory](https://github.com/gspia/fcf-containers/blob/master/test)
+contains a lot of useful examples.
+
 See [Orbits.hs](https://github.com/gspia/fcf-containers/blob/master/examples/Orbits.hs). 
 It shows how to solve a real problem,
 what PRAGMAs are probably needed etc.
@@ -174,6 +178,7 @@
 
 Source also contains a lot of examples, see
 [fcf-containers](https://github.com/gspia/fcf-containers/tree/master/src/Fcf).
-
+The examples will be left near the code, even thou the doctest runs will be 
+removed and replaced with real tests at the test-directory.
 
 Happy :kinding!
diff --git a/fcf-containers.cabal b/fcf-containers.cabal
--- a/fcf-containers.cabal
+++ b/fcf-containers.cabal
@@ -7,7 +7,7 @@
     contents of containers-package and show how these can be used. Everything is
     based on the ideas given in the first-class-families -package.
 Homepage:            https://github.com/gspia/fcf-containers
-Version:             0.8.0
+Version:             0.8.1
 Build-type:          Simple
 Author:              gspia
 Maintainer:          iahogsp@gmail.com
@@ -15,7 +15,7 @@
 License-file:        LICENSE
 Category:            Other
 Copyright:           gspia (c) 2020-
-Extra-source-files:  README.md, TODO.md, CHANGELOG.md, default.nix, shell.nix
+Extra-source-files:  README.md, TODO.md, CHANGELOG.md, default.nix, flake.nix, flake.lock
 Tested-With:         GHC ==9.2.4 || ==9.0.2 || ==8.10.7
 
 
@@ -47,7 +47,6 @@
                    , containers
                    , first-class-families >= 0.8 && < 0.9
                    , ghc-prim
-                   , mtl
                    , text
   ghc-options:      -Wall
   default-language:  Haskell2010
@@ -95,12 +94,18 @@
   hs-source-dirs:      test
   main-is:             test.hs
   default-language:    Haskell2010
-  other-modules:       Test.Data
+  other-modules:       Test.Alg
+                     , Test.Alg.List
+                     , Test.Data
                      , Test.Data.Reflect
+                     , Test.Data.Set
+                     , Test.Control
+                     , Test.Control.Monad
   build-depends:
       base
     , first-class-families
     , fcf-containers
+    , hspec
     , containers
     , text
 
diff --git a/flake.lock b/flake.lock
new file mode 100644
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,44 @@
+{
+  "nodes": {
+    "nix-filter": {
+      "locked": {
+        "lastModified": 1666547822,
+        "narHash": "sha256-razwnAybPHyoAyhkKCwXdxihIqJi1G6e1XP4FQOJTEs=",
+        "owner": "numtide",
+        "repo": "nix-filter",
+        "rev": "1a3b735e13e90a8d2fd5629f2f8363bd7ffbbec7",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "ref": "master",
+        "repo": "nix-filter",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1674990008,
+        "narHash": "sha256-4zOyp+hFW2Y7imxIpZqZGT8CEqKmDjwgfD6BzRUE0mQ=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "d2bbcbe6c626d339b25a4995711f07625b508214",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixpkgs-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nix-filter": "nix-filter",
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,69 @@
+{
+  description = "Data structures and algorithms for first-class-families";
+
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
+    nix-filter.url = "github:numtide/nix-filter/master";
+  };
+
+  outputs = { self, nixpkgs, nix-filter }: 
+    let
+      pkgs = import nixpkgs { system = "x86_64-linux"; };
+
+      # filter = import nix-filter { };
+
+      ghcVersion = "925";
+
+      src = nix-filter.lib {
+        root = ./.;
+        include = [
+          (nix-filter.lib.inDirectory "src")
+          (nix-filter.lib.inDirectory "examples")
+          (nix-filter.lib.inDirectory "test")
+          (nix-filter.lib.matchExt "hs")
+          ./fcf-containers.cabal
+          ./cabal.project
+          ./LICENSE
+        ];
+      };
+
+      fcf-containers = hself: hself.callCabal2nix "fcf-containers" src {};
+
+      myHaskellPackages = pkgs.haskell.packages."ghc${ghcVersion}".override {
+        overrides = hself: hsuper: {
+          # fcf-containers = hself.callCabal2nix "fcf-containers" sources.fcf-containers {};
+          # fcf-containers = (import sources.fcf-containers {});
+          fcf-containers = fcf-containers hself;
+          # ListLike = pkgs.haskell.lib.dontCheck hsuper.ListLike;
+          # type-of-html = pkgs.haskell.lib.doBenchmark (hself.callPackage ./nix/type-of-html.nix {inherit src;});
+          # type-of-html = hself.callCabal2nix "type-of-html" src {};
+          # optics-core = hsuper.optics-core.overrideAttrs(old: {
+          #   configureFlags = "-f explicit-generic-labels";
+          #   patches = [./optics-core.patch];
+          # });
+        };
+      };
+
+      shell = myHaskellPackages.shellFor {
+        packages = p: [
+          p.fcf-containers
+        ];
+        buildInputs = with pkgs.haskell.packages."ghc${ghcVersion}"; [
+          myHaskellPackages.cabal-install
+          ghcid
+          (pkgs.haskell-language-server.override { supportedGhcVersions = [ "${ghcVersion}" ]; })
+          hlint
+          # implicit-hie
+          # cabal2nix
+        ];
+        withHoogle = true;
+        doBenchmark = true;
+      };
+
+    in
+      {
+        library = fcf-containers;
+        # packages.x86_64-linux.default = ;
+        devShell.x86_64-linux = shell;
+      };
+}
diff --git a/shell.nix b/shell.nix
deleted file mode 100644
--- a/shell.nix
+++ /dev/null
@@ -1,9 +0,0 @@
-{ nixpkgs ? import <nixpkgs> {}
-/* , compiler ? "ghc822" */
-} : 
-let
-  inherit (nixpkgs) pkgs;
-  /* drv = import ./. { inherit compiler; }; */
-  drv = import ./. { };
-in
-if pkgs.lib.inNixShell then drv.env else drv
diff --git a/src/Fcf/Alg/List.hs b/src/Fcf/Alg/List.hs
--- a/src/Fcf/Alg/List.hs
+++ b/src/Fcf/Alg/List.hs
@@ -19,6 +19,8 @@
 This module also contains other list-related functions (that might move to
 other place some day).
 
+To see examples, please do take a look of the respective test module.
+
 -}
 
 --------------------------------------------------------------------------------
@@ -39,13 +41,6 @@
 
 --------------------------------------------------------------------------------
 
--- For the doctests:
-
--- $setup
--- >>> import           Fcf.Combinators
-
---------------------------------------------------------------------------------
-
 -- | Base functor for a list of type @[a]@.
 data ListF a b = ConsF a b | NilF
 
@@ -65,7 +60,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (ListToFix '[1,2,3])
+-- > :kind! Eval (ListToFix '[1,2,3])
 -- Eval (ListToFix '[1,2,3]) :: Fix (ListF TL.Natural)
 -- = 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF))))))
 data ListToFix :: [a] -> Exp (Fix (ListF a))
@@ -76,7 +71,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])
+-- > :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])
 -- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: TL.Natural
 -- = 3
 data LenAlg :: Algebra (ListF a) Nat
@@ -87,7 +82,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])
+-- > :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])
 -- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural
 -- = 10
 data SumAlg :: Algebra (ListF Nat) Nat
@@ -98,7 +93,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])
+-- > :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])
 -- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural
 -- = 24
 data ProdAlg :: Algebra (ListF Nat) Nat
@@ -111,7 +106,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (ListToParaFix '[1,2,3])
+-- > :kind! Eval (ListToParaFix '[1,2,3])
 -- Eval (ListToParaFix '[1,2,3]) :: Fix
 --                                    (ListF (TL.Natural, [TL.Natural]))
 -- = 'Fix
@@ -129,7 +124,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])
+-- > :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])
 -- Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2]) :: [TL.Natural]
 -- = '[5, 1, 3, 2]
 data DedupAlg :: RAlgebra (ListF (a,[a])) [a]
@@ -145,7 +140,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Sliding 3 '[1,2,3,4,5,6])
+-- > :kind! Eval (Sliding 3 '[1,2,3,4,5,6])
 -- Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[TL.Natural]]
 -- = '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]]
 data Sliding :: Nat -> [a] -> Exp [[a]]
@@ -177,7 +172,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Evens =<< RunInc 8)
+-- > :kind! Eval (Evens =<< RunInc 8)
 -- Eval (Evens =<< RunInc 8) :: [TL.Natural]
 -- = '[2, 4, 6, 8]
 data Evens :: [a] -> Exp [a]
@@ -199,7 +194,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (RunInc 8)
+-- > :kind! Eval (RunInc 8)
 -- Eval (RunInc 8) :: [TL.Natural]
 -- = '[1, 2, 3, 4, 5, 6, 7, 8]
 data RunInc :: Nat -> Exp [Nat]
@@ -212,7 +207,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Sum '[1,2,3])
+-- > :kind! Eval (Sum '[1,2,3])
 -- Eval (Sum '[1,2,3]) :: TL.Natural
 -- = 6
 data Sum :: [Nat] -> Exp Nat
@@ -233,7 +228,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (MToN 1 3)
+-- > :kind! Eval (MToN 1 3)
 -- Eval (MToN 1 3) :: [TL.Natural]
 -- = '[1, 2, 3]
 data MToN :: Nat -> Nat -> Exp [Nat]
@@ -245,7 +240,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (ToList 1)
+-- > :kind! Eval (ToList 1)
 -- Eval (ToList 1) :: [TL.Natural]
 -- = '[1]
 data ToList :: a -> Exp [a]
@@ -256,13 +251,12 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Equal '[1,2,3] '[1,2,3])
+-- > :kind! Eval (Equal '[1,2,3] '[1,2,3])
 -- Eval (Equal '[1,2,3] '[1,2,3]) :: Bool
 -- = 'True
 --
--- >>> :kind! Eval (Equal '[1,2,3] '[1,3,2])
+-- > :kind! Eval (Equal '[1,2,3] '[1,3,2])
 -- Eval (Equal '[1,2,3] '[1,3,2]) :: Bool
 -- = 'False
 data Equal :: [a] -> [a] -> Exp Bool
 type instance Eval (Equal as bs) = Eval (And =<< ZipWith TyEq as bs)
-
diff --git a/src/Fcf/Control/Monad.hs b/src/Fcf/Control/Monad.hs
--- a/src/Fcf/Control/Monad.hs
+++ b/src/Fcf/Control/Monad.hs
@@ -22,10 +22,12 @@
 
 module Fcf.Control.Monad where
 
-import           Control.Monad.Identity
+import           Data.Functor.Identity
 import           GHC.TypeNats as TN
 
 import           Fcf hiding (type (<*>))
+import           Fcf.Class.Monoid (type (<>), MEmpty)
+import           Fcf.Data.Tuple
 
 --------------------------------------------------------------------------------
 
@@ -40,8 +42,6 @@
 
 type instance Eval (Map f ('Identity a)) = 'Identity (Eval (f a))
 
-
-
 --------------------------------------------------------------------------------
 -- Common methods for both Applicative and Monad
 
@@ -57,6 +57,9 @@
 type instance Eval (Return a) = 'Just a
 type instance Eval (Return a) = 'Right a
 type instance Eval (Return a) = 'Identity a
+type instance Eval (Return a) = '(MEmpty, a)
+type instance Eval (Return a) = '(MEmpty, MEmpty, a)
+type instance Eval (Return a) = '(MEmpty, MEmpty, MEmpty, a)
 
 
 --------------------------------------------------------------------------------
@@ -71,6 +74,9 @@
 --  - []
 --  - Maybe
 --  - Either
+--  - (,)
+--  - (,,)
+--  - (,,,)
 --
 -- === __Example__
 --
@@ -98,29 +104,29 @@
 type instance Eval ((f ': fs) <*> (a ': as)) =
     Eval ((++) (Eval (Star_ f (a ': as))) (Eval ((<*>) fs (a ':as))))
 
--- | Helper for the [] applicative instance.
-data Star_ :: (a -> Exp b) -> f a -> Exp (f b)
-type instance Eval (Star_ _ '[]) = '[]
-type instance Eval (Star_ f (a ': as)) = Eval (f a) ': Eval (Star_ f as)
-
-
--- Example
-data Plus1 :: Nat -> Exp Nat
-type instance Eval (Plus1 n) = n TN.+ 1
-
--- Example
-data Plus2 :: Nat -> Exp Nat
-type instance Eval (Plus2 n) = n TN.+ 2
-
-
+-- Maybe
 type instance Eval ('Nothing <*> _) = 'Nothing
 type instance Eval ('Just f <*> m) = Eval (Map f m)
 
-
+-- Either
 type instance Eval ('Left e <*> _) = 'Left e
 type instance Eval ('Right f <*> m) = Eval (Map f m)
 
+-- | For tuples, the 'Monoid' constraint determines how the first values merge.
+-- For example, 'Symbol's concatenate:
+--
+-- >>> :kind! Eval ('("hello", (Fcf.+) 15) <*> '("world!", 2002))
+-- Eval ('("hello", (Fcf.+) 15) <*> '("world!", 2002)) :: (TL.Symbol,
+--                                                         Natural)
+-- = '("helloworld!", 2017)
+type instance Eval ('(u, f) <*> '(v, x)) = '(u <> v, Eval (f x))
 
+-- ((,,) a b)
+type instance Eval ('(a, b, f) <*> '(a', b', x)) = '(a <> a', b <> b', Eval (f x))
+
+-- ((,,,) a b)
+type instance Eval ('(a, b, c, f) <*> '(a', b', c', x)) = '(a <> a', b <> b', c <> c', Eval (f x))
+
 -- | Type level LiftA2.
 --
 -- === __Example__
@@ -131,31 +137,33 @@
 --
 --
 data LiftA2 :: (a -> b -> Exp c) -> f a -> f b -> Exp (f c)
--- Could a single default implementation work here? Looks like it would need
--- a function that turns (a -> b -> c) to (b -> c).
--- E.g. something like:
--- type instance Eval (LiftA2 f fa fb) = Eval ( (<*>) (Map (f fa)) fb)
-
-type instance Eval (LiftA2 f 'Nothing _) = 'Nothing
-type instance Eval (LiftA2 f _ 'Nothing) = 'Nothing
-type instance Eval (LiftA2 f ('Just a) ('Just b)) = 'Just (Eval (f a b))
-
-type instance Eval (LiftA2 f ('Left e) _) = 'Left e
-type instance Eval (LiftA2 f ('Right _) ('Left e)) = 'Left e
-type instance Eval (LiftA2 f ('Right a) ('Right b)) = 'Right (Eval (f a b))
-
+type instance Eval (LiftA2 f fa fb) = Eval (Eval (Map (App2 f) fa) <*> fb)
 
-type instance Eval (LiftA2 f '[] _) = '[]
-type instance Eval (LiftA2 f (a ': as) '[]) = '[]
-type instance Eval (LiftA2 f (a ': as) (b ':bs)) =
-    Eval ((++) (Eval (LiftA2_ f a (b ': bs))) (Eval (LiftA2 f as (b ':bs))))
+-- | Type level LiftA3.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (LiftA3 Tuple3 '[1,2] '[3,4] '[5,6])
+-- Eval (LiftA3 Tuple3 '[1,2] '[3,4] '[5,6]) :: [(Natural, Natural,
+--                                                Natural)]
+-- = '[ '(1, 3, 5), '(1, 3, 6), '(1, 4, 5), '(1, 4, 6), '(2, 3, 5),
+--      '(2, 3, 6), '(2, 4, 5), '(2, 4, 6)]
+--
+-- >>> :kind! Eval (LiftA3 Tuple3 ('Right 5) ('Right 6) ('Left "fail"))
+-- Eval (LiftA3 Tuple3 ('Right 5) ('Right 6) ('Left "fail")) :: Either
+--                                                                TL.Symbol (Natural, Natural, c)
+-- = 'Left "fail"
+--
+data LiftA3 :: (a -> b -> c -> Exp d) -> f a -> f b -> f c -> Exp (f d)
+type instance Eval (LiftA3 f fa fb fc) = Eval (Eval (Eval (Map (App3 f) fa) <*> fb) <*> fc)
 
--- Helper for list LiftA2 instance.
-data LiftA2_ :: (a -> b -> Exp c) -> a -> f b -> Exp (f c)
-type instance Eval (LiftA2_ f a '[]) = '[]
-type instance Eval (LiftA2_ f a (b ': bs)) =
-    Eval (f a b) ': Eval (LiftA2_ f a bs)
+-- | Type level LiftA4.
+data LiftA4 :: (a -> b -> c -> d -> Exp e) -> f a -> f b -> f c -> f d -> Exp (f e)
+type instance Eval (LiftA4 f fa fb fc fd) = Eval (Eval (Eval (Eval (Map (App4 f) fa) <*> fb) <*> fc) <*> fd)
 
+-- | Type level LiftA5.
+data LiftA5 :: (a -> b -> c -> d -> e -> Exp g) -> f a -> f b -> f c -> f d -> f e -> Exp (f g)
+type instance Eval (LiftA5 f fa fb fc fd fe) = Eval (Eval (Eval (Eval (Eval (Map (App5 f) fa) <*> fb) <*> fc) <*> fd) <*> fe)
 
 --------------------------------------------------------------------------------
 -- Monad
@@ -171,6 +179,9 @@
 --  - []
 --  - Maybe
 --  - Either
+--  - (,)
+--  - (,,)
+--  - (,,,)
 --
 -- === __Example__
 --
@@ -202,45 +213,16 @@
 type instance Eval ('[] >>= _) = '[]
 type instance Eval ((x ': xs) >>= f) = Eval ((f @@ x) ++  Eval (xs >>= f))
 
-
--- For the example. Turn an input number to list of two numbers of a bit
--- larger numbers.
-data Plus2M :: Nat -> Exp [Nat]
-type instance Eval (Plus2M n) = '[n TN.+ 2, n TN.+3]
-
--- Part of an example
-data PureXPlusY :: Nat -> Nat -> Exp [Nat]
-type instance Eval (PureXPlusY x y) = Eval (Return ((TN.+) x y))
-
--- Part of an example
-data XPlusYs :: Nat -> [Nat] -> Exp [Nat]
-type instance Eval (XPlusYs x ys) = Eval (ys >>= PureXPlusY x)
-
--- | An example implementing
---
--- sumM xs ys = do
---     x <- xs
---     y <- ys
---     return (x + y)
---
--- or
---
--- sumM xs ys = xs >>= (\x -> ys >>= (\y -> pure (x+y)))
---
--- Note the use of helper functions. This is a bit awkward, a type level
--- lambda would be nice.
-data XsPlusYsMonadic :: [Nat] -> [Nat] -> Exp [Nat]
-type instance Eval (XsPlusYsMonadic xs ys) = Eval (xs >>= Flip XPlusYs ys)
-
-
-
+-- (,)
+type instance Eval ('(u, a) >>= k) = Eval ('(u, Id) <*> Eval (k a))
 
--- data Sumnd :: [Nat] -> [Nat] -> Exp [Nat]
--- type instance Eval (Sumnd xs ys) = xs >>=
+-- (,,)
+type instance Eval ('(u, v, a) >>= k) = Eval ('(u, v, Id) <*> Eval (k a))
 
--- data Sum2 :: Nat -> Nat -> Exp Nat
--- type instance Eval (Sum2 x y) = x TN.+ y
+-- (,,,)
+type instance Eval ('(u, v, w, a) >>= k) = Eval ('(u, v, w, Id) <*> Eval (k a))
 
+-- | Type level >> 
 --
 -- === __Example__
 --
@@ -252,21 +234,8 @@
 -- Eval ( 'Nothing >> 'Just 2) :: Maybe Natural
 -- = 'Nothing
 --
---
 data (>>) :: m a -> m b -> Exp (m b)
-
--- Maybe
-type instance Eval ('Nothing >> b) = 'Nothing
-type instance Eval ('Just a >> b) = b
-
--- Either
-type instance Eval ('Left a >> _) = 'Left a
-type instance Eval ('Right _ >> b) = b
-
--- Lists
--- TODO, are the instances ok?
-type instance Eval ('[] >> _) = '[]
-type instance Eval ((x ': xs) >> b) = b
+type instance Eval (m >> k) = Eval (m >>= ConstFn k)
 
 --------------------------------------------------------------------------------
 -- MapM
@@ -314,10 +283,6 @@
 data FoldlM :: (b -> a -> Exp (m b)) -> b -> t a -> Exp (m b)
 type instance Eval (FoldlM f z0 xs) = Eval ((Eval (Foldr (FoldlMHelper f) Return xs)) z0)
 
--- | Helper for 'FoldlM'
-data FoldlMHelper :: (b -> a -> Exp (m b)) -> a -> (b -> Exp (m b)) -> Exp (b -> Exp (m b))
-type instance Eval (FoldlMHelper f a b) = Flip (>>=) b <=< Flip f a
-
 --------------------------------------------------------------------------------
 -- Traversable
 
@@ -340,13 +305,6 @@
 type instance Eval (Traverse f lst) =
     Eval (Foldr (ConsHelper f) (Eval (Return '[])) lst)
 
--- | Helper for [] traverse
-data ConsHelper :: (a -> Exp (f b)) -> a -> f [b] -> Exp (f [b])
-type instance Eval (ConsHelper f x ys) = Eval (LiftA2 (Pure2 '(:)) (Eval (f x)) ys)
--- The following would need an extra import line:
--- type instance Eval (ConsHelper f x ys) = Eval (LiftA2 Cons (Eval (f x)) ys)
-
-
 -- Maybe
 type instance Eval (Traverse f 'Nothing) = Eval (Return 'Nothing)
 type instance Eval (Traverse f ('Just x)) = Eval (Map (Pure1 'Just) (Eval (f x)))
@@ -355,10 +313,8 @@
 type instance Eval (Traverse f ('Left e)) = Eval (Return ('Left e))
 type instance Eval (Traverse f ('Right x)) = Eval (Map (Pure1 'Right) (Eval (f x)))
 
-
--- | Id function correspondes to term level 'id'-function.
-data Id :: a -> Exp a
-type instance Eval (Id a) = a
+-- ((,) a)
+type instance Eval (Traverse f '(x, y)) = Eval (Map (Tuple2 x) (Eval (f y)))
 
 
 -- | Sequence
@@ -385,4 +341,91 @@
 data Sequence :: t (f a) -> Exp (f (t a))
 type instance Eval (Sequence tfa) = Eval (Traverse Id tfa)
 
+--------------------------------------------------------------------------------
+-- Utility
 
+-- | Id function correspondes to term level 'id'-function.
+data Id :: a -> Exp a
+type instance Eval (Id a) = a
+
+--------------------------------------------------------------------------------
+-- Helper Functions
+
+-- | Needed by LiftA2 instance to partially apply function
+data App2 :: (a -> b -> c) -> a -> Exp (b -> c)
+type instance Eval (App2 f a) = f a
+
+-- | Needed by LiftA3 instance to partially apply function
+data App3 :: (a -> b -> c -> d) -> a -> Exp (b -> Exp (c -> d))
+type instance Eval (App3 f a) = Pure2 f a
+
+-- | Needed by LiftA4 instance to partially apply function
+data App4 :: (a -> b -> c -> d -> e) -> a -> Exp (b -> Exp (c -> Exp (d -> e)))
+type instance Eval (App4 f a) = App3 (f a)
+
+-- | Needed by LiftA5 instance to partially apply function
+data App5 :: (a -> b -> c -> d -> e -> g) -> a -> Exp (b -> Exp (c -> Exp (d -> Exp (e -> g))))
+type instance Eval (App5 f a) = App4 (f a)
+
+-- | Helper for the [] applicative instance.
+data Star_ :: (a -> Exp b) -> f a -> Exp (f b)
+type instance Eval (Star_ _ '[]) = '[]
+type instance Eval (Star_ f (a ': as)) =
+    Eval (f a) ': Eval (Star_ f as)
+
+-- | Helper for 'FoldlM'
+data FoldlMHelper :: (b -> a -> Exp (m b)) -> a -> (b -> Exp (m b)) -> Exp (b -> Exp (m b))
+type instance Eval (FoldlMHelper f a b) = Flip (>>=) b <=< Flip f a
+
+-- | Helper for [] traverse
+data ConsHelper :: (a -> Exp (f b)) -> a -> f [b] -> Exp (f [b])
+type instance Eval (ConsHelper f x ys) = Eval (LiftA2 (Pure2 '(:)) (Eval (f x)) ys)
+-- The following would need an extra import line:
+-- type instance Eval (Cons_f f x ys) = Eval (LiftA2 Cons (Eval (f x)) ys)
+
+
+--------------------------------------------------------------------------------
+-- For Examples
+
+-- | For Applicative documentation example
+data Plus1 :: Nat -> Exp Nat
+type instance Eval (Plus1 n) = n TN.+ 1
+
+-- | For Applicative documentation example
+data Plus2 :: Nat -> Exp Nat
+type instance Eval (Plus2 n) = n TN.+ 2
+
+-- | For the example. Turn an input number to list of two numbers of a bit
+-- larger numbers.
+data Plus2M :: Nat -> Exp [Nat]
+type instance Eval (Plus2M n) = '[n TN.+ 2, n TN.+3]
+
+-- | Part of an example
+data PureXPlusY :: Nat -> Nat -> Exp [Nat]
+type instance Eval (PureXPlusY x y) = Eval (Return ((TN.+) x y))
+
+-- | Part of an example
+data XPlusYs :: Nat -> [Nat] -> Exp [Nat]
+type instance Eval (XPlusYs x ys) = Eval (ys >>= PureXPlusY x)
+
+-- | An example implementing
+--
+-- sumM xs ys = do
+--     x <- xs
+--     y <- ys
+--     return (x + y)
+--
+-- or
+--
+-- sumM xs ys = xs >>= (\x -> ys >>= (\y -> pure (x+y)))
+--
+-- Note the use of helper functions. This is a bit awkward, a type level
+-- lambda would be nice.
+data XsPlusYsMonadic :: [Nat] -> [Nat] -> Exp [Nat]
+type instance Eval (XsPlusYsMonadic xs ys) = Eval (xs >>= Flip XPlusYs ys)
+
+-- data Sumnd :: [Nat] -> [Nat] -> Exp [Nat]
+-- type instance Eval (Sumnd xs ys) = xs >>=
+
+-- data Sum2 :: Nat -> Nat -> Exp Nat
+-- type instance Eval (Sum2 x y) = x TN.+ y
diff --git a/src/Fcf/Data/Reflect.hs b/src/Fcf/Data/Reflect.hs
--- a/src/Fcf/Data/Reflect.hs
+++ b/src/Fcf/Data/Reflect.hs
@@ -7,7 +7,6 @@
 {-# LANGUAGE TypeFamilies           #-}
 {-# LANGUAGE TypeInType             #-}
 {-# LANGUAGE TypeOperators          #-}
-{-# LANGUAGE UndecidableInstances   #-}
 {-# OPTIONS_GHC -Wall                       #-}
 {-# OPTIONS_GHC -Werror=incomplete-patterns #-}
 
@@ -30,13 +29,14 @@
 
 import qualified GHC.TypeLits as TL
 import           GHC.TypeLits (Nat, Symbol, KnownNat, KnownSymbol)
+import           Data.String (fromString, IsString)
 import           Data.Proxy
-import qualified Data.Map.Strict as MS
+-- import qualified Data.Map.Strict as MS
+import qualified Data.Map as DM
 import qualified Data.IntMap.Strict as IMS
 import qualified Data.Set as S
-#if __GLASGOW_HASKELL__ >= 902
-import qualified Data.Text as Txt
-#endif
+-- #if __GLASGOW_HASKELL__ >= 902
+-- #endif
 import qualified Data.Tree as T
 
 -- import qualified Fcf.Core as C (Eval)
@@ -87,218 +87,112 @@
 
 --------------------------------------------------------------------------------
 
-class KnownVal typeval val where
-    fromType :: Proxy typeval -> val
-
-instance KnownNat n => KnownVal (n :: Nat) Integer where
-    fromType _ = TL.natVal (Proxy @n)
+class KnownVal val kind where
+    fromType :: Proxy kind -> val
 
-instance KnownNat n => KnownVal (n :: Nat) Int where
+instance (KnownNat n, Num a) => KnownVal a (n :: Nat) where
     fromType _ = fromInteger $ TL.natVal (Proxy @n)
 
-instance KnownSymbol s => KnownVal (s :: Symbol) String where
-    fromType _ = TL.symbolVal (Proxy @s)
-
---------------------------------------------------------------------------------
-
--- List instances
-
-instance KnownVal ('[] :: [Nat]) [Integer] where
-    fromType _ = []
-
-instance (KnownNat n, KnownVal ns [Integer]) => KnownVal (n : ns :: [Nat]) [Integer] where
-    fromType _ = TL.natVal (Proxy @n) : fromType (Proxy @ns)
-
-
-instance KnownVal ('[] :: [Nat]) [Int] where
-    fromType _ = []
-
-instance (KnownNat n, KnownVal ns [Int]) => KnownVal (n : ns :: [Nat]) [Int] where
-    fromType _ = fromInteger (TL.natVal (Proxy @n)) : fromType (Proxy @ns)
+instance KnownVal Bool 'True where fromType _ = True
+instance KnownVal Bool 'False where fromType _ = False
 
+instance (IsString str, KnownSymbol s) => KnownVal str (s :: Symbol )where
+    fromType _ = fromString $ TL.symbolVal (Proxy @s)
 
-instance KnownVal ('[] :: [Symbol]) [String] where
-    fromType _ = []
+#if __GLASGOW_HASKELL__ >= 902
 
-instance (KnownSymbol sym, KnownVal syms [String])
-    => KnownVal (sym : syms :: [Symbol]) [String]
+-- | Text instance.
+--
+-- === __Example__
+--
+-- >>> import qualified Data.Text as Txt
+-- >>> :{
+-- afun :: forall r. (r ~ 'FTxt.Text "hmm") => Txt.Text
+-- afun = fromType (Proxy @r)
+-- :}
+--
+-- >>> afun
+-- "hmm"
+instance (IsString str, KnownSymbol sym) => KnownVal str ('FTxt.Text sym)
   where
-    fromType _ = TL.symbolVal (Proxy @sym) : fromType (Proxy @syms)
+    fromType _ = fromString $ fromType $ Proxy @sym 
 
+#endif
 
-instance KnownVal ('[] :: [(Nat,Nat)]) [(Int,Int)] where
-    fromType _ = []
--- This helps with NatMap instances
+--------------------------------------------------------------------------------
 
-instance (KnownNat n, KnownNat m, KnownVal nms [(Int,Int)])
-    => KnownVal ( '(n,m) : nms :: [(Nat,Nat)]) [(Int,Int)]
-  where
-    fromType _ =
-        (fromInteger (TL.natVal (Proxy @n)), fromInteger (TL.natVal (Proxy @m)))
-        : fromType (Proxy @nms)
--- This helps with NatMap instances
+-- List instances
 
-instance KnownVal ('[] :: [(Nat,Symbol)]) [(Int,String)] where
+instance KnownVal [a] '[] where
     fromType _ = []
--- This helps with NatMap instances
 
-instance (KnownNat n, KnownSymbol m, KnownVal nms [(Int,String)])
-    => KnownVal ( '(n,m) : nms :: [(Nat,Symbol)]) [(Int,String)]
-  where
-    fromType _ =
-        (fromInteger (TL.natVal (Proxy @n)), TL.symbolVal (Proxy @m))
-        : fromType (Proxy @nms)
--- This helps with NatMap instances
+instance (KnownVal typ x, KnownVal [typ] xs) => KnownVal [typ] (x ': xs) where
+    fromType _ = fromType (Proxy @x) : fromType (Proxy @xs)
 
 --------------------------------------------------------------------------------
 
 -- Trees
-
--- instances for Forests, that is, lists of Trees.
-instance KnownVal '[] [T.Tree Int] where fromType _ = []
-
--- instances for Forests
-instance (KnownVal t (T.Tree Int), KnownVal trees [T.Tree Int])
-    => KnownVal (t : trees) [T.Tree Int]
-  where
-    fromType _ = fromType @t Proxy : fromType @trees Proxy
-
--- instance for Trees (using forest definition).
-instance (KnownNat n, KnownVal trees [T.Tree Int])
-    => KnownVal ('FT.Node (n :: Nat) trees) (T.Tree Int)
-  where
-    fromType _ = T.Node (fromType @n Proxy) (fromType @trees Proxy)
-
-
-instance KnownVal '[] [T.Tree Integer] where fromType _ = []
-
-instance (KnownVal t (T.Tree Integer), KnownVal trees [T.Tree Integer])
-    => KnownVal (t : trees) [T.Tree Integer]
-  where
-    fromType _ = fromType @t Proxy : fromType @trees Proxy
-
-instance (KnownNat n, KnownVal trees [T.Tree Integer])
-    => KnownVal ('FT.Node (n :: Nat) trees) (T.Tree Integer)
-  where
-    fromType _ = T.Node (fromType @n Proxy) (fromType @trees Proxy)
-
-
-instance KnownVal '[] [T.Tree String] where fromType _ = []
-
-instance (KnownVal t (T.Tree String), KnownVal trees [T.Tree String])
-    => KnownVal (t : trees) [T.Tree String]
-  where
-    fromType _ = fromType @t Proxy : fromType @trees Proxy
-
-instance (KnownSymbol n, KnownVal trees [T.Tree String])
-    => KnownVal ('FT.Node (n :: Symbol) trees) (T.Tree String)
+--
+instance (KnownVal typ k, KnownVal (T.Forest typ) trees) => KnownVal (T.Tree typ) ('FT.Node k trees)
   where
-    fromType _ = T.Node (fromType @n Proxy) (fromType @trees Proxy)
-
+    fromType _ = T.Node (fromType (Proxy @k)) (fromType (Proxy @trees))
 
 --------------------------------------------------------------------------------
 
 -- NatMaps / IntMaps
-
-instance (KnownVal (pairs :: [(Nat,Nat)]) [(Int,Int)])
-    => KnownVal ('NM.NatMap pairs) (IMS.IntMap Int)
-  where
-    fromType _ = IMS.fromList (fromType @pairs Proxy)
-
-instance (KnownVal (pairs :: [(Nat,Integer)]) [(Int,Integer)])
-    => KnownVal ('NM.NatMap pairs) (IMS.IntMap Integer)
-  where
-    fromType _ = IMS.fromList (fromType @pairs Proxy)
-
-instance (KnownVal (pairs :: [(Nat,Symbol)]) [(Int,String)])
-    => KnownVal ('NM.NatMap pairs) (IMS.IntMap String)
+--
+instance (KnownVal [(Int,val)] pairs) => KnownVal (IMS.IntMap val) ('NM.NatMap pairs)
   where
-    fromType _ = IMS.fromList (fromType @pairs Proxy)
-
+    fromType _ = IMS.fromList (fromType (Proxy @pairs))
 
 --------------------------------------------------------------------------------
 
 -- Maps
 
-instance (KnownVal (pairs :: [(Nat,Nat)]) [(Int,Int)])
-    => KnownVal ('MC.MapC pairs) (MS.Map Int Int)
-  where
-    fromType _ = MS.fromList (fromType @pairs Proxy)
-
-instance (KnownVal (pairs :: [(Nat,Integer)]) [(Int,Integer)])
-    => KnownVal ('MC.MapC pairs) (MS.Map Int Integer)
-  where
-    fromType _ = MS.fromList (fromType @pairs Proxy)
-
-instance (KnownVal (pairs :: [(Nat,Symbol)]) [(Int,String)])
-    => KnownVal ('MC.MapC pairs) (MS.Map Int String)
-  where
-    fromType _ = MS.fromList (fromType @pairs Proxy)
-
-
-instance (KnownVal (pairs :: [(Symbol,Nat)]) [(String,Int)])
-    => KnownVal ('MC.MapC pairs) (MS.Map String Int)
-  where
-    fromType _ = MS.fromList (fromType @pairs Proxy)
-
-instance (KnownVal (pairs :: [(Symbol,Integer)]) [(String,Integer)])
-    => KnownVal ('MC.MapC pairs) (MS.Map String Integer)
-  where
-    fromType _ = MS.fromList (fromType @pairs Proxy)
-
-instance (KnownVal (pairs :: [(Symbol,Symbol)]) [(String,String)])
-    => KnownVal ('MC.MapC pairs) (MS.Map String String)
+instance (Ord key, KnownVal [(key,val)] pairs) => KnownVal (DM.Map key val) ('MC.MapC pairs)
   where
-    fromType _ = MS.fromList (fromType @pairs Proxy)
-
+    fromType _ = DM.fromList (fromType (Proxy @pairs))
 
 --------------------------------------------------------------------------------
 
 -- Set
- 
-instance (KnownVal (mems :: [Nat]) [Int]) => KnownVal ('FS.Set mems) (S.Set Int)
-  where
-    fromType _ = S.fromList (fromType @mems Proxy)
 
-instance (KnownVal (mems :: [Nat]) [Integer]) => KnownVal ('FS.Set mems) (S.Set Integer)
-  where
-    fromType _ = S.fromList (fromType @mems Proxy)
-
-instance (KnownVal (mems :: [Symbol]) [String]) => KnownVal ('FS.Set mems) (S.Set String)
+instance (Ord typ, KnownVal [typ] kind) => KnownVal (S.Set typ) ('FS.Set kind)
   where
-    fromType _ = S.fromList (fromType @mems Proxy)
+    fromType _ = S.fromList (fromType (Proxy @kind))
+ 
+--------------------------------------------------------------------------------
 
+-- Either
 
---------------------------------------------------------------------------------
+instance (KnownVal a1 a) => KnownVal (Either a1 b1) ('Left a) where
+    fromType _ = Left (fromType @a1 (Proxy @a))
 
-#if __GLASGOW_HASKELL__ >= 902
+instance (KnownVal b1 b) => KnownVal (Either a1 b1) ('Right b) where
+    fromType _ = Right (fromType @b1 (Proxy @b))
 
--- Text
+--------------------------------------------------------------------------------
 
--- instance (KnownVal (sym :: Symbol) String) => KnownVal ('FTxt.Text sym) Txt.Text
---   where
---     fromType _ = Txt.pack $ fromType @sym Proxy
+-- Maybe
 
+instance (KnownVal a1 a) => KnownVal (Maybe a1) ('Just a) where
+    fromType _ = Just (fromType @a1 (Proxy @a))
 
--- | Text instance.
---
--- === __Example__
---
--- >>> :{
--- afun :: forall r. (r ~ 'FTxt.Text "hmm") => Txt.Text
--- afun = fromType @r Proxy
--- :}
---
--- >>> afun
--- "hmm"
-instance KnownSymbol sym => KnownVal ('FTxt.Text sym) Txt.Text
-  where
-    fromType _ = Txt.pack $ fromType @sym Proxy
+instance KnownVal (Maybe a1) 'Nothing where
+    fromType _ = Nothing
 
+--------------------------------------------------------------------------------
 
+-- Tuples
 
-#else
+instance (KnownVal a1 a, KnownVal b1 b) => KnownVal (a1,b1) '(a,b) where
+    fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b))
 
-#endif
+instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c) => KnownVal (a1,b1,c1) '(a,b,c) where
+    fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b), fromType @c1 (Proxy @c))
 
+instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c, KnownVal d1 d) => KnownVal (a1,b1,c1,d1) '(a,b,c,d) where
+    fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b), fromType @c1 (Proxy @c), fromType @d1 (Proxy @d))
 
+instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c, KnownVal d1 d, KnownVal e1 e) => KnownVal (a1,b1,c1,d1,e1) '(a,b,c,d,e) where
+    fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b), fromType @c1 (Proxy @c), fromType @d1 (Proxy @d), fromType @e1 (Proxy @e))
diff --git a/src/Fcf/Data/Set.hs b/src/Fcf/Data/Set.hs
--- a/src/Fcf/Data/Set.hs
+++ b/src/Fcf/Data/Set.hs
@@ -73,16 +73,6 @@
 
 --------------------------------------------------------------------------------
 
--- For the doctests:
-
--- $setup
--- >>> import qualified GHC.TypeLits as TL
--- >>> import           Fcf.Data.Nat
--- >>> import           Fcf.Data.Symbol
--- >>> import           Fcf.Alg.Sort
-
---------------------------------------------------------------------------------
-
 -- | Set-definition.
 newtype Set a = Set [a]
 
@@ -93,7 +83,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! (Eval Empty :: Set Nat)
+-- > :kind! (Eval Empty :: Set Nat)
 -- (Eval Empty :: Set Nat) :: Set TL.Natural
 -- = 'Set '[]
 --
@@ -105,7 +95,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Singleton 1)
+-- > :kind! Eval (Singleton 1)
 -- Eval (Singleton 1) :: Set TL.Natural
 -- = 'Set '[1]
 data Singleton :: v -> Exp (Set v)
@@ -116,11 +106,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Insert 3 =<< FromList '[1, 2])
+-- > :kind! Eval (Insert 3 =<< FromList '[1, 2])
 -- Eval (Insert 3 =<< FromList '[1, 2]) :: Set TL.Natural
 -- = 'Set '[3, 1, 2]
 --
--- >>> :kind! Eval (Insert 2 =<< FromList '[1, 2])
+-- > :kind! Eval (Insert 2 =<< FromList '[1, 2])
 -- Eval (Insert 2 =<< FromList '[1, 2]) :: Set TL.Natural
 -- = 'Set '[1, 2]
 data Insert :: v -> Set v -> Exp (Set v)
@@ -133,11 +123,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Delete 5 =<< FromList '[5, 3])
+-- > :kind! Eval (Delete 5 =<< FromList '[5, 3])
 -- Eval (Delete 5 =<< FromList '[5, 3]) :: Set TL.Natural
 -- = 'Set '[3]
 --
--- >>> :kind! Eval (Delete 7 =<< FromList '[5, 3])
+-- > :kind! Eval (Delete 7 =<< FromList '[5, 3])
 -- Eval (Delete 7 =<< FromList '[5, 3]) :: Set TL.Natural
 -- = 'Set '[5, 3]
 data Delete :: v -> Set v -> Exp (Set v)
@@ -148,10 +138,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Member 5 =<< FromList '[5, 3])
+-- > :kind! Eval (Member 5 =<< FromList '[5, 3])
 -- Eval (Member 5 =<< FromList '[5, 3]) :: Bool
 -- = 'True
--- >>> :kind! Eval (Member 7 =<< FromList '[5, 3])
+--
+-- > :kind! Eval (Member 7 =<< FromList '[5, 3])
 -- Eval (Member 7 =<< FromList '[5, 3]) :: Bool
 -- = 'False
 data Member :: v -> Set v -> Exp Bool
@@ -161,10 +152,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (NotMember 5 =<< FromList '[5, 3])
+-- > :kind! Eval (NotMember 5 =<< FromList '[5, 3])
 -- Eval (NotMember 5 =<< FromList '[5, 3]) :: Bool
 -- = 'False
--- >>> :kind! Eval (NotMember 7 =<< FromList '[5, 3])
+--
+-- > :kind! Eval (NotMember 7 =<< FromList '[5, 3])
 -- Eval (NotMember 7 =<< FromList '[5, 3]) :: Bool
 -- = 'True
 data NotMember :: v -> Set v -> Exp Bool
@@ -176,10 +168,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Null =<< FromList '[5, 3])
+-- > :kind! Eval (Null =<< FromList '[5, 3])
 -- Eval (Null =<< FromList '[5, 3]) :: Bool
 -- = 'False
--- >>> :kind! Eval (Null =<< Empty)
+-- 
+-- > :kind! Eval (Null =<< Empty)
 -- Eval (Null =<< Empty) :: Bool
 -- = 'True
 data Null :: Set v -> Exp Bool
@@ -191,7 +184,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Size =<< FromList '[5, 3])
+-- > :kind! Eval (Size =<< FromList '[5, 3])
 -- Eval (Size =<< FromList '[5, 3]) :: TL.Natural
 -- = 2
 data Size :: Set v -> Exp TL.Nat
@@ -202,19 +195,19 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))
+-- > :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))
 -- Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4])) :: Bool
 -- = 'True
 --
--- >>> :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))
+-- > :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))
 -- Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4])) :: Bool
 -- = 'True
 --
--- >>> :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4]))
+-- > :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4]))
 -- Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4])) :: Bool
 -- = 'True
 --
--- >>> :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))
+-- > :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))
 -- Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4])) :: Bool
 -- = 'False
 data IsSubsetOf :: Set a -> Set a -> Exp Bool
@@ -226,11 +219,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))
+-- > :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))
 -- Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4])) :: Bool
 -- = 'False
 --
--- >>> :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))
+-- > :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))
 -- Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) :: Bool
 -- = 'True
 data IsProperSubsetOf :: Set a -> Set a -> Exp Bool
@@ -244,7 +237,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )
+-- > :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )
 -- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set
 --                                                                        TL.Natural
 -- = 'Set '[7, 5, 3]
@@ -263,7 +256,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
+-- > :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
 -- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set
 --                                                                            TL.Natural
 -- = 'Set '[3]
@@ -280,7 +273,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
+-- > :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
 -- Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set
 --                                                                              TL.Natural
 -- = 'Set '[5]
@@ -333,7 +326,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])
+-- > :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])
 -- Eval (PowerSet =<< FromList '["a", "b", "c"]) :: Set
 --                                                    (Set TL.Symbol)
 -- = 'Set
@@ -341,7 +334,7 @@
 --        'Set '["a"], 'Set '["a", "b"], 'Set '["a", "c"],
 --        'Set '["a", "b", "c"]]
 --
--- >>> :kind! Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])
+-- > :kind! Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])
 -- Eval (PowerSet =<< FromList '[Int, Char, Maybe Int]) :: Set
 --                                                           (Set (*))
 -- = 'Set
@@ -361,7 +354,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (FromList '[1, 2])
+-- > :kind! Eval (FromList '[1, 2])
 -- Eval (FromList '[1, 2]) :: Set TL.Natural
 -- = 'Set '[1, 2]
 data FromList :: [v] -> Exp (Set v)
@@ -371,15 +364,14 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])
+-- > :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])
 -- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set
 --                                                        TL.Natural]
 -- = '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],
 --      'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]
 --
--- >>> :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])
+-- > :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])
 -- Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3]) :: [[TL.Natural]]
 -- = '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]]
 data ToList :: Set v -> Exp [v]
 type instance Eval (ToList ('Set lst)) = lst
-
diff --git a/src/Fcf/Data/Tuple.hs b/src/Fcf/Data/Tuple.hs
--- a/src/Fcf/Data/Tuple.hs
+++ b/src/Fcf/Data/Tuple.hs
@@ -40,3 +40,20 @@
 -- = '(2, 1)
 data Swap :: (a, b) -> Exp (b, a)
 type instance Eval (Swap '(a,b)) = '(b,a)
+
+-- | 2-tuple to allow for partial application of 2-tuple at the type level
+data Tuple2 :: a -> b -> Exp (a, b)
+type instance Eval (Tuple2 a b) = '(a,b)
+
+-- | 3-tuple to allow for partial application of 3-tuple at the type level
+data Tuple3 :: a -> b -> c -> Exp (a, b, c)
+type instance Eval (Tuple3 a b c) = '(a,b,c)
+
+-- | 4-tuple to allow for partial application of 4-tuple at the type level
+data Tuple4 :: a -> b -> c -> d -> Exp (a, b, c, d)
+type instance Eval (Tuple4 a b c d) = '(a,b,c,d)
+
+-- | 5-tuple to allow for partial application of 4-tuple at the type level
+data Tuple5 :: a -> b -> c -> d -> e -> Exp (a, b, c, d, e)
+type instance Eval (Tuple5 a b c d e) = '(a,b,c,d,e)
+
diff --git a/test/Test/Alg.hs b/test/Test/Alg.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Alg.hs
@@ -0,0 +1,10 @@
+
+module Test.Alg where
+
+import           Test.Alg.List as L (spec)
+import           Test.Hspec (describe, Spec)
+
+spec :: Spec
+spec = describe "Data"  
+  L.spec
+
diff --git a/test/Test/Alg/List.hs b/test/Test/Alg/List.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Alg/List.hs
@@ -0,0 +1,171 @@
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeInType             #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# OPTIONS_GHC -Wall                       #-}
+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
+
+{- 
+In this module, we test mainly Fcf.Alg.List module. In couple of 
+places, we use the "spec" and Reflect. 
+
+Many of the tests are such that if the answer is not correct, the
+whole test module refuses to compile.  Please do try to change some 
+of the values to see. 
+
+Note that in a way, the spec tests are not needed. If testing just 
+the type level behaviour, the module would refuse to compile if 
+test is not ok (and thus, guard the quality earlier than what the 
+test framework can do).  
+
+Anyhow, as these also work as examples, it is probably ok to have different 
+ways of reaching the results. (E.g. to see, how to get the type level 
+values to value level.)
+
+-}
+module Test.Alg.List where
+
+import           Data.Proxy
+import           Data.Type.Equality ((:~:)(Refl))
+import           Test.Hspec (describe, it, shouldBe, Spec)
+
+import           Fcf.Core (Eval)
+import           Fcf.Combinators (type (=<<))
+import           Fcf.Alg.List
+import           Fcf.Alg.Morphism
+import           Fcf.Data.Reflect (fromType)
+
+--------------------------------------------------------------------------------
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--
+-- > :kind! Eval (ListToFix '[1,2,3])
+-- Eval (ListToFix '[1,2,3]) :: Fix (ListF TL.Natural)
+-- = 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF))))))
+_ = Refl :: Eval (ListToFix '[1,2,3])
+  :~: 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF))))))
+
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--  
+-- > :kind! Eval (ListToParaFix '[1,2,3])
+-- Eval (ListToParaFix '[1,2,3]) :: Fix
+--                                    (ListF (TL.Natural, [TL.Natural]))
+-- = 'Fix
+--     ('ConsF
+--        '(1, '[2, 3])
+--        ('Fix ('ConsF '(2, '[3]) ('Fix ('ConsF '(3, '[]) ('Fix 'NilF))))))
+_ = Refl :: Eval (ListToParaFix '[1,2,3])
+  :~: 'Fix ('ConsF
+       '(1, '[2, 3])
+       ('Fix ('ConsF '(2, '[3]) ('Fix ('ConsF '(3, '[]) ('Fix 'NilF))))))
+
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--  
+-- > :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])
+-- Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2]) :: [TL.Natural]
+-- = '[5, 1, 3, 2]
+_ = Refl :: Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])
+  :~: '[5, 1, 3, 2]
+
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--  
+-- > :kind! Eval (Sliding 3 '[1,2,3,4,5,6])
+-- Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[TL.Natural]]
+-- = '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]]
+_ = Refl :: Eval (Sliding 3 '[1,2,3,4,5,6])
+  :~: '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]]
+
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--  
+-- > :kind! Eval (Evens =<< RunInc 8)
+-- Eval (Evens =<< RunInc 8) :: [TL.Natural]
+-- = '[2, 4, 6, 8]
+_ = Refl :: Eval (Evens =<< RunInc 8)
+  :~: '[2, 4, 6, 8]
+
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--  
+-- > :kind! Eval (RunInc 8)
+-- Eval (RunInc 8) :: [TL.Natural]
+-- = '[1, 2, 3, 4, 5, 6, 7, 8]
+_ = Refl :: Eval (RunInc 8)
+  :~: '[1, 2, 3, 4, 5, 6, 7, 8]
+
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--  
+-- > :kind! Eval (MToN 1 3)
+-- Eval (MToN 1 3) :: [TL.Natural]
+-- = '[1, 2, 3]
+_ = Refl :: Eval (MToN 1 3)
+  :~: '[1, 2, 3]
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--  
+-- > :kind! Eval (ToList 1)
+-- Eval (ToList 1) :: [TL.Natural]
+-- = '[1]
+_ = Refl :: Eval (ToList 1)
+  :~: '[1]
+
+  
+--------------------------------------------------------------------------------
+
+-- > :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])
+-- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: TL.Natural
+-- = 3
+
+-- > :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])
+-- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural
+-- = 10
+
+-- > :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])
+-- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural
+-- = 24
+
+-- > :kind! Eval (Sum '[1,2,3])
+-- Eval (Sum '[1,2,3]) :: TL.Natural
+-- = 6
+
+-- > :kind! Eval (Equal '[1,2,3] '[1,2,3])
+-- Eval (Equal '[1,2,3] '[1,2,3]) :: Bool
+-- = 'True
+
+-- > :kind! Eval (Equal '[1,2,3] '[1,3,2])
+-- Eval (Equal '[1,2,3] '[1,3,2]) :: Bool
+-- = 'False
+
+spec :: Spec
+spec = describe "List" $ do
+  it "Cata LenAlg" $ do
+    let test :: forall r. (r ~ Eval (Cata LenAlg =<< ListToFix '[1,2,3])) => Int
+        test = fromType (Proxy @r)
+    test `shouldBe` 3
+  it "Cata SumAlg" $ do
+    let test :: forall r. (r ~ Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])) => Int
+        test = fromType (Proxy @r)
+    test `shouldBe` 10
+  it "Cata ProdAlg" $ do
+    let test :: forall r. (r ~ Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])) => Int
+        test = fromType (Proxy @r)
+    test `shouldBe` 24
+  it "Sum" $ do
+    let test :: forall r. (r ~ Eval (Sum '[1,2,3])) => Int
+        test = fromType (Proxy @r)
+    test `shouldBe` 6
+  it "Equal, True" $ do
+    let test :: forall r. (r ~ Eval (Equal '[1,2,3] '[1,2,3])) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` True
+  it "Equal, False" $ do
+    let test :: forall r. (r ~ Eval (Equal '[1,2,3] '[1,3,2])) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` False
+
diff --git a/test/Test/Control.hs b/test/Test/Control.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Control.hs
@@ -0,0 +1,9 @@
+
+module Test.Control where
+
+import           Test.Control.Monad as M (spec)
+import           Test.Hspec (describe, Spec)
+
+spec :: Spec
+spec = describe "Control" $ do
+  M.spec
diff --git a/test/Test/Control/Monad.hs b/test/Test/Control/Monad.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Control/Monad.hs
@@ -0,0 +1,140 @@
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE TupleSections          #-}
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# OPTIONS_GHC -Wall                       #-}
+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
+
+module Test.Control.Monad where
+
+import           Data.Functor ((<&>))
+import           Data.Proxy
+import           Control.Applicative
+import           Test.Hspec (describe, it, shouldBe, Spec)
+import           GHC.TypeLits (Nat, Symbol)
+
+import           Fcf hiding (type (<*>))
+import           Fcf.Data.Tuple
+import           Fcf.Data.List (Cons)
+import           Fcf.Control.Monad
+import           Fcf.Class.Monoid (type (.<>))
+import           Fcf.Data.Reflect (fromType)
+
+-- data TraversableTest = TraversableTest Symbol [(Symbol, Nat)]
+
+data SafeMinus :: Nat -> Nat -> Exp (Either Symbol Nat)
+type instance Eval (SafeMinus a b) = If (Eval (a >= b)) ('Right (Eval (a - b))) ('Left "Nat cannot be negative")
+
+
+spec :: Spec
+spec = describe "Monad" $ do
+  it "liftA2 (,) instance" $ do
+    let test :: forall r. (r ~ Eval (LiftA2 Tuple2 '("hello ", 5) '("world", 6))) => (String, (Int, Int))
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      liftA2 (,) ("hello ", 5) ("world", 6)
+  it "<*> (,) instance" $ do
+    let test :: forall r. (r ~ Eval ('("hello ", (+) 15) <*> '("world!", 2002))) => (String,Int)
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      ("hello ", (+) 15) <*> ("world!", 2002)
+  it ">>= (,) instance" $ do
+    let test :: forall r. (r ~ Eval ('("age", 5) >>= (Return <=< (+) 1))) => (String,Int)
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      (("age",5) <&> (+) 1)
+      -- Above was suggested by hlint for the following:
+      -- (("age",5) >>= return . (+) 1)
+  it "liftA3 (,,) instance" $ do
+    let test :: forall r. (r ~ Eval (LiftA3 Tuple3 '("hello ", "<", 6) '("world", " ", 8) '("!", ">", 10))) => (String, String, (Int, Int, Int))
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      liftA3 (,,) ("hello ","<",6) ("world"," ",8) ("!",">",10)
+  it ">>= (,,) instance" $ do
+    let test :: forall r. (r ~ Eval ('("he","wo",19) >>= (Tuple3 "llo" "rld" <=< Flip (-) 1))) => (String,String,Int)
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      (("he","wo",19) >>= ("llo","rld",) . flip (-) 1)
+  it "liftA4 Either instance test Left" $ do
+    let test :: forall r. (r ~ Eval (LiftA4 Tuple4 ('Right 5) ('Right 6) ('Right 7) ('Left "fail"))) => Either String (Int,Int,Int,Int)
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      (,,,) <$> Right 5 <*> Right 6 <*> Right 7 <*> Left "fail"
+  it "liftA4 Either instance test Right" $ do
+    let test :: forall r. (r ~ Eval (LiftA4 Tuple4 ('Right 5) ('Right 6) ('Right 7) ('Right 0))) => Either String (Int,Int,Int,Int)
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      (,,,) <$> Right 5 <*> Right 6 <*> Right 7 <*> Right 0
+  it "Traversable Either instance, test with MapM" $ do
+    let typeLevelFunc :: forall (list :: [(Symbol,Nat)]) r. 
+            (r ~ Eval 
+              (Map 
+                (Flip Cons '[] <=< Tuple2 "test") 
+                (MapM
+                  (MapM (Flip SafeMinus 1))
+                  @@ list
+                )
+              )
+            ) => Proxy r
+        typeLevelFunc = Proxy @r
+    let safeMinus a b = if a >= b then Right (a - b) else Left "Nat cannot be negative"
+    let valTest :: [(String,Int)] -> Either String [(String, [(String, Int)])]
+        valTest list = fmap (flip (:) [] . ("test",)) (mapM (mapM (`safeMinus` 1)) list)
+    fromType (typeLevelFunc @'[ '("key1",1), '("key2",2)])
+      `shouldBe` 
+      valTest [("key1",1),("key2",2)]
+    fromType (typeLevelFunc @'[ '("key1",0), '("key2",2)])
+      `shouldBe` 
+      valTest [("key1",0),("key2",2)]
+  it "liftA5 [] instance" $ do
+    let test :: forall r. (r ~ Eval (LiftA5 Tuple5 '[1,5] '[2,4] '[6,7,8] '[9,11,10] '[0] )) => [(Int,Int,Int,Int,Int)]
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      (,,,,) <$> [1,5] <*> [2,4] <*> [6,7,8] <*> [9,11,10] <*> [0]
+  it "<*> [] instance" $ do
+    let test :: forall r. (r ~ Eval ('[(+) 1,(+) 2] <*> '[3,4])) => [Int]
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      [(+) 1,(+) 2] <*> [3,4]
+  it ">>= [] instance" $ do
+    let test :: forall r. (r ~ Eval ('[5,6,7] >>= Plus2M)) => [Int]
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      ([5,6,7] >>= (\n -> [n + 2, n + 3]))
+  it ">>= Maybe instance test Just" $ do
+    let test :: forall r. (r ~ Eval ('Just "hello" >>= (Return <=< Flip (.<>) " world"))) => Maybe String
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      (Just "hello" <&> flip (<>) " world")
+      -- Above was suggested by hlint for the following:
+      -- (Just "hello" >>= (return . flip (<>) " world"))
+  it ">>= Maybe instance test Nothing" $ do
+    let test :: forall r. (r ~ Eval ('Nothing >>= (Return <=< Flip (.<>) " world"))) => Maybe String
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      (Nothing <&> flip (<>) " world")
+      -- Above was suggested by hlint for the following:
+      -- (Nothing >>= (return . flip (<>) " world"))
+  it ">> Maybe instance" $ do
+    let test :: forall r. (r ~ Eval ('Just 5 >> 'Just "hello world")) => Maybe String
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      (Just (5 :: Int) >> Just "hello world")
diff --git a/test/Test/Data.hs b/test/Test/Data.hs
--- a/test/Test/Data.hs
+++ b/test/Test/Data.hs
@@ -1,7 +1,12 @@
 
 module Test.Data where
 
-import           Test.Data.Reflect as R (tests)
+import           Test.Data.Reflect as R (spec)
+import           Test.Data.Set as S (spec)
+import           Test.Hspec (describe, Spec)
 
-tests = R.tests
+spec :: Spec
+spec = describe "Data" $ do 
+  R.spec
+  S.spec
 
diff --git a/test/Test/Data/Reflect.hs b/test/Test/Data/Reflect.hs
--- a/test/Test/Data/Reflect.hs
+++ b/test/Test/Data/Reflect.hs
@@ -1,10 +1,10 @@
 {-# LANGUAGE CPP                    #-}
 {-# LANGUAGE ScopedTypeVariables    #-}
-{-# LANGUAGE TypeApplications       #-}
 {-# LANGUAGE TypeFamilies           #-}
-{-# LANGUAGE TypeInType             #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE DataKinds              #-}
 {-# LANGUAGE TypeOperators          #-}
-{-# LANGUAGE UndecidableInstances   #-}
 {-# OPTIONS_GHC -Wall                       #-}
 {-# OPTIONS_GHC -Werror=incomplete-patterns #-}
 
@@ -18,6 +18,7 @@
 import qualified Data.Text as DTxt
 #endif
 import           Data.Proxy
+import           Test.Hspec (describe, it, shouldBe, Spec)
 
 import           Fcf (Eval, type (=<<))
 import qualified Fcf.Data.Set as FS
@@ -29,71 +30,227 @@
 import qualified Fcf.Data.Tree as FT
 import           Fcf.Data.Reflect
 
-tests :: Bool
-tests = 
-     testNatMap
-  && testMap
-  && testSet
-#if __GLASGOW_HASKELL__ >= 902
-  && testText
-#endif
-  && testTree
+--------------------------------------------------------------------------------
 
-testNatMap 
-  :: forall r. (r ~ Eval (FNM.Insert 3 "hih" =<< FNM.FromList '[ '(1,"haa"), '(2,"hoo")])) 
-  => Bool
-testNatMap = result == expected
-  where
-    result   = fromType @r Proxy :: IM.IntMap String
-    expected = IM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]
+spec :: Spec
+spec = describe "Reflect" $ do
+  specMaybe
+  specEither
+  specMaybeEither
+  specStructures
+  specTrees
+  
+specBool :: Spec
+specBool = describe "Bool" $ do
+  it "Bool, True" $ do
+    let test :: forall r. (r ~ 'True) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` True
+  it "Bool, False" $ do
+    let test :: forall r. (r ~ 'False) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` False
 
-testMap 
-  :: forall r. (r ~ Eval (FNMC.Insert 3 "hih" =<< FNMC.FromList '[ '(1,"haa"), '(2,"hoo")])) 
-  => Bool
-testMap = result == expected
-  where
-    result   = fromType @r Proxy :: DM.Map Int String
-    expected = DM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]
+specMaybe :: Spec
+specMaybe = describe "Maybe" $ do
+  it "Maybe Int, Just" $ do
+    let test :: forall r. (r ~ 'Just 5) 
+             => Maybe Int
+        test = fromType (Proxy @r)
+    test `shouldBe` Just 5
+  it "Maybe Int, Nothing" $ do
+    let test :: forall r. (r ~ 'Nothing) 
+             => Maybe Int
+        test = fromType (Proxy @r)
+    test `shouldBe` Nothing
+  it "Maybe String, Just" $ do
+    let test :: forall r. (r ~ 'Just "just") 
+             => Maybe String
+        test = fromType (Proxy @r)
+    test `shouldBe` Just "just"
+  it "Maybe String, Nothing" $ do
+    let test :: forall r. (r ~ 'Nothing) 
+             => Maybe String
+        test = fromType (Proxy @r)
+    test `shouldBe` Nothing
 
-testSet
-  :: forall r. (r ~ Eval (FS.FromList '[5, 9, 1, 8, 3, 5]))
-  => Bool
-testSet = result == expected
-  where
-    result   = fromType @r Proxy :: DS.Set Int
-    expected = DS.fromList [1, 3, 5, 8, 9]
-  
+specEither :: Spec
+specEither = describe "Either" $ do
+  it "Either Int String, Left" $ do
+    let test :: forall r. (r ~ 'Left 5) 
+             => Either Int String
+        test = fromType (Proxy @r)
+    test `shouldBe` Left 5
+  it "Either Int String, Right" $ do
+    let test :: forall r. (r ~ 'Right "right") 
+             => Either Int String
+        test = fromType (Proxy @r)
+    test `shouldBe` Right "right"
+  it "Either Int (Either Int String), Right Right" $ do
+    let test :: forall r. (r ~ 'Right ('Right "right"))
+             => Either Int (Either Int String)
+        test = fromType (Proxy @r)
+    test `shouldBe` Right (Right "right")
+  it "Either (Either Int String) String, Left Left" $ do
+    let test :: forall r. (r ~ 'Left ('Left 5)) 
+             => Either (Either Int String) String
+        test = fromType (Proxy @r)
+    test `shouldBe` Left (Left 5)
 
-type ExT1r =
+specMaybeEither :: Spec
+specMaybeEither = describe "Maybe Either and Either Maybe" $ do
+  it "Either Int (Maybe String), Right Just" $ do
+    let test :: forall r. (r ~ 'Right ('Just "right just"))
+             => Either Int (Maybe String)
+        test = fromType (Proxy @r)
+    test `shouldBe` Right (Just "right just")
+  it "Either Int (Maybe String), Right Nothing" $ do
+    let test :: forall r. (r ~ 'Right 'Nothing)
+             => Either Int (Maybe String)
+        test = fromType (Proxy @r)
+    test `shouldBe` Right Nothing
+  it "Maybe (Either Int String), Just Right" $ do
+    let test :: forall r. (r ~ 'Just ('Right "just right"))
+             => Maybe (Either Int String)
+        test = fromType (Proxy @r)
+    test `shouldBe` Just (Right "just right")
+  it "Maybe (Either Int String), Nothing" $ do
+    let test :: forall r. (r ~ 'Nothing)
+             => Maybe (Either Int String)
+        test = fromType (Proxy @r)
+    test `shouldBe` Nothing
+
+
+specStructures :: Spec
+specStructures = describe "Maps and other structures" $ do
+  it "NatMap" $ do
+    let test :: forall r. (r ~ Eval (
+                  FNM.Insert 3 "hih" =<< FNM.FromList '[ '(1,"haa"), '(2,"hoo")]
+                )) 
+             => IM.IntMap String
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      IM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]
+  it "Map" $ do
+    let test :: forall r. (r ~ Eval (
+                  FNMC.Insert 3 "hih" =<< FNMC.FromList '[ '(1,"haa"), '(2,"hoo")]
+                )) 
+             => DM.Map Int String
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      DM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]
+  it "Set" $ do
+    let test :: forall r. (r ~ Eval (FS.FromList '[5, 9, 1, 8, 3, 5])) 
+             => DS.Set Int
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      DS.fromList [1, 3, 5, 8, 9]
+#if __GLASGOW_HASKELL__ >= 902
+  it "text" $ do
+    let test :: forall r. (r ~ 'FTxt.Text "trial") => DTxt.Text
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      DTxt.pack "trial"
+#endif
+
+type ExTr1 =
     'FT.Node 1 
        '[ 'FT.Node 2 
           '[ 'FT.Node 3 '[ 'FT.Node 4 '[]]]
         , 'FT.Node 5 '[ 'FT.Node 6 '[]]
         ]
 
--- type ExTr2 =
---     'Node ('Just 1)
---         '[ 'Node ('Just 2)
---             '[ 'Node ('Just 3)
---                 '[ 'Node ('Just 4) '[]]
---              ]
---          , 'Node ('Just 5)
---             '[ 'Node ('Just 6) '[]
---              ]
---          ]
+type ExTr2 =
+    'FT.Node ('Just 1)
+        '[ 'FT.Node ('Just 2)
+            '[ 'FT.Node ('Just 3)
+                '[ 'FT.Node ('Just 4) '[]]
+             ]
+         , 'FT.Node ('Just 5)
+            '[ 'FT.Node ('Just 6) '[]
+             ]
+         ]
 
+type ExTr3 =
+    'FT.Node ('Just 1)
+        '[ 'FT.Node ('Just 2)
+            '[ 'FT.Node ('Just 3)
+                '[ 'FT.Node ('Just 4) '[]]
+             ]
+         , 'FT.Node ('Just 5)
+            '[ 'FT.Node 'Nothing '[]
+             ]
+         ]
 
-testTree :: forall r. (r ~ ExT1r) => Bool
-testTree = result == expected
-  where
-    result   = fromType @r Proxy :: DT.Tree Int
-    expected = DT.Node 1 [DT.Node 2 [DT.Node 3 [DT.Node 4 []]], DT.Node 5 [DT.Node 6 []]]
-    
+type ExTr4 =
+    'FT.Node ('Left 1)
+        '[ 'FT.Node ('Right "two")
+            '[ 'FT.Node ('Left 3)
+                '[ 'FT.Node ('Right "four") '[]]
+             ]
+         , 'FT.Node ('Left 5)
+            '[ 'FT.Node ('Right "six") '[]
+             ]
+         ]
     
-#if __GLASGOW_HASKELL__ >= 902
-testText :: forall r. (r ~ 'FTxt.Text "trial") => Bool
-testText = result == expected
-  where
-    result   = fromType @r Proxy :: DTxt.Text
-    expected = DTxt.pack "trial"
-#endif
+specTrees :: Spec
+specTrees = describe "Tree structures" $ do
+  it "tree 1" $ do
+    let test :: forall r. (r ~ ExTr1) 
+             => DT.Tree Int
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      DT.Node 1 [DT.Node 2 [DT.Node 3 [DT.Node 4 []]], DT.Node 5 [DT.Node 6 []]]
+  it "tree 2" $ do
+    let test :: forall r. (r ~ ExTr2) 
+             => DT.Tree (Maybe Int)
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      DT.Node (Just 1) 
+        [ DT.Node (Just 2) 
+          [ DT.Node (Just 3) 
+            [ DT.Node (Just 4) []
+            ]
+          ]
+        , DT.Node (Just 5) 
+          [DT.Node (Just 6) []
+          ]
+        ]
+  it "tree 3" $ do
+    let test :: forall r. (r ~ ExTr3) 
+             => DT.Tree (Maybe Int)
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      DT.Node (Just 1) 
+        [ DT.Node (Just 2) 
+          [ DT.Node (Just 3) 
+            [ DT.Node (Just 4) []
+            ]
+          ]
+        , DT.Node (Just 5) 
+          [DT.Node Nothing []
+          ]
+        ]
+  it "tree 4" $ do
+    let test :: forall r. (r ~ ExTr4) 
+             => DT.Tree (Either Int String)
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      DT.Node (Left 1) 
+        [ DT.Node (Right "two") 
+          [ DT.Node (Left 3) 
+            [ DT.Node (Right "four") []
+            ]
+          ]
+        , DT.Node (Left 5) 
+          [DT.Node (Right "six") []
+          ]
+        ]
diff --git a/test/Test/Data/Set.hs b/test/Test/Data/Set.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Data/Set.hs
@@ -0,0 +1,221 @@
+{-# LANGUAGE CPP                    #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE DataKinds              #-}
+{-# OPTIONS_GHC -Wall                       #-}
+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
+
+module Test.Data.Set where
+
+import           Data.Proxy
+import           Data.Type.Equality ((:~:)(Refl))
+import           Test.Hspec (describe, it, shouldBe, Spec)
+import qualified Data.Set as DS
+
+import           Fcf (Eval, type (=<<), Map)
+import           Fcf.Data.Nat
+import           Fcf.Data.Set
+import           Fcf.Data.Reflect (fromType)
+import           Fcf.Alg.Sort
+
+--------------------------------------------------------------------------------
+
+-- > :kind! Eval (Size =<< FromList '[5, 3])
+-- Eval (Size =<< FromList '[5, 3]) :: TL.Natural
+-- = 2
+
+spec :: Spec
+spec = describe "Set" $ do
+  it "PowerSet" $ do
+    let test :: forall r. (r ~ Eval (PowerSet  =<< FromList '[1,2,9,5])) => DS.Set (DS.Set Int)
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      DS.powerSet (DS.fromList [1,2,9,5])
+  it "Size" $ do
+    let test :: forall r. (r ~ Eval (Size  =<< FromList '[5,3])) => Int
+        test = fromType (Proxy @r)
+    test `shouldBe` 2
+
+--------------------------------------------------------------------------------
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--
+-- > :kind! (Eval Empty :: Set Nat)
+-- (Eval Empty :: Set Nat) :: Set TL.Natural
+-- = 'Set '[]
+_ = Refl :: (Eval Empty :: Set Nat)
+  :~: 'Set '[]
+
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--
+-- > :kind! Eval (Singleton 1)
+-- Eval (Singleton 1) :: Set TL.Natural
+-- = 'Set '[1]
+_ = Refl :: Eval (Singleton 1)
+  :~: 'Set '[1]
+
+
+-- > :kind! Eval (Insert 3 =<< FromList '[1, 2])
+-- Eval (Insert 3 =<< FromList '[1, 2]) :: Set TL.Natural
+-- = 'Set '[3, 1, 2]
+_ = Refl :: Eval (Insert 3 =<< FromList '[1, 2])
+  :~: 'Set '[3, 1, 2]
+
+-- > :kind! Eval (Insert 2 =<< FromList '[1, 2])
+-- Eval (Insert 2 =<< FromList '[1, 2]) :: Set TL.Natural
+-- = 'Set '[1, 2]
+_ = Refl :: Eval (Insert 2 =<< FromList '[1, 2])
+  :~: 'Set '[1, 2]
+
+-- > :kind! Eval (Delete 5 =<< FromList '[5, 3])
+-- Eval (Delete 5 =<< FromList '[5, 3]) :: Set TL.Natural
+-- = 'Set '[3]
+_ = Refl :: Eval (Delete 5 =<< FromList '[5, 3])
+  :~: 'Set '[3]
+
+-- > :kind! Eval (Delete 7 =<< FromList '[5, 3])
+-- Eval (Delete 7 =<< FromList '[5, 3]) :: Set TL.Natural
+-- = 'Set '[5, 3]
+_ = Refl :: Eval (Delete 7 =<< FromList '[5, 3])
+  :~: 'Set '[5, 3]
+
+-- > :kind! Eval (Member 5 =<< FromList '[5, 3])
+-- Eval (Member 5 =<< FromList '[5, 3]) :: Bool
+-- = 'True
+_ = Refl :: Eval (Member 5 =<< FromList '[5, 3])
+  :~: 'True
+
+-- > :kind! Eval (Member 7 =<< FromList '[5, 3])
+-- Eval (Member 7 =<< FromList '[5, 3]) :: Bool
+-- = 'False
+_ = Refl :: Eval (Member 7 =<< FromList '[5, 3])
+  :~: 'False
+
+-- > :kind! Eval (NotMember 5 =<< FromList '[5, 3])
+-- Eval (NotMember 5 =<< FromList '[5, 3]) :: Bool
+-- = 'False
+_ = Refl :: Eval (NotMember 5 =<< FromList '[5, 3])
+  :~: 'False
+
+
+-- > :kind! Eval (NotMember 7 =<< FromList '[5, 3])
+-- Eval (NotMember 7 =<< FromList '[5, 3]) :: Bool
+-- = 'True
+_ = Refl :: Eval (NotMember 7 =<< FromList '[5, 3])
+  :~: 'True
+
+-- > :kind! Eval (Null =<< FromList '[5, 3])
+-- Eval (Null =<< FromList '[5, 3]) :: Bool
+-- = 'False
+_ = Refl :: Eval (Null =<< FromList '[5, 3])
+  :~: 'False
+
+-- > :kind! Eval (Null =<< Empty)
+-- Eval (Null =<< Empty) :: Bool
+-- = 'True
+_ = Refl :: Eval (Null =<< Empty)
+  :~: 'True
+
+-- > :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))
+-- Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'True
+_ = Refl :: Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))
+  :~: 'True
+
+-- > :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))
+-- Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'True
+_ = Refl :: Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))
+  :~: 'True
+
+-- > :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4]))
+-- Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'True
+_ = Refl :: Eval (IsSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))
+  :~: 'True
+
+-- > :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))
+-- Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'False
+_ = Refl :: Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))
+  :~: 'False
+
+-- > :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))
+-- Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'False
+_ = Refl :: Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))
+  :~: 'False
+
+-- > :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))
+-- Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'True
+_ = Refl :: Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))
+  :~: 'True
+
+-- > :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )
+-- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set
+--                                                                        TL.Natural
+-- = 'Set '[7, 5, 3]
+_ = Refl ::  Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )
+  :~: 'Set '[7, 5, 3]
+
+-- > :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
+-- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set
+--                                                                            TL.Natural
+-- = 'Set '[3]
+_ = Refl :: Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
+  :~: 'Set '[3]
+
+-- > :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
+-- Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set
+--                                                                              TL.Natural
+-- = 'Set '[5]
+_ = Refl :: Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) 
+  :~: 'Set '[5]
+
+-- > :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])
+-- Eval (PowerSet =<< FromList '["a", "b", "c"]) :: Set
+--                                                    (Set TL.Symbol)
+-- = 'Set
+--     '[ 'Set '[], 'Set '["c"], 'Set '["b"], 'Set '["b", "c"],
+--        'Set '["a"], 'Set '["a", "b"], 'Set '["a", "c"],
+--        'Set '["a", "b", "c"]]
+--
+-- > :kind! Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])
+-- Eval (PowerSet =<< FromList '[Int, Char, Maybe Int]) :: Set
+--                                                           (Set (*))
+-- = 'Set
+--     '[ 'Set '[], 'Set '[Maybe Int], 'Set '[Char],
+--        'Set '[Char, Maybe Int], 'Set '[Int], 'Set '[Int, Char],
+--        'Set '[Int, Maybe Int], 'Set '[Int, Char, Maybe Int]]
+_ = Refl :: Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])
+  :~: 'Set
+    '[ 'Set '[], 'Set '[Maybe Int], 'Set '[Char],
+       'Set '[Char, Maybe Int], 'Set '[Int], 'Set '[Int, Char],
+       'Set '[Int, Maybe Int], 'Set '[Int, Char, Maybe Int]]
+
+-- > :kind! Eval (FromList '[1, 2])
+-- Eval (FromList '[1, 2]) :: Set TL.Natural
+-- = 'Set '[1, 2]
+_ = Refl :: Eval (FromList '[1, 2])
+  :~: 'Set '[1, 2]
+
+-- > :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])
+-- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set
+--                                                        TL.Natural]
+-- = '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],
+--      'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]
+_ = Refl :: Eval (ToList =<< PowerSet =<< FromList '[1,2,3])
+  :~: '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],
+         'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]
+
+-- > :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])
+-- Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3]) :: [[TL.Natural]]
+-- = '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]]
+_ = Refl :: Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])
+  :~: '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]]
diff --git a/test/test.hs b/test/test.hs
--- a/test/test.hs
+++ b/test/test.hs
@@ -1,34 +1,33 @@
 {-# LANGUAGE
     DataKinds,
     KindSignatures,
+    TypeFamilies,
+    UndecidableInstances,
     TypeOperators #-}
 
 --------------------------------------------------------------------------------
 
 import           Data.Type.Equality ((:~:)(Refl))
-import           GHC.TypeLits (Nat)
-import           Fcf
+import           GHC.TypeLits (Nat, Symbol)
+import           Fcf hiding (type (<*>))
 
 --------------------------------------------------------------------------------
 
 import           Fcf.Data.Set
+import           Fcf.Control.Monad
+import           Fcf.Data.Tuple
+import           Fcf.Class.Monoid
+import           Fcf.Data.List
 
 --------------------------------------------------------------------------------
 
-import           Test.Data (tests)
-
-
-
--- Compile-time tests
-
-_ = Refl :: Eval (ToList =<< PowerSet  =<< FromList '[1,2])
-        :~: '[ 'Set '[], 'Set '[2], 'Set '[1], 'Set '[1,2]]
-
--- Dummy
+import           Test.Alg as A (spec)
+import           Test.Data as D (spec)
+import           Test.Control as C (spec)
+import           Test.Hspec (hspec, parallel)
 
 main :: IO ()
-main = 
-  if tests 
-    then pure ()
-    else error "Tests not ok."
-
+main = hspec $ parallel $ do
+  D.spec
+  C.spec
+  A.spec