diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,4 +1,20 @@
 
+# 0.8.2
+
+Thank you again to Skyfold (Martin P.)
+
+- Deprecation warning for the KnownNats class and its instances: the KnownVal
+  can be used instead.
+- Instances to IntMap, Map and Set to convert directly from '[a] or '[ '(key,val) ]
+- The ErrorMessage instance for KnownVal to show information about types 
+- Add KnownVal instance for typeable types, this can be used as Show for
+  the types presented at the kind level. 
+- Fix the Test.Alg test description
+- Remove doc-tests from all Fcf.Alg modules and write the corresponding test modules
+- Some cleaning
+- Add depracation and warning pragmas to text modules.
+
+
 # 0.8.1
 
 20230410
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -56,18 +56,38 @@
 cabal test 
 ```
 
-The doc-tests both document and work as main testing mechanism for this lib. 
+If you are flakes user, `nix develop -c zsh` (or without that `-c zsh`) works as well.
 
+The doc-tests both document and work partly as testing mechanism for this lib. Please 
+do note that we are moving away from the doc-tests and building the testing modules 
+under `test` directory.
+
 If you don't use nix, `cabal install fcf-containers` should be enough. This
 package has almost as good number of dependencies as the first-class-families.
 
 
 ## Example
 
+
+### Test cases as examples
+
 The  
 [test directory](https://github.com/gspia/fcf-containers/blob/master/test)
-contains a lot of useful examples.
+contains a lot of useful examples.  There you will find out, how to apply most
+of the methods: examples that only work on "compile time", and examples on how
+to get the results from type level calculations to value level (see the Reflect
+test module and the `fromType` method applications, also in some other testing
+modules).
 
+
+### Three example programs calculating something
+
+These are a bit larger examples, but not yet too large: somewhat convenient small 
+module size.  Idea was to take an algorithm, and convert it to a type-level 
+computation, or in some other way give an example of methods that this library
+provides.
+
+
 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.
@@ -76,12 +96,18 @@
 cabal run orbits 
 ```
 
-There is also another example that show how to use MapC, see
+There is also another Advent of Code problem, see the Carbcombat file.
+
+
+To see, how to use MapC, take a look at
 [Haiku.hs](https://github.com/gspia/fcf-containers/blob/master/examples/Haiku.hs)
 
 ```
 cabal run haiku 
 ```
+
+
+### Other example material
 
 Please, do take a look of the notes made for the Helsinki Haskell meetup
 on 11th January 2023
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.1
+Version:             0.8.2
 Build-type:          Simple
 Author:              gspia
 Maintainer:          iahogsp@gmail.com
@@ -96,11 +96,17 @@
   default-language:    Haskell2010
   other-modules:       Test.Alg
                      , Test.Alg.List
+                     , Test.Alg.Morphism
+                     , Test.Alg.Nat
+                     , Test.Alg.Other
+                     , Test.Alg.Sort
+                     , Test.Alg.Symbol
+                     , Test.Alg.Tree
+                     , Test.Control
+                     , Test.Control.Monad
                      , Test.Data
                      , Test.Data.Reflect
                      , Test.Data.Set
-                     , Test.Control
-                     , Test.Control.Monad
   build-depends:
       base
     , first-class-families
@@ -108,6 +114,8 @@
     , hspec
     , containers
     , text
+--  ghc-options:
+--      -freduction-depth=0
 
 test-suite fcf-doctest
   type:                exitcode-stdio-1.0
diff --git a/flake.nix b/flake.nix
--- a/flake.nix
+++ b/flake.nix
@@ -13,6 +13,8 @@
       # filter = import nix-filter { };
 
       ghcVersion = "925";
+      # ghcVersion = "92";
+      # ghcVersion = "902";
 
       src = nix-filter.lib {
         root = ./.;
@@ -65,5 +67,6 @@
         library = fcf-containers;
         # packages.x86_64-linux.default = ;
         devShell.x86_64-linux = shell;
+        inherit pkgs;
       };
 }
diff --git a/src/Fcf/Alg/Morphism.hs b/src/Fcf/Alg/Morphism.hs
--- a/src/Fcf/Alg/Morphism.hs
+++ b/src/Fcf/Alg/Morphism.hs
@@ -32,15 +32,6 @@
 
 --------------------------------------------------------------------------------
 
--- For the doctests:
-
--- $setup
--- >>> import qualified GHC.TypeLits as TL
--- >>> import           Fcf.Alg.List
--- >>> import           Fcf.Data.Nat
-
---------------------------------------------------------------------------------
-
 -- | Structure that 'Cata' can fold and that is a result structure of 'Ana'.
 newtype Fix f = Fix (f (Fix f))
 
@@ -68,15 +59,15 @@
 --
 -- === __Example__
 --
--- >>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat
--- >>> :{
+-- > data NToOneCoA :: CoAlgebra (ListF Nat) Nat
+-- > :{
 --   type instance Eval (NToOneCoA b) =
 --     If (Eval (b < 1) )
 --         'NilF
 --         ('ConsF b ( b TL.- 1))
 -- :}
 --
--- >>> :kind! Eval (Ana NToOneCoA 3)
+-- > :kind! Eval (Ana NToOneCoA 3)
 -- Eval (Ana NToOneCoA 3) :: Fix (ListF TL.Natural)
 -- = 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))
 data Ana :: CoAlgebra f a -> a -> Exp (Fix f)
@@ -89,15 +80,15 @@
 --
 -- === __Example__
 --
--- >>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat
--- >>> :{
+-- > data NToOneCoA :: CoAlgebra (ListF Nat) Nat
+-- > :{
 --   type instance Eval (NToOneCoA b) =
 --     If (Eval (b < 1) )
 --         'NilF
 --         ('ConsF b ( b TL.- 1))
 -- :}
 --
--- >>> :kind! Eval (Hylo SumAlg NToOneCoA 5)
+-- > :kind! Eval (Hylo SumAlg NToOneCoA 5)
 -- Eval (Hylo SumAlg NToOneCoA 5) :: TL.Natural
 -- = 15
 data Hylo :: Algebra f a -> CoAlgebra f b -> b -> Exp a
@@ -183,7 +174,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (First ((+) 1) '(3,"a"))
+-- > :kind! Eval (First ((+) 1) '(3,"a"))
 -- Eval (First ((+) 1) '(3,"a")) :: (TL.Natural, TL.Symbol)
 -- = '(4, "a")
 data First :: (a -> Exp b) -> f a c -> Exp (f b c)
@@ -199,7 +190,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Second ((+) 1) '("a",3))
+-- > :kind! Eval (Second ((+) 1) '("a",3))
 -- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, TL.Natural)
 -- = '("a", 4)
 data Second :: (c -> Exp d) -> f a c -> Exp (f a d)
@@ -210,4 +201,3 @@
 -- Either
 type instance Eval (Second f ('Left a)) = 'Left a
 type instance Eval (Second f ('Right b)) = 'Right (f @@ b)
-
diff --git a/src/Fcf/Alg/Other.hs b/src/Fcf/Alg/Other.hs
--- a/src/Fcf/Alg/Other.hs
+++ b/src/Fcf/Alg/Other.hs
@@ -26,19 +26,11 @@
 
 --------------------------------------------------------------------------------
 
--- For the doctests:
-
--- $setup
--- >>> import           GHC.Types
--- >>> import qualified GHC.TypeLits as TL
-
---------------------------------------------------------------------------------
-
 -- | Helper.
 --
 -- === __Example__
 --
--- >>> :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1))
+-- > :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1))
 -- Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) :: Maybe
 --                                                           (Symbol, TL.Natural)
 -- = 'Just '("txt", 1)
@@ -52,9 +44,8 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Id "id")
+-- > :kind! Eval (Id "id")
 -- Eval (Id "id") :: Symbol
 -- = "id"
 data Id :: a -> Exp a
 type instance Eval (Id a) = a
-
diff --git a/src/Fcf/Alg/Sort.hs b/src/Fcf/Alg/Sort.hs
--- a/src/Fcf/Alg/Sort.hs
+++ b/src/Fcf/Alg/Sort.hs
@@ -36,14 +36,6 @@
 
 --------------------------------------------------------------------------------
 
--- For the doctests:
-
--- $setup
--- >>> import qualified Fcf.Data.Nat as N ( type (<) )
--- >>> import qualified Fcf.Alg.Symbol as S ( type (<) )
-
---------------------------------------------------------------------------------
-
 -- helper for the ListCmp
 data ListCmpFnd :: [Ordering] -> Exp Ordering
 type instance Eval (ListCmpFnd '[]) = 'EQ
@@ -106,11 +98,11 @@
 --
 -- __Example__
 --
--- >>> :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3])
+-- > :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3])
 -- Eval (Qsort (N.<) '[5,3,1,9,4,6,3]) :: [TL.Natural]
 -- = '[1, 3, 3, 4, 5, 6, 9]
 --
--- >>> :kind! Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])
+-- > :kind! Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])
 -- Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ]) :: [Symbol]
 -- = '["a", "bb", "d", "e", "e"]
 data Qsort :: (a -> a -> Exp Bool) -> [a] -> Exp [a]
@@ -122,4 +114,3 @@
 -- Nat-list. Sorting would work without PartCmp.
 data PartCmp :: (a -> a -> Exp Bool) -> CoAlgebra (BTreeF a) [a] 
 type instance Eval (PartCmp cmp coalg) = Eval (PartHlp (Flip cmp) coalg)
-
diff --git a/src/Fcf/Alg/Symbol.hs b/src/Fcf/Alg/Symbol.hs
--- a/src/Fcf/Alg/Symbol.hs
+++ b/src/Fcf/Alg/Symbol.hs
@@ -71,7 +71,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Append "hmm" " ok")
+-- > :kind! Eval (Append "hmm" " ok")
 -- Eval (Append "hmm" " ok") :: Symbol
 -- = "hmm ok"
 data Append :: Symbol -> Symbol -> Exp Symbol
@@ -82,15 +82,15 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Intercalate "+" '["aa", "bb", "cc"])
+-- > :kind! Eval (Intercalate "+" '["aa", "bb", "cc"])
 -- Eval (Intercalate "+" '["aa", "bb", "cc"]) :: Symbol
 -- = "aa+bb+cc"
 --
--- >>> :kind! Eval (Intercalate "+" '["aa"])
+-- > :kind! Eval (Intercalate "+" '["aa"])
 -- Eval (Intercalate "+" '["aa"]) :: Symbol
 -- = "aa"
 --
--- >>> :kind! Eval (Intercalate "+" '[])
+-- > :kind! Eval (Intercalate "+" '[])
 -- Eval (Intercalate "+" '[]) :: Symbol
 -- = ""
 data Intercalate :: Symbol -> [Symbol] -> Exp Symbol
@@ -107,11 +107,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (IsSpace "a")
+-- > :kind! Eval (IsSpace "a")
 -- Eval (IsSpace "a") :: Bool
 -- = 'False
 --
--- >>> :kind! Eval (IsSpace " ")
+-- > :kind! Eval (IsSpace " ")
 -- Eval (IsSpace " ") :: Bool
 -- = 'True
 data IsSpace :: Symbol -> Exp Bool
@@ -122,11 +122,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (IsNewLine "a")
+-- > :kind! Eval (IsNewLine "a")
 -- Eval (IsNewLine "a") :: Bool
 -- = 'False
 --
--- >>> :kind! Eval (IsNewLine "\n")
+-- > :kind! Eval (IsNewLine "\n")
 -- Eval (IsNewLine "\n") :: Bool
 -- = 'True
 data IsNewLine :: Symbol -> Exp Bool
@@ -137,11 +137,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (IsTab "a")
+-- > :kind! Eval (IsTab "a")
 -- Eval (IsTab "a") :: Bool
 -- = 'False
 --
--- >>> :kind! Eval (IsTab "\t")
+-- > :kind! Eval (IsTab "\t")
 -- Eval (IsTab "\t") :: Bool
 -- = 'True
 data IsTab :: Symbol -> Exp Bool
@@ -152,11 +152,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (IsSpaceDelim "a")
+-- > :kind! Eval (IsSpaceDelim "a")
 -- Eval (IsSpaceDelim "a") :: Bool
 -- = 'False
 --
--- >>> :kind! Eval (IsSpaceDelim "\n")
+-- > :kind! Eval (IsSpaceDelim "\n")
 -- Eval (IsSpaceDelim "\n") :: Bool
 -- = 'True
 data IsSpaceDelim :: Symbol -> Exp Bool
@@ -168,11 +168,11 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (IsDigit "3")
+-- > :kind! Eval (IsDigit "3")
 -- Eval (IsDigit "3") :: Bool
 -- = 'True
 --
--- >>> :kind! Eval (IsDigit "a")
+-- > :kind! Eval (IsDigit "a")
 -- Eval (IsDigit "a") :: Bool
 -- = 'False
 data IsDigit :: Symbol -> Exp Bool
@@ -189,7 +189,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval (SymbolOrd "a" "b")
+-- > :kind! Eval (SymbolOrd "a" "b")
 -- Eval (SymbolOrd "a" "b") :: Ordering
 -- = 'LT
 data SymbolOrd :: Symbol -> Symbol -> Exp Ordering
@@ -199,10 +199,9 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval ("b" <= "a")
+-- > :kind! Eval ("b" <= "a")
 -- Eval ("b" <= "a") :: Bool
 -- = 'False
---
 data (<=) :: Symbol -> Symbol -> Exp Bool
 type instance Eval ((<=) a b) =
     Eval (Eval (TyEq (TL.CmpSymbol a b) 'LT) || Eval (TyEq (TL.CmpSymbol a b) 'EQ))
@@ -211,7 +210,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval ("b" >= "a")
+-- > :kind! Eval ("b" >= "a")
 -- Eval ("b" >= "a") :: Bool
 -- = 'True
 data (>=) :: Symbol -> Symbol -> Exp Bool
@@ -222,7 +221,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval ("a" < "b")
+-- > :kind! Eval ("a" < "b")
 -- Eval ("a" < "b") :: Bool
 -- = 'True
 data (<) :: Symbol -> Symbol -> Exp Bool
@@ -232,7 +231,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval ("b" > "a")
+-- > :kind! Eval ("b" > "a")
 -- Eval ("b" > "a") :: Bool
 -- = 'True
 data (>) :: Symbol -> Symbol -> Exp Bool
@@ -242,7 +241,7 @@
 --
 -- === __Example__
 --
--- >>> :kind! Eval ("b" == "a")
+-- > :kind! Eval ("b" == "a")
 -- Eval ("b" == "a") :: Bool
 -- = 'False
 data (==) :: Symbol -> Symbol -> Exp Bool
diff --git a/src/Fcf/Alg/Tree.hs b/src/Fcf/Alg/Tree.hs
--- a/src/Fcf/Alg/Tree.hs
+++ b/src/Fcf/Alg/Tree.hs
@@ -75,15 +75,15 @@
 -- Size is defined as @ Cata CountNodesAlg =<< TreeToFix tr @
 -- and can be used with the following.
 --
--- >>> data BuildNode :: Nat -> Exp (Nat,[Nat])
--- >>> :{
+-- > data BuildNode :: Nat -> Exp (Nat,[Nat])
+-- > :{
 --   type instance Eval (BuildNode x) =
 --       If (Eval ((2 TL.* x TL.+ 1) >= 8))
 --           '(x, '[])
 --           '(x, '[ 2 TL.* x, (2 TL.* x) TL.+ 1 ])
 -- :}
 --
--- >>> :kind! Eval (Size =<< UnfoldTree BuildNode 1)
+-- > :kind! Eval (Size =<< UnfoldTree BuildNode 1)
 -- Eval (Size =<< UnfoldTree BuildNode 1) :: TL.Natural
 -- = 7
 data Size :: Tree a -> Exp Nat
@@ -114,7 +114,7 @@
 --
 -- __Example__
 --
--- >>> :kind! Eval (FibHylo 10)
+-- > :kind! Eval (FibHylo 10)
 -- Eval (FibHylo 10) :: TL.Natural
 -- = 55
 data FibHylo :: Nat -> Exp Nat
@@ -147,7 +147,7 @@
 --
 -- __Example__
 --
--- >>> :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)
+-- > :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)
 -- Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix
 --                                          (AnnF (TreeF TL.Natural) TL.Natural)
 -- = 'Fix
@@ -208,10 +208,8 @@
 --
 -- __Example__
 --
--- >>> :kind! Eval (FibHisto 100)
+-- > :kind! Eval (FibHisto 100)
 -- Eval (FibHisto 100) :: TL.Natural
 -- = 354224848179261915075
 data FibHisto :: Nat -> Exp Nat
 type instance Eval (FibHisto n) = Eval (Histo FibAlgebra =<< NatToFix n)
-
-
diff --git a/src/Fcf/Data/OldText.hs b/src/Fcf/Data/OldText.hs
--- a/src/Fcf/Data/OldText.hs
+++ b/src/Fcf/Data/OldText.hs
@@ -6,7 +6,7 @@
 {-# OPTIONS_GHC -Werror=incomplete-patterns #-}
 
 {-|
-Module      : Fcf.Data.Text
+Module      : Fcf.Data.OldText
 Description : Type-level Text data structure with methods
 Copyright   : (c) gspia 2020-
 License     : BSD
@@ -25,6 +25,7 @@
 --------------------------------------------------------------------------------
 
 module Fcf.Data.OldText
+    {-# DEPRECATED "Use Fcf.Data.NewText instead" #-}
     ( Text (..)
 
     -- * Creation
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
@@ -31,7 +31,8 @@
 import           GHC.TypeLits (Nat, Symbol, KnownNat, KnownSymbol)
 import           Data.String (fromString, IsString)
 import           Data.Proxy
--- import qualified Data.Map.Strict as MS
+import           Data.Typeable (Typeable, typeRep)
+import           Data.Kind (Type)
 import qualified Data.Map as DM
 import qualified Data.IntMap.Strict as IMS
 import qualified Data.Set as S
@@ -39,7 +40,6 @@
 -- #endif
 import qualified Data.Tree as T
 
--- import qualified Fcf.Core as C (Eval)
 import qualified Fcf.Data.MapC as MC
 import qualified Fcf.Data.NatMap as NM
 import qualified Fcf.Data.Set as FS
@@ -50,15 +50,6 @@
 
 --------------------------------------------------------------------------------
 
--- For the doctests:
-
--- $setup
--- >>> import qualified GHC.TypeLits as TL
--- >>> import           Fcf.Data.Nat
-
---------------------------------------------------------------------------------
-
-
 -- | Reflect a list of Nats
 --
 -- Note that you may also use the KnownVal methods given below.
@@ -68,16 +59,18 @@
 --
 -- === __Example__
 --
--- >>> :{
+-- > :{
 -- afun :: forall n. (n ~ '[1,2,3,4]) => [Int]
 -- afun = natVals @n Proxy
 -- :}
 --
--- >>> afun
+-- > afun
 -- [1,2,3,4]
 class KnownNats (ns :: [Nat]) where
   natVals :: Proxy ns -> [Int]
 
+{-# DEPRECATED KnownNats "Replaced with KnownVal" #-}
+
 instance KnownNats '[] where
   natVals _ = []
 
@@ -95,27 +88,36 @@
 
 instance KnownVal Bool 'True where fromType _ = True
 instance KnownVal Bool 'False where fromType _ = False
+instance KnownVal () '() where fromType _ = ()
 
-instance (IsString str, KnownSymbol s) => KnownVal str (s :: Symbol )where
+instance (IsString str, KnownSymbol s) => KnownVal str (s :: Symbol) where
     fromType _ = fromString $ TL.symbolVal (Proxy @s)
 
+#if __GLASGOW_HASKELL__ >= 920
+instance (TL.KnownChar c) => KnownVal Char c where
+    fromType _ = TL.charVal (Proxy @c)
+#endif
+
+instance (IsString str, Typeable typ) => KnownVal str (typ :: Type) where
+    fromType = fromString . show . typeRep
+
 #if __GLASGOW_HASKELL__ >= 902
 
 -- | Text instance.
 --
 -- === __Example__
 --
--- >>> import qualified Data.Text as Txt
--- >>> :{
+-- > import qualified Data.Text as Txt
+-- > :{
 -- afun :: forall r. (r ~ 'FTxt.Text "hmm") => Txt.Text
 -- afun = fromType (Proxy @r)
 -- :}
 --
--- >>> afun
+-- > afun
 -- "hmm"
 instance (IsString str, KnownSymbol sym) => KnownVal str ('FTxt.Text sym)
   where
-    fromType _ = fromString $ fromType $ Proxy @sym 
+    fromType _ = fromType @str (Proxy @sym) 
 
 #endif
 
@@ -126,14 +128,14 @@
 instance KnownVal [a] '[] where
     fromType _ = []
 
-instance (KnownVal typ x, KnownVal [typ] xs) => KnownVal [typ] (x ': xs) where
+instance (KnownVal val x, KnownVal [val] xs) => KnownVal [val] (x ': xs) where
     fromType _ = fromType (Proxy @x) : fromType (Proxy @xs)
 
 --------------------------------------------------------------------------------
 
 -- Trees
 --
-instance (KnownVal typ k, KnownVal (T.Forest typ) trees) => KnownVal (T.Tree typ) ('FT.Node k trees)
+instance (KnownVal val k, KnownVal (T.Forest val) trees) => KnownVal (T.Tree val) ('FT.Node k trees)
   where
     fromType _ = T.Node (fromType (Proxy @k)) (fromType (Proxy @trees))
 
@@ -145,6 +147,10 @@
   where
     fromType _ = IMS.fromList (fromType (Proxy @pairs))
 
+instance (KnownVal [(Int,val)] pairs) => KnownVal (IMS.IntMap val) (pairs :: [(Nat, val')])
+  where
+    fromType _ = IMS.fromList (fromType (Proxy @pairs))
+
 --------------------------------------------------------------------------------
 
 -- Maps
@@ -153,13 +159,21 @@
   where
     fromType _ = DM.fromList (fromType (Proxy @pairs))
 
+instance (Ord key, KnownVal [(key,val)] pairs) => KnownVal (DM.Map key val) (pairs :: [(key',val')])
+  where
+    fromType _ = DM.fromList (fromType (Proxy @pairs))
+
 --------------------------------------------------------------------------------
 
 -- Set
 
-instance (Ord typ, KnownVal [typ] kind) => KnownVal (S.Set typ) ('FS.Set kind)
+instance (Ord val, KnownVal [val] kind) => KnownVal (S.Set val) ('FS.Set kind)
   where
     fromType _ = S.fromList (fromType (Proxy @kind))
+
+instance (Ord val, KnownVal [val] kind) => KnownVal (S.Set val) (kind :: [kind'])
+  where
+    fromType _ = S.fromList (fromType (Proxy @kind))
  
 --------------------------------------------------------------------------------
 
@@ -196,3 +210,19 @@
 
 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))
+
+--------------------------------------------------------------------------------
+
+-- ErrorMessage from GHC.TypeLits
+
+instance (IsString str, KnownSymbol sym) => KnownVal str ('TL.Text sym) where
+  fromType _ = fromType @str (Proxy @sym)
+
+instance (IsString str, Typeable typ) => KnownVal str ('TL.ShowType typ) where
+  fromType _ = fromString $ show $ typeRep (Proxy @typ)
+
+instance (IsString str, KnownVal str err1, KnownVal str err2, Semigroup str) => KnownVal str (err1 'TL.:<>: err2) where
+  fromType _ = fromType (Proxy @err1) <> fromType (Proxy @err2)
+
+instance (IsString str, KnownVal str err1, KnownVal str err2, Semigroup str) => KnownVal str (err1 'TL.:$$: err2) where
+  fromType _ = fromType (Proxy @err1) <> fromString "\n" <> fromType (Proxy @err2)
diff --git a/src/Fcf/Data/Text.hs b/src/Fcf/Data/Text.hs
--- a/src/Fcf/Data/Text.hs
+++ b/src/Fcf/Data/Text.hs
@@ -28,6 +28,7 @@
 --------------------------------------------------------------------------------
 
 module Fcf.Data.Text
+    {-# WARNING "This still uses the OldText implementaion, which will be replaced with NewText implementation." #-}
     ( Text (..)
 
     -- * Creation
diff --git a/test/Test/Alg.hs b/test/Test/Alg.hs
--- a/test/Test/Alg.hs
+++ b/test/Test/Alg.hs
@@ -1,10 +1,22 @@
 
 module Test.Alg where
 
-import           Test.Alg.List as L (spec)
+import           Test.Alg.List     as L (spec)
+import           Test.Alg.Morphism as M (spec)
+import           Test.Alg.Nat      as N (spec)
+import           Test.Alg.Other    as O (spec)
+import           Test.Alg.Sort     as So (spec)
+import           Test.Alg.Symbol   as Sy (spec)
+import           Test.Alg.Tree     as T (spec)
 import           Test.Hspec (describe, Spec)
 
 spec :: Spec
-spec = describe "Data"  
+spec = describe "Alg" $ do
   L.spec
+  M.spec
+  N.spec
+  O.spec
+  So.spec
+  Sy.spec
+  T.spec
 
diff --git a/test/Test/Alg/Morphism.hs b/test/Test/Alg/Morphism.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Alg/Morphism.hs
@@ -0,0 +1,85 @@
+{-# 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.Morphism 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.Morphism where
+
+import qualified GHC.TypeLits as TL
+
+import           Data.Proxy
+import           Data.Type.Equality ((:~:)(Refl))
+import           Test.Hspec (describe, it, shouldBe, Spec)
+
+import           Fcf.Core (Eval)
+import           Fcf.Utils (If)
+import           Fcf.Alg.List
+import           Fcf.Alg.Morphism
+import           Fcf.Data.Nat
+import           Fcf.Data.Reflect (fromType)
+
+--------------------------------------------------------------------------------
+
+-- For the Ana and Hylo tests made below.
+data NToOneCoA :: CoAlgebra (ListF Nat) Nat
+type instance Eval (NToOneCoA b) =
+  If (Eval (b < 1) )
+      'NilF
+      ('ConsF b ( b TL.- 1))
+
+
+-- This module won't compile, if the Refl doesn't give the correct answer.
+--
+-- > :kind! Eval (Ana NToOneCoA 3)
+-- Eval (Ana NToOneCoA 3) :: Fix (ListF TL.Natural)
+-- = 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))
+_ = Refl :: Eval (Ana NToOneCoA 3)
+  :~: 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))
+
+-- > :kind! Eval (Second ((+) 1) '("a",3))
+-- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, TL.Natural)
+-- = '("a", 4)
+_ = Refl :: Eval (Second ((+) 1) '("a",3))
+  :~: '("a", 4)
+
+
+-- > :kind! Eval (Hylo SumAlg NToOneCoA 5)
+-- Eval (Hylo SumAlg NToOneCoA 5) :: TL.Natural
+-- = 15
+
+-- > :kind! Eval (First ((+) 1) '(3,"a"))
+-- Eval (First ((+) 1) '(3,"a")) :: (TL.Natural, TL.Symbol)
+-- = '(4, "a")
+
+spec :: Spec
+spec = describe "Morphism" $ do
+  it "Hylo SumAlg" $ do
+    let test :: forall r. (r ~ Eval (Hylo SumAlg NToOneCoA 5)) => Int
+        test = fromType (Proxy @r)
+    test `shouldBe` 15
+  it "First" $ do
+    let test :: forall r. (r ~ Eval (First ((+) 1) '(3,"a"))) => (Int, String)
+        test = fromType (Proxy @r)
+    test `shouldBe` (4,"a")
diff --git a/test/Test/Alg/Nat.hs b/test/Test/Alg/Nat.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Alg/Nat.hs
@@ -0,0 +1,66 @@
+{-# 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.Nat 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.Nat where
+
+import           Data.Proxy
+import           Data.Type.Equality ((:~:)(Refl))
+import           Test.Hspec (describe, it, shouldBe, Spec)
+
+import           Fcf.Core (Eval)
+import           Fcf.Alg.Nat
+import           Fcf.Data.Reflect (fromType)
+
+-- > :kind! Eval (2 == 2)
+-- Eval (2 == 2) :: Bool
+-- = 'True
+_ = Refl :: Eval (2==2) :~: 'True
+
+-- > :kind! Eval (2 == 3)
+-- Eval (2 == 3) :: Bool
+-- = 'False
+_ = Refl :: Eval (2==3) :~: 'False
+
+
+-- > :kind! Eval (2 /= 2)
+-- Eval (2 /= 2) :: Bool
+-- = 'False
+--
+-- > :kind! Eval (2 /= 3)
+-- Eval (2 /= 3) :: Bool
+-- = 'True
+spec :: Spec
+spec = describe "Nat" $ do
+  it "In-equality, false" $ do
+    let test :: forall r. (r ~ Eval (2 /= 2)) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` False
+  it "In-equality, true" $ do
+    let test :: forall r. (r ~ Eval (2 /= 3)) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` True
diff --git a/test/Test/Alg/Other.hs b/test/Test/Alg/Other.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Alg/Other.hs
@@ -0,0 +1,54 @@
+{-# 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.Other 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.Other where
+
+import           Data.Proxy
+import           Data.Type.Equality ((:~:)(Refl))
+import           Test.Hspec (describe, it, shouldBe, Spec)
+
+import           Fcf.Core (Eval)
+import           Fcf.Alg.Other
+import           Fcf.Data.Reflect (fromType)
+
+-- > :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1))
+-- Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) :: Maybe
+--                                                           (Symbol, TL.Natural)
+-- = 'Just '("txt", 1)
+_ = Refl :: Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) 
+  :~: 'Just '("txt", 1)
+
+
+-- > :kind! Eval (Id "id")
+-- Eval (Id "id") :: Symbol
+-- = "id"
+spec :: Spec
+spec = describe "Other" $ do
+  it "Id" $ do
+    let test :: forall r. (r ~ Eval (Id "id")) => String
+        test = fromType (Proxy @r)
+    test `shouldBe` "id"
diff --git a/test/Test/Alg/Sort.hs b/test/Test/Alg/Sort.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Alg/Sort.hs
@@ -0,0 +1,56 @@
+{-# 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.Sort 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.Sort where
+
+import           Data.Proxy
+import           Data.Type.Equality ((:~:)(Refl))
+import           Test.Hspec (describe, it, shouldBe, Spec)
+
+import           Fcf.Core (Eval)
+import           Fcf.Alg.Sort
+import qualified Fcf.Alg.Symbol as S ( type (<) )
+import qualified Fcf.Data.Nat as N ( type (<) )
+import           Fcf.Data.Reflect (fromType)
+
+-- > :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3])
+-- Eval (Qsort (N.<) '[5,3,1,9,4,6,3]) :: [TL.Natural]
+-- = '[1, 3, 3, 4, 5, 6, 9]
+spec :: Spec
+spec = describe "Sort" $ do
+  it "QSort (<)" $ do
+    let test :: forall r. (r ~ Eval (Qsort (N.<) '[5,3,1,9,4,6,3])) => [Int]
+        test = fromType (Proxy @r)
+    test `shouldBe` [1, 3, 3, 4, 5, 6, 9]
+
+-- > :kind! Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])
+-- Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ]) :: [Symbol]
+-- = '["a", "bb", "d", "e", "e"]
+_ = Refl :: Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])
+  :~: '["a", "bb", "d", "e", "e"]
+
diff --git a/test/Test/Alg/Symbol.hs b/test/Test/Alg/Symbol.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Alg/Symbol.hs
@@ -0,0 +1,157 @@
+{-# 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.Symbol 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.Symbol where
+
+import           Data.Proxy
+import           Data.Type.Equality ((:~:)(Refl))
+import           Test.Hspec (describe, it, shouldBe, Spec)
+
+import           Fcf.Core (Eval)
+import           Fcf.Alg.Symbol
+import           Fcf.Data.Reflect (fromType)
+
+-- > :kind! Eval (Append "hmm" " ok")
+-- Eval (Append "hmm" " ok") :: Symbol
+-- = "hmm ok"
+_ = Refl :: Eval (Append "hmm" " ok") :~: "hmm ok"
+
+-- > :kind! Eval (Intercalate "+" '["aa", "bb", "cc"])
+-- Eval (Intercalate "+" '["aa", "bb", "cc"]) :: Symbol
+-- = "aa+bb+cc"
+_ = Refl :: Eval (Intercalate "+" '["aa", "bb", "cc"]) :~: "aa+bb+cc"
+
+-- > :kind! Eval (Intercalate "+" '["aa"])
+-- Eval (Intercalate "+" '["aa"]) :: Symbol
+-- = "aa"
+_ = Refl :: Eval (Intercalate "+" '["aa"]) :~: "aa"
+
+-- > :kind! Eval (Intercalate "+" '[])
+-- Eval (Intercalate "+" '[]) :: Symbol
+-- = ""
+_ = Refl :: Eval (Intercalate "+" '[]) :~: ""
+
+-- > :kind! Eval (IsSpace "a")
+-- Eval (IsSpace "a") :: Bool
+-- = 'False
+_ = Refl :: Eval (IsSpace "a") :~: 'False
+--
+-- > :kind! Eval (IsSpace " ")
+-- Eval (IsSpace " ") :: Bool
+-- = 'True
+_ = Refl :: Eval (IsSpace " ") :~: 'True
+
+-- > :kind! Eval (IsNewLine "a")
+-- Eval (IsNewLine "a") :: Bool
+-- = 'False
+_ = Refl :: Eval (IsNewLine "a") :~: 'False
+
+-- > :kind! Eval (IsNewLine "\n")
+-- Eval (IsNewLine "\n") :: Bool
+-- = 'True
+_ = Refl :: Eval (IsNewLine "\n") :~: 'True
+
+-- > :kind! Eval (IsTab "a")
+-- Eval (IsTab "a") :: Bool
+-- = 'False
+_ = Refl :: Eval (IsTab "a") :~: 'False
+--
+-- > :kind! Eval (IsTab "\t")
+-- Eval (IsTab "\t") :: Bool
+-- = 'True
+_ = Refl :: Eval (IsTab "\t") :~: 'True
+
+-- > :kind! Eval (IsSpaceDelim "a")
+-- Eval (IsSpaceDelim "a") :: Bool
+-- = 'False
+_ = Refl :: Eval (IsSpaceDelim "a") :~: 'False
+--
+-- > :kind! Eval (IsSpaceDelim "\n")
+-- Eval (IsSpaceDelim "\n") :: Bool
+-- = 'True
+_ = Refl :: Eval (IsSpaceDelim "\n") :~: 'True
+
+-- > :kind! Eval (IsDigit "3")
+-- Eval (IsDigit "3") :: Bool
+-- = 'True
+_ = Refl :: Eval (IsDigit "3") :~: 'True
+--
+-- > :kind! Eval (IsDigit "a")
+-- Eval (IsDigit "a") :: Bool
+-- = 'False
+_ = Refl :: Eval (IsDigit "a") :~: 'False
+
+-- > :kind! Eval (SymbolOrd "a" "b")
+-- Eval (SymbolOrd "a" "b") :: Ordering
+-- = 'LT
+_ = Refl :: Eval (SymbolOrd "a" "b") :~: 'LT
+
+--------------------------------------------------------------------------------
+
+-- > :kind! Eval ("b" <= "a")
+-- Eval ("b" <= "a") :: Bool
+-- = 'False
+--
+-- > :kind! Eval ("b" >= "a")
+-- Eval ("b" >= "a") :: Bool
+-- = 'True
+--
+-- > :kind! Eval ("a" < "b")
+-- Eval ("a" < "b") :: Bool
+-- = 'True
+--
+-- > :kind! Eval ("b" > "a")
+-- Eval ("b" > "a") :: Bool
+-- = 'True
+--
+-- > :kind! Eval ("b" == "a")
+-- Eval ("b" == "a") :: Bool
+-- = 'False
+spec :: Spec
+spec = describe "Symbol" $ do
+  it "<=" $ do
+    let test :: forall r. (r ~ Eval ("b" <= "a")) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` False
+  it ">=" $ do
+    let test :: forall r. (r ~ Eval ("b" >= "a")) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` True
+  it "<" $ do
+    let test :: forall r. (r ~ Eval ("b" < "a")) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` False
+  it ">" $ do
+    let test :: forall r. (r ~ Eval ("b" > "a")) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` True
+  it "==" $ do
+    let test :: forall r. (r ~ Eval ("b" == "a")) => Bool
+        test = fromType (Proxy @r)
+    test `shouldBe` False
+    
diff --git a/test/Test/Alg/Tree.hs b/test/Test/Alg/Tree.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Alg/Tree.hs
@@ -0,0 +1,129 @@
+{-# 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.Tree 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.Tree where
+
+import qualified GHC.TypeLits as TL
+
+import           Data.Proxy
+import           Data.Type.Equality ((:~:)(Refl))
+import           Test.Hspec (describe, it, shouldBe, Spec)
+
+import           Fcf.Data.Nat
+
+import           Fcf.Alg.Morphism 
+import           Fcf.Alg.Tree
+import           Fcf.Combinators (type (=<<))
+import           Fcf.Core (Eval, Exp)
+import           Fcf.Utils (If)
+import           Fcf.Data.Reflect (fromType)
+import           Fcf.Data.Tree
+
+data BuildNode :: Nat -> Exp (Nat,[Nat])
+type instance Eval (BuildNode x) =
+    If (Eval ((2 TL.* x TL.+ 1) >= 8))
+        '(x, '[])
+        '(x, '[ 2 TL.* x, (2 TL.* x) TL.+ 1 ])
+
+-- > :kind! Eval (Size =<< UnfoldTree BuildNode 1)
+-- Eval (Size =<< UnfoldTree BuildNode 1) :: TL.Natural
+-- = 7
+_ = Refl :: Eval (Size =<< UnfoldTree BuildNode 1) :~: 7
+
+
+-- :kind! Eval (Ana BuildNodeCoA 1)
+-- :kind! Eval (Hylo CountNodesAlg BuildNodeCoA 1)
+
+
+-- > :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)
+-- Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix
+--                                          (AnnF (TreeF TL.Natural) TL.Natural)
+-- = 'Fix
+--     ('AnnF
+--        '( 'NodeF
+--             1
+--             '[ 'Fix
+--                  ('AnnF
+--                     '( 'NodeF
+--                          2
+--                          '[ 'Fix ('AnnF '( 'NodeF 4 '[], 1)),
+--                             'Fix ('AnnF '( 'NodeF 5 '[], 1))],
+--                        3)),
+--                'Fix
+--                  ('AnnF
+--                     '( 'NodeF
+--                          3
+--                          '[ 'Fix ('AnnF '( 'NodeF 6 '[], 1)),
+--                             'Fix ('AnnF '( 'NodeF 7 '[], 1))],
+--                        3))],
+--           7))
+_ = Refl :: Eval (Sizes =<< Ana BuildNodeCoA 1)
+  :~: 'Fix
+    ('AnnF
+       '( 'NodeF
+            1
+            '[ 'Fix
+                 ('AnnF
+                    '( 'NodeF
+                         2
+                         '[ 'Fix ('AnnF '( 'NodeF 4 '[], 1)),
+                            'Fix ('AnnF '( 'NodeF 5 '[], 1))],
+                       3)),
+               'Fix
+                 ('AnnF
+                    '( 'NodeF
+                         3
+                         '[ 'Fix ('AnnF '( 'NodeF 6 '[], 1)),
+                            'Fix ('AnnF '( 'NodeF 7 '[], 1))],
+                       3))],
+          7))
+
+-- Turning this off, because of the slowness. In practice, this would
+-- also require turning on ghc-options (-freduction-depth=0). 
+-- Please, do try on ghci.
+-- > :kind! Eval (FibHisto 100)
+-- Eval (FibHisto 100) :: TL.Natural
+-- = 354224848179261915075
+-- _ = Refl :: Eval (FibHisto 100) :~: 354224848179261915075
+
+-- > :kind! Eval (FibHylo 10)
+-- Eval (FibHylo 10) :: TL.Natural
+-- = 55
+spec :: Spec
+spec = describe "Tree" $ do
+  it "FibHisto" $ do
+    let test :: forall r. (r ~ Eval (FibHylo 10)) => Int
+        test = fromType (Proxy @r)
+    test `shouldBe` 55
+  -- The following is very slow and would require turning on ghc-options
+  -- (-freduction-depth=0).  
+  -- it "FibHisto" $ do
+  --   let test :: forall r. (r ~ Eval (FibHisto 100)) => Integer
+  --       test = fromType (Proxy @r)
+  --   test `shouldBe` 354224848179261915075
+
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
@@ -14,9 +14,8 @@
 import qualified Data.Map as DM
 import qualified Data.Set as DS
 import qualified Data.Tree as DT
-#if __GLASGOW_HASKELL__ >= 902
 import qualified Data.Text as DTxt
-#endif
+import qualified GHC.TypeLits as TL
 import           Data.Proxy
 import           Test.Hspec (describe, it, shouldBe, Spec)
 
@@ -34,11 +33,13 @@
 
 spec :: Spec
 spec = describe "Reflect" $ do
+  specTrees
   specMaybe
   specEither
   specMaybeEither
   specStructures
-  specTrees
+  specShowTypeable
+  specErrorMessage
   
 specBool :: Spec
 specBool = describe "Bool" $ do
@@ -123,31 +124,73 @@
 
 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]
+  describe "[]" $ do
+    it "[]" $ do
+      let test :: forall r. (r ~ '[]) => [()]
+          test = fromType (Proxy @r)
+      test `shouldBe` []
+    it "[(Bool,Int)]" $ do
+      let test :: forall r. (r ~ '[ '( 'True,5), '( 'False,6)]) => [(Bool,Int)]
+          test = fromType (Proxy @r)
+      test `shouldBe` [(True,5),(False,6)]
+  describe "IntMap" $ do
+#if __GLASGOW_HASKELL__ >= 920
+    it "IntMap char, from '[ '(Nat,Char) ]" $ do
+      let test :: forall r. (r ~ '[ '(1,'H'), '(2,'e'), '(5,'o'), '(3,'b'), '(4,'l'), '(3,'l')]) => IM.IntMap Char
+          test = fromType (Proxy @r)
+      test `shouldBe` IM.fromList [(1,'H'),(2,'e'),(5,'o'),(4,'l'),(3,'l')]
+#endif
+    it "IntMap String, from NatMap" $ do
+      let test :: forall r. (r ~ Eval (FNM.FromList '[ '(1,"H"), '(4,"b"), '(2,"e"), '(5,"o"), '(4,"l"), '(3,"l")])) => IM.IntMap String
+          test = fromType (Proxy @r)
+      test `shouldBe` IM.fromList [(2,"e"),(1,"H"),(4,"l"),(3,"l"),(5,"o")]
+    it "IntMap String, with insert" $ 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")]
+  describe "Map" $ do
+#if __GLASGOW_HASKELL__ >= 920
+    it "Map Int char, from '[ '(Nat,Char) ]" $ do
+      let test :: forall r. (r ~ '[ '(1,'H'), '(2,'e'), '(5,'o'), '(4,'l'), '(3,'b'), '(3,'l')]) => DM.Map Int Char
+          test = fromType (Proxy @r)
+      test `shouldBe` DM.fromList [(1,'H'),(2,'e'),(5,'o'),(4,'l'),(3,'l')]
+#endif
+    it "Map Int String, from MapC" $ do
+      let test :: forall r. (r ~ Eval (FNMC.FromList '[ '(1,"H"), '(2,"e"), '(3,"c"), '(5,"o"), '(4,"l"), '(3,"l")])) => DM.Map Int String
+          test = fromType (Proxy @r)
+      test `shouldBe` DM.fromList [(2,"e"),(1,"H"),(4,"l"),(3,"l"),(5,"o")]
+    it "Map Int String, with insert" $ 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")]
+  describe "Set" $ do
+#if __GLASGOW_HASKELL__ >= 920
+    it "Set char, from '[Char]" $ do
+      let test :: forall r. (r ~ '[ 'H','e','o','l','l' ]) => DS.Set Char
+          test = fromType (Proxy @r)
+      test `shouldBe` DS.fromList ['H','e','o','l','l']
+#endif
+    it "Set String, from Set" $ do
+      let test :: forall r. (r ~ Eval (FS.FromList '["H","e","o","l","l"])) => DS.Set String
+          test = fromType (Proxy @r)
+      test `shouldBe` DS.fromList ["e","H","l","l","o"]
+    it "Set Int" $ 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
@@ -254,3 +297,32 @@
           [DT.Node (Right "six") []
           ]
         ]
+
+specShowTypeable :: Spec
+specShowTypeable = describe "Show Type represented at the Kind level" $ do
+  it "Show Int" $ do
+    fromType @String (Proxy @Int)
+      `shouldBe`
+      "Int"
+  it "Show Set of Types" $ do
+    let test :: forall r. (r ~ Eval (FS.FromList '[Int, Maybe String, (), [Integer], IO ()])) 
+             => DS.Set String
+        test = fromType (Proxy @r)
+    test 
+      `shouldBe` 
+      DS.fromList ["Int", "Maybe [Char]", "()", "[Integer]", "IO ()"]
+
+specErrorMessage :: Spec
+specErrorMessage = describe "show GHC.TypeLits.ErrorMessage" $ do
+  it "text error" $ do
+    (fromType @DTxt.Text $ Proxy @('TL.Text "I am error"))
+      `shouldBe`
+      DTxt.pack "I am error"
+  it "ShowType 'True" $ do
+    (fromType @DTxt.Text $ Proxy @('TL.ShowType '()))
+      `shouldBe`
+      DTxt.pack "'()"
+  it "with Kinds" $ do
+    (fromType @DTxt.Text $ Proxy @('TL.Text "Kind: " 'TL.:<>: 'TL.ShowType 'True 'TL.:$$: 'TL.Text "Type: " 'TL.:<>: 'TL.ShowType Bool))
+      `shouldBe`
+      DTxt.pack "Kind: 'True\nType: Bool"