diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,12 @@
 # Changelog for [`clash-prelude` package](http://hackage.haskell.org/package/clash-prelude)
 
+## 0.5 *April 3rd 2014*
+ * Add explicitly clocked synchronous signals for multi-clock circuits
+
+## 0.4.1 *March 27th 2014*
+  * Add saturation to fixed-point operators
+  * Finalize most documentation
+
 ## 0.4 *March 20th 2014*
   * Add fixed-point integers
   * Extend documentation
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,2 +1,2 @@
 = WARNING =
-Only works with latest version of GHC-HEAD (https://github.com/ghc/ghc)!
+Only works with GHC-7.8 (http://www.haskell.org/ghc/dist/7.8.1-rc2/)!
diff --git a/clash-prelude.cabal b/clash-prelude.cabal
--- a/clash-prelude.cabal
+++ b/clash-prelude.cabal
@@ -1,5 +1,5 @@
 Name:                 clash-prelude
-Version:              0.4
+Version:              0.5
 Synopsis:             CAES Language for Synchronous Hardware - Prelude library
 Description:
   CλaSH (pronounced ‘clash’) is a functional hardware description language that
@@ -12,6 +12,15 @@
   This package provides:
   .
   * Prelude library containing datatypes and functions for circuit design
+  .
+  To use the library:
+  .
+  * Import "CLaSH.Prelude"
+  * Additionally import "CLaSH.Prelude.Explicit" if you want to design
+    explicitly clocked circuits in a multi-clock setting
+  .
+  A preliminary version of a tutorial can be found in "CLaSH.Tutorial", for a
+  general overview of the library you should however check out "CLaSH.Prelude".
 Homepage:             http://christiaanb.github.io/clash2/
 bug-reports:          http://github.com/christiaanb/clash-prelude/issues
 License:              BSD3
@@ -41,16 +50,20 @@
                       CLaSH.Class.BitVector
                       CLaSH.Class.Num
                       CLaSH.Prelude
-                      CLaSH.Promoted.Bool
+                      CLaSH.Prelude.Explicit
                       CLaSH.Promoted.Nat
                       CLaSH.Promoted.Nat.TH
                       CLaSH.Promoted.Nat.Literals
                       CLaSH.Promoted.Ord
-                      CLaSH.Signal
+                      CLaSH.Signal.Explicit
+                      CLaSH.Signal.Implicit
                       CLaSH.Sized.Fixed
                       CLaSH.Sized.Signed
                       CLaSH.Sized.Unsigned
                       CLaSH.Sized.Vector
+                      CLaSH.Tutorial
+
+  Other-modules:      CLaSH.Signal.Types
 
   Build-depends:      base                 >= 4.7.0.0 && < 5,
                       data-default         >= 0.5.3,
diff --git a/src/CLaSH/Class/BitVector.hs b/src/CLaSH/Class/BitVector.hs
--- a/src/CLaSH/Class/BitVector.hs
+++ b/src/CLaSH/Class/BitVector.hs
@@ -9,7 +9,7 @@
 import CLaSH.Sized.Vector
 import GHC.TypeLits
 
--- | Convert types from and to a vector of @Bit@s
+-- | Convert types from and to a 'Vec'tor of 'Bit's
 class BitVector a where
   -- | Number of 'Bit's needed to represents elements of type @a@
   type BitSize a :: Nat
diff --git a/src/CLaSH/Class/Num.hs b/src/CLaSH/Class/Num.hs
--- a/src/CLaSH/Class/Num.hs
+++ b/src/CLaSH/Class/Num.hs
@@ -1,14 +1,22 @@
+{-# LANGUAGE DataKinds              #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE MultiParamTypeClasses  #-}
-{-# LANGUAGE NoImplicitPrelude      #-}
 {-# LANGUAGE TypeFamilies           #-}
 module CLaSH.Class.Num where
 
+import GHC.TypeLits
+
+-- | Implicitly adding or subtracting values of two different (sub-)types.
 class Add a b where
   type AResult a b
   plus  :: a -> b -> AResult a b
   minus :: a -> b -> AResult a b
 
+-- | Implicitly multiplying values of two different (sub-)types.
 class Mult a b where
   type MResult a b
   mult :: a -> b -> MResult a b
+
+-- | Coerce a value to be represented by a different number of bits
+class Resize f where
+  resize :: (KnownNat a, KnownNat b) => f a -> f b
diff --git a/src/CLaSH/Prelude.hs b/src/CLaSH/Prelude.hs
--- a/src/CLaSH/Prelude.hs
+++ b/src/CLaSH/Prelude.hs
@@ -1,11 +1,32 @@
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE ImplicitParams      #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE KindSignatures      #-}
 {-# LANGUAGE TypeOperators       #-}
 
 {-# OPTIONS_GHC -O0 -fno-omit-interface-pragmas #-}
 
+{- |
+  CλaSH (pronounced ‘clash’) is a functional hardware description language that
+  borrows both its syntax and semantics from the functional programming language
+  Haskell. The merits of using a functional language to describe hardware comes
+  from the fact that combinational circuits can be directly modeled as
+  mathematical functions and that functional languages lend themselves very well
+  at describing and (de-)composing mathematical functions.
+
+  This package provides:
+
+  * Prelude library containing datatypes and functions for circuit design
+
+  To use the library:
+
+  * Import "CLaSH.Prelude"
+  * Additionally import "CLaSH.Prelude.Explicit" if you want to design
+    explicitly clocked circuits in a multi-clock setting
+
+  For now, "CLaSH.Prelude" is also the best starting point for exploring the
+  library. A tutorial module will be added within due time.
+-}
 module CLaSH.Prelude
   ( -- * Creating synchronous sequential circuits
     (<^>)
@@ -23,40 +44,75 @@
     -- * Utility functions
   , window
   , windowD
-  , module Exported
+    -- * Testbench functions
+  , sassert
+  , stimuliGenerator
+  , outputVerifier
+    -- * Exported modules
+    -- ** Implicitly clocked synchronous signals
+  , module CLaSH.Signal.Implicit
+    -- ** Datatypes
+  , module CLaSH.Bit
+    -- *** Arbitrary-width numbers
+  , module CLaSH.Sized.Signed
+  , module CLaSH.Sized.Unsigned
+    -- *** Fixed point numbers
+  , module CLaSH.Sized.Fixed
+    -- *** Fixed size vectors
+  , module CLaSH.Sized.Vector
+    -- ** Type-level natural numbers
+  , module GHC.TypeLits
+  , module CLaSH.Promoted.Nat
+  , module CLaSH.Promoted.Nat.Literals
+  , module CLaSH.Promoted.Nat.TH
+    -- ** Type-level functions
+  , module CLaSH.Promoted.Ord
+    -- ** Template Haskell
+  , Lift (..), deriveLift
+    -- ** Type classes
+    -- *** CLaSH
+  , module CLaSH.Class.BitVector
+  , module CLaSH.Class.Num
+    -- *** Other
+  , module Control.Arrow
+  , module Control.Applicative
+  , module Data.Bits
+  , module Data.Default
   )
 where
 
-import Control.Arrow               as Exported
-import Control.Applicative         as Exported
+import Control.Arrow
+import Control.Applicative
 import Control.Category            as Category
-import Data.Bits                   as Exported
-import Data.Default                as Exported
-import CLaSH.Class.BitVector       as Exported
-import CLaSH.Class.Num             as Exported
-import CLaSH.Promoted.Bool         as Exported
-import CLaSH.Promoted.Nat          as Exported
-import CLaSH.Promoted.Nat.TH       as Exported
-import CLaSH.Promoted.Nat.Literals as Exported
-import CLaSH.Promoted.Ord          as Exported
-import CLaSH.Sized.Fixed           as Exported
-import CLaSH.Sized.Signed          as Exported
-import CLaSH.Sized.Unsigned        as Exported
-import CLaSH.Sized.Vector          as Exported
-import CLaSH.Bit                   as Exported
-import CLaSH.Signal                as Exported
-import GHC.TypeLits                as Exported
+import Data.Bits
+import Data.Default
+import Debug.Trace                 (trace)
+import CLaSH.Class.BitVector
+import CLaSH.Class.Num
+import CLaSH.Promoted.Nat
+import CLaSH.Promoted.Nat.TH
+import CLaSH.Promoted.Nat.Literals
+import CLaSH.Promoted.Ord
+import CLaSH.Sized.Fixed
+import CLaSH.Sized.Signed
+import CLaSH.Sized.Unsigned
+import CLaSH.Sized.Vector
+import CLaSH.Bit
+import CLaSH.Signal.Implicit
+import GHC.TypeLits
+import Language.Haskell.TH.Lift     (Lift(..),deriveLift)
 
 {-# INLINABLE window #-}
 -- | Give a window over a 'Signal'
 --
 -- > window4 :: Signal Int -> Vec 4 (Signal Int)
 -- > window4 = window
--- >
--- > simulateP window4 [1,2,3,4,5,... == [1:>0:>0:>0:>Nil, 2:>1:>0:>0:>Nil, 3:>2:>1:>0:>Nil, 4:>3:>2:>1:>Nil, 5:>4:>3:>2:>Nil,...
+--
+-- >>> simulateP window4 [1,2,3,4,5,...
+-- [<1,0,0,0>, <2,1,0,0>, <3,2,1,0>, <4,3,2,1>, <5,4,3,2>,...
 window :: (KnownNat (n + 1), Default a)
-       => Signal a
-       -> Vec ((n + 1) + 1) (Signal a)
+       => Signal a                     -- ^ Signal to create a window over
+       -> Vec ((n + 1) + 1) (Signal a) -- ^ Window of at least size 2
 window x = x :> prev
   where
     prev = registerP (vcopyI def) next
@@ -67,11 +123,12 @@
 --
 -- > windowD3 :: Signal Int -> Vec 3 (Signal Int)
 -- > windowD3 = windowD
--- >
--- > simulateP windowD3 [1,2,3,4,... == [0:>0:>0:>Nil, 1:>0:>0:>Nil, 2:>1:>0:>Nil, 3:>2:>1:>Nil, 4:>3:>2:>Nil,...
+--
+-- >>> simulateP windowD3 [1,2,3,4,...
+-- [<0,0,0>, <1,0,0>, <2,1,0>, <3,2,1>, <4,3,2>,...
 windowD :: (KnownNat (n + 1), Default a)
-        => Signal a
-        -> Vec (n + 1) (Signal a)
+        => Signal a               -- ^ Signal to create a window over
+        -> Vec (n + 1) (Signal a) -- ^ Window of at least size 1
 windowD x = prev
   where
     prev = registerP (vcopyI def) next
@@ -90,9 +147,10 @@
 -- >
 -- > topEntity :: (Signal Int, Signal Int) -> Signal Int
 -- > topEntity = mac <^> 0
--- >
--- > simulateP topEntity [(1,1),(2,2),(3,3),(4,4),... == [0,1,5,14,30,...
 --
+-- >>> simulateP topEntity [(1,1),(2,2),(3,3),(4,4),...
+-- [0,1,5,14,30,...
+--
 -- Synchronous sequential functions can be composed just like their combinational counterpart:
 --
 -- > dualMac :: (Signal Int, Signal Int)
@@ -106,7 +164,7 @@
       => (s -> i -> (s,o))        -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@
       -> s                        -- ^ Initial state
       -> (SignalP i -> SignalP o) -- ^ Synchronous sequential function with input and output matching that of the mealy machine
-f <^> iS = \i -> let (s',o) = unpack $ f <$> s <*> (pack i)
+f <^> iS = \i -> let (s',o) = unpack $ f <$> s <*> pack i
                      s      = register iS s'
                  in unpack o
 
@@ -115,8 +173,9 @@
 --
 -- > rP :: (Signal Int,Signal Int) -> (Signal Int, Signal Int)
 -- > rP = registerP (8,8)
--- >
--- > simulateP rP [(1,1),(2,2),(3,3),... == [(8,8),(1,1),(2,2),(3,3),...
+--
+-- >>> simulateP rP [(1,1),(2,2),(3,3),...
+-- [(8,8),(1,1),(2,2),(3,3),...
 registerP :: Pack a => a -> SignalP a -> SignalP a
 registerP i = unpack Prelude.. register i Prelude.. pack
 
@@ -125,7 +184,7 @@
 --
 -- > bram40 :: Signal (Unsigned 6) -> Signal (Unsigned 6) -> Signal Bool -> Signal a -> Signal a
 -- > bram40 = blockRam d50
-blockRam :: forall n m a . (KnownNat n, KnownNat m, Pack a)
+blockRam :: forall n m a . (KnownNat n, KnownNat m, Pack a, Default a)
          => SNat n              -- ^ Size @n@ of the blockram
          -> Signal (Unsigned m) -- ^ Write address @w@
          -> Signal (Unsigned m) -- ^ Read address @r@
@@ -135,7 +194,7 @@
 blockRam n wr rd en din = pack $ (bram' <^> binit) (wr,rd,en,din)
   where
     binit :: (Vec n a,a)
-    binit = (vcopy n (error "uninitialized ram"),error "uninitialized ram")
+    binit = (vcopy n def,def)
 
     bram' :: (Vec n a,a) -> (Unsigned m, Unsigned m, Bool, a)
           -> (((Vec n a),a),a)
@@ -145,11 +204,12 @@
              | otherwise = ram
         o'               = ram ! r
 
+{-# DEPRECATED blockRamC "'Comp' is deprecated, use 'blockRam' instead" #-}
 -- | Create a blockRAM with space for @n@ elements
 --
 -- > bramC40 :: Comp (Unsigned 6, Unsigned 6, Bool, a) a
 -- > bramC40 = blockRamC d50
-blockRamC :: (KnownNat n, KnownNat m, Pack a)
+blockRamC :: (KnownNat n, KnownNat m, Pack a, Default a)
           => SNat n -- ^ Size @n@ of the blockram
           -> Comp (Unsigned m, Unsigned m, Bool, a) a
 blockRamC n = C ((\(wr,rd,en,din) -> blockRam n wr rd en din) Prelude.. unpack)
@@ -159,8 +219,8 @@
 --
 -- > bram32 :: Signal (Unsigned 5) -> Signal (Unsigned 5) -> Signal Bool -> Signal a -> Signal a
 -- > bram32 = blockRamPow2 d32
-blockRamPow2 :: (KnownNat n, KnownNat (2^n), Pack a)
-             => SNat ((2^n) :: Nat) -- ^ Size @2^n@ of the blockram
+blockRamPow2 :: (KnownNat n, KnownNat (2^n), Pack a, Default a)
+             => SNat (2^n)          -- ^ Size @2^n@ of the blockram
              -> Signal (Unsigned n) -- ^ Write address @w@
              -> Signal (Unsigned n) -- ^ Read address @r@
              -> Signal Bool         -- ^ Write enable
@@ -168,29 +228,29 @@
              -> Signal a            -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle
 blockRamPow2 = blockRam
 
+{-# DEPRECATED blockRamPow2C "'Comp' is deprecated, use 'blockRamPow2' instead" #-}
 -- | Create a blockRAM with space for 2^@n@ elements
 --
 -- > bramC32 :: Comp (Unsigned 5, Unsigned 5, Bool, a) a
 -- > bramC32 = blockRamPow2C d32
-blockRamPow2C :: (KnownNat n, KnownNat (2^n), Pack a)
-              => SNat ((2^n) :: Nat) -- ^ Size @2^n@ of the blockram
+blockRamPow2C :: (KnownNat n, KnownNat (2^n), Pack a, Default a)
+              => SNat (2^n) -- ^ Size @2^n@ of the blockram
               -> Comp (Unsigned n, Unsigned n, Bool, a) a
 blockRamPow2C n = C ((\(wr,rd,en,din) -> blockRamPow2 n wr rd en din) Prelude.. unpack)
 
+{-# DEPRECATED Comp "Use 'Applicative' interface and ('<^>') instead" #-}
 -- | 'Comp'onent: an 'Arrow' interface to synchronous sequential functions
-newtype Comp a b = C { asFunction :: Signal a -> Signal b }
+newtype Comp  a b = C { asFunction :: Signal a -> Signal b }
 
 instance Category Comp where
   id            = C Prelude.id
   (C f) . (C g) = C (f Prelude.. g)
 
-infixr 8 ><
-(><) :: (a -> b) -> (c -> d) -> (a, c) -> (b, d)
-(f >< g) (x,y) = (f x,g y)
-
 instance Arrow Comp where
   arr         = C Prelude.. fmap
   first (C f) = C $ pack Prelude.. (f >< Prelude.id) Prelude.. unpack
+    where
+      (g >< h) (x,y) = (g x,h y)
 
 instance ArrowLoop Comp where
   loop (C f) = C $ simpleLoop (unpack Prelude.. f Prelude.. pack)
@@ -198,21 +258,26 @@
       simpleLoop g b = let ~(c,d) = g (b,d)
                        in c
 
+{-# DEPRECATED registerC "'Comp' is deprecated, use 'register' instead" #-}
 -- | Create a 'register' 'Comp'onent
 --
 -- > rC :: Comp (Int,Int) (Int,Int)
 -- > rC = registerC (8,8)
--- >
--- > simulateC rP [(1,1),(2,2),(3,3),... == [(8,8),(1,1),(2,2),(3,3),...
+--
+-- >>> simulateC rP [(1,1),(2,2),(3,3),...
+-- [(8,8),(1,1),(2,2),(3,3),...
 registerC :: a -> Comp a a
 registerC = C Prelude.. register
 
+{-# DEPRECATED simulateC "'Comp' is deprecated, use 'simulate' instead" #-}
 -- | Simulate a 'Comp'onent given a list of samples
 --
--- > simulateC (registerC 8) [1, 2, 3, ... == [8, 1, 2, 3, ...
+-- >>> simulateC (registerC 8) [1, 2, 3, ...
+-- [8, 1, 2, 3, ...
 simulateC :: Comp a b -> [a] -> [b]
 simulateC f = simulate (asFunction f)
 
+{-# DEPRECATED (^^^) "Use 'Applicative' interface and ('<^>') instead" #-}
 {-# INLINABLE (^^^) #-}
 -- | Create a synchronous 'Comp'onent from a combinational function describing
 -- a mealy machine
@@ -226,9 +291,10 @@
 -- >
 -- > topEntity :: Comp (Int,Int) Int
 -- > topEntity = mac ^^^ 0
--- >
--- > simulateC topEntity [(1,1),(2,2),(3,3),(4,4),... == [0,1,5,14,30,...
 --
+-- >>> simulateC topEntity [(1,1),(2,2),(3,3),(4,4),...
+-- [0,1,5,14,30,...
+--
 -- Synchronous sequential must be composed using the 'Arrow' syntax
 --
 -- > dualMac :: Comp (Int,Int,Int,Int) Int
@@ -242,3 +308,100 @@
 f ^^^ sI = C $ \i -> let (s',o) = unpack $ f <$> s <*> i
                          s      = register sI s'
                      in  o
+
+{-# NOINLINE sassert #-}
+-- | Compares the first two arguments for equality and logs a warning when they
+-- are not equal. The second argument is considered the expected value. This
+-- function simply returns the third argument unaltered as its result. This
+-- function is used by 'outputVerifier'.
+--
+-- This function is translated to the following VHDL:
+--
+-- > sassert_block : block
+-- > begin
+-- >   -- pragma translate_off
+-- >   process(clk_1000,reset_1000,arg0,arg1) is
+-- >   begin
+-- >     if (rising_edge(clk_1000) or rising_edge(reset_1000)) then
+-- >       assert (arg0 = arg1) report ("expected: " & to_string (arg1) & \", actual: \" & to_string (arg0)) severity error;
+-- >     end if;
+-- >   end process;
+-- >   -- pragma translate_on
+-- >   result <= arg2;
+-- > end block;
+--
+-- And can, due to the pragmas, be used in synthesizable designs
+sassert :: (Eq a, Show a)
+        => Signal a -- ^ Checked value
+        -> Signal a -- ^ Expected value
+        -> Signal b -- ^ Returned value
+        -> Signal b
+sassert = liftA3
+  (\a' b' c' -> if a' == b' then c'
+                            else trace ("\nexpected value: " ++ show b' ++ ", not equal to actual value: " ++ show a') c')
+
+{-# INLINABLE stimuliGenerator #-}
+-- | To be used as a one of the functions to create the \"magical\" 'testInput'
+-- value, which the CλaSH compilers looks for to create the stimulus generator
+-- for the generated VHDL testbench.
+--
+-- Example:
+--
+-- > testInput :: Signal Int
+-- > testInput = stimuliGenerator $(v [(1::Int),3..21])
+--
+-- >>> sample testInput
+-- [1,3,5,7,9,11,13,15,17,19,21,21,21,...
+stimuliGenerator :: forall l a . KnownNat l
+                 => Vec l a  -- ^ Samples to generate
+                 -> Signal a -- ^ Signal of given samples
+stimuliGenerator samples  =
+    let (r,o) = unpack (genT <$> register (fromInteger (maxIndex samples)) r)
+    in  o
+  where
+    genT :: Unsigned l -> (Unsigned l, a)
+    genT s = (s',samples ! s)
+      where
+        s' = if s > 0 then s - 1
+                      else s
+
+{-# INLINABLE outputVerifier #-}
+-- | To be used as a functions to generate the \"magical\" 'expectedOutput'
+-- function, which the CλaSH compilers looks for to create the signal verifier
+-- for the generated VHDL testbench.
+--
+-- Example:
+--
+-- > expectedOutput :: Signal Int -> Signal Bool
+-- > expectedOutput = outputVerifier $(v ([70,99,2,3,4,5,7,8,9,10]::[Int]))
+--
+-- >>> sample (expectedOutput (fromList ([0..10] ++ [10,10,10])))
+-- [
+-- expected value: 70, not equal to actual value: 0
+-- False,
+-- expected value: 99, not equal to actual value: 1
+-- False,False,False,False,False,
+-- expected value: 7, not equal to actual value: 6
+-- False,
+-- expected value: 8, not equal to actual value: 7
+-- False,
+-- expected value: 9, not equal to actual value: 8
+-- False,
+-- expected value: 10, not equal to actual value: 9
+-- False,True,True,...
+outputVerifier :: forall l a . (KnownNat l, Eq a, Show a)
+               => Vec l a     -- ^ Samples to compare with
+               -> Signal a    -- ^ Signal to verify
+               -> Signal Bool -- ^ Indicator that all samples are verified
+outputVerifier samples i =
+    let (s,o) = unpack (genT <$> register (fromInteger (maxIndex samples)) s)
+        (e,f) = unpack o
+    in  sassert i e (register False f)
+  where
+    genT :: Unsigned l -> (Unsigned l, (a,Bool))
+    genT s = (s',(samples ! s,finished))
+      where
+        s' = if s >= 1 then s - 1
+                       else s
+
+        finished = s == 0
diff --git a/src/CLaSH/Prelude/Explicit.hs b/src/CLaSH/Prelude/Explicit.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Prelude/Explicit.hs
@@ -0,0 +1,393 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ExplicitNamespaces  #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
+
+{-# OPTIONS_GHC -O0 -fno-omit-interface-pragmas #-}
+
+{- |
+  This module defines the explicitly clocked counterparts of the functions
+  defined in "CLaSH.Prelude".
+
+  This module uses the explicitly clocked 'CSignal's synchronous signals, as
+  opposed to the implicitly clocked 'Signal's used in "CLaSH.Prelude". Take a
+  look at "CLaSH.Signal.Explicit" to see how you can make multi-clock designs
+  using explicitly clocked signals.
+-}
+module CLaSH.Prelude.Explicit
+  ( -- * Creating synchronous sequential circuits
+    sync
+  , cregisterP
+    -- * 'Arrow' interface for synchronous sequential circuits
+  , CComp (..)
+  , syncA
+  , cregisterC
+  , csimulateC
+    -- * BlockRAM primitives
+  , cblockRam
+  , cblockRamPow2
+  , blockRamCC
+  , blockRamPow2CC
+    -- * Utility functions
+  , cwindow
+  , cwindowD
+    -- * Testbench functions
+  , csassert
+  , cstimuliGenerator
+  , coutputVerifier
+    -- * Exported modules
+    -- ** Explicitly clocked synchronous signals
+  , module CLaSH.Signal.Explicit
+  )
+where
+
+import Data.Default          (Default (..))
+import Debug.Trace           (trace)
+import Control.Applicative   (Applicative (..), (<$>),liftA3)
+import Control.Arrow         (Arrow (..), ArrowLoop (..))
+import Control.Category      as Category
+import GHC.TypeLits          (KnownNat,type (^), type (+))
+
+import CLaSH.Promoted.Nat    (SNat, snat)
+import CLaSH.Signal.Explicit
+import CLaSH.Sized.Unsigned  (Unsigned)
+import CLaSH.Sized.Vector    (Vec (..), (!), (+>>), maxIndex, vcopy, vcopyI, vreplace)
+
+{-# INLINABLE sync #-}
+-- | Create a synchronous function from a combinational function describing
+-- a mealy machine
+--
+-- > mac :: Int        -- Current state
+-- >     -> (Int,Int)  -- Input
+-- >     -> (Int,Int)  -- (Updated state, output)
+-- > mac s (x,y) = (s',s)
+-- >   where
+-- >     s' = x * y + s
+-- >
+-- > clk100 = Clock d100
+-- >
+-- > topEntity :: (CSignal 100 Int, CSignal 100 Int) -> CSignal 100 Int
+-- > topEntity = sync clk100 mac 0
+--
+-- >>> csimulateP clk100 clk100 topEntity [(1,1),(2,2),(3,3),(4,4),...
+-- [0,1,5,14,30,...
+--
+-- Synchronous sequential functions can be composed just like their combinational counterpart:
+--
+-- > dualMac :: (CSignal 100 Int, CSignal 100 Int)
+-- >         -> (CSignal 100 Int, CSignal 100 Int)
+-- >         -> CSignal 100 Int
+-- > dualMac (a,b) (x,y) = s1 + s2
+-- >   where
+-- >     s1 = sync clk100 mac 0 (a,b)
+-- >     s2 = sync clk100 mac 0 (x,y)
+sync :: (CPack i, CPack o)
+     => Clock clk                          -- ^ 'Clock' to synchronize to
+     -> (s -> i -> (s,o))                  -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@
+     -> s                                  -- ^ Initial state
+     -> (CSignalP clk i -> CSignalP clk o) -- ^ Synchronous sequential function with input and output matching that of the mealy machine
+sync clk f iS = \i -> let (s',o) = cunpack clk $ f <$> s <*> cpack clk i
+                          s      = cregister clk iS s'
+                      in cunpack clk o
+
+{-# INLINABLE cregisterP #-}
+-- | Create a 'register' function for product-type like signals (e.g. '(Signal a, Signal b)')
+--
+-- > clk100 = Clock d100
+-- >
+-- > rP :: (CSignal 100 Int, CSignal 100 Int) -> (CSignal 100 Int, CSignal 100 Int)
+-- > rP = cregisterP d100 (8,8)
+--
+-- >>> csimulateP clk100 clk100 rP [(1,1),(2,2),(3,3),...
+-- [(8,8),(1,1),(2,2),(3,3),...
+cregisterP :: CPack a => Clock clk -> a -> CSignalP clk a -> CSignalP clk a
+cregisterP clk i = cunpack clk Prelude.. cregister clk i Prelude.. cpack clk
+
+{-# DEPRECATED CComp "Use 'Applicative' interface and 'sync' instead" #-}
+-- | 'CComp'onent: an 'Arrow' interface to explicitly clocked synchronous
+-- sequential functions
+newtype CComp t a b = CC { asCFunction :: CSignal t a -> CSignal t b }
+
+instance Category (CComp t) where
+  id              = CC Prelude.id
+  (CC f) . (CC g) = CC (f Prelude.. g)
+
+instance KnownNat t => Arrow (CComp t) where
+  arr          = CC Prelude.. fmap
+  first (CC f) = let clk = Clock snat
+                 in  CC $ cpack clk Prelude.. (f >< Prelude.id) Prelude.. cunpack clk
+    where
+      (g >< h) (x,y) = (g x,h y)
+
+instance KnownNat t => ArrowLoop (CComp t) where
+  loop (CC f) = let clk = Clock snat
+                in  CC $ simpleLoop (cunpack clk Prelude.. f Prelude.. cpack clk)
+    where
+      simpleLoop g b = let ~(c,d) = g (b,d)
+                       in c
+
+{-# DEPRECATED syncA "Use 'Applicative' interface and 'sync' instead" #-}
+{-# INLINABLE syncA #-}
+-- | Create a synchronous 'CComp'onent from a combinational function describing
+-- a mealy machine
+--
+-- > mac :: Int        -- Current state
+-- >     -> (Int,Int)  -- Input
+-- >     -> (Int,Int)  -- (Updated state, output)
+-- > mac s (x,y) = (s',s)
+-- >   where
+-- >     s' = x * y + s
+-- >
+-- > clk100 = Clock d100
+-- >
+-- > topEntity :: CComp 100 (Int,Int) Int
+-- > topEntity = syncA clk100 mac 0
+--
+-- >>> simulateC topEntity [(1,1),(2,2),(3,3),(4,4),...
+-- [0,1,5,14,30,...
+--
+-- Synchronous sequential must be composed using the 'Arrow' syntax
+--
+-- > dualMac :: CComp 100 (Int,Int,Int,Int) Int
+-- > dualMac = proc (a,b,x,y) -> do
+-- >   rec s1 <- syncA clk100 mac 0 -< (a,b)
+-- >       s2 <- syncA clk100 mac 0 -< (x,y)
+-- >   returnA -< (s1 + s2)
+syncA :: Clock clk         -- ^ 'Clock' to synchronize to
+      -> (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@
+      -> s                 -- ^ Initial state
+      -> CComp clk i o     -- ^ Synchronous sequential 'Comp'onent with input and output matching that of the mealy machine
+syncA clk f sI = CC $ \i -> let (s',o) = cunpack clk $ f <$> s <*> i
+                                s      = cregister clk sI s'
+                            in  o
+
+{-# DEPRECATED cregisterC "'CComp' is deprecated, use 'cregister' instead" #-}
+-- | Create a 'cregister' 'CComp'onent
+--
+-- > clk100 = Clock d100
+-- >
+-- > rC :: CComp 100 (Int,Int) (Int,Int)
+-- > rC = cregisterC clk100 (8,8)
+--
+-- >>> simulateC rP [(1,1),(2,2),(3,3),...
+-- [(8,8),(1,1),(2,2),(3,3),...
+cregisterC :: Clock clk -> a -> CComp clk a a
+cregisterC clk = CC Prelude.. cregister clk
+
+{-# DEPRECATED csimulateC "'CComp' is deprecated, use 'csimulate' instead" #-}
+-- | Simulate a 'Comp'onent given a list of samples
+--
+-- > clk100 = Clock d100
+-- >>> csimulateC (cregisterC clk100 8) [1, 2, 3, ...
+-- [8, 1, 2, 3, ...
+csimulateC :: CComp clk a b -> [a] -> [b]
+csimulateC f = csimulate (asCFunction f)
+
+{-# NOINLINE cblockRam #-}
+-- | Create a blockRAM with space for @n@ elements
+--
+-- > clk100 = Clock d100
+-- >
+-- > bram40 :: CSignal 100 (Unsigned 6) -> CSignal 100 (Unsigned 6)
+-- >        -> CSignal 100 Bool -> CSignal 100 a -> 100 CSignal a
+-- > bram40 = cblockRam clk100 d50
+cblockRam :: forall n m a clk . (KnownNat n, KnownNat m, CPack a, Default a)
+          => Clock clk                -- ^ 'Clock' to synchronize to
+          -> SNat n                   -- ^ Size @n@ of the blockram
+          -> CSignal clk (Unsigned m) -- ^ Write address @w@
+          -> CSignal clk (Unsigned m) -- ^ Read address @r@
+          -> CSignal clk Bool         -- ^ Write enable
+          -> CSignal clk a            -- ^ Value to write (at address @w@)
+          -> CSignal clk a            -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle
+cblockRam clk n wr rd en din = cpack clk $ (sync clk bram' binit) (wr,rd,en,din)
+  where
+    binit :: (Vec n a,a)
+    binit = (vcopy n def,def)
+
+    bram' :: (Vec n a,a) -> (Unsigned m, Unsigned m, Bool, a)
+          -> (((Vec n a),a),a)
+    bram' (ram,o) (w,r,e,d) = ((ram',o'),o)
+      where
+        ram' | e         = vreplace ram w d
+             | otherwise = ram
+        o'               = ram ! r
+
+{-# DEPRECATED blockRamCC "'CComp' is deprecated, use 'cblockRam' instead" #-}
+-- | Create a blockRAM with space for @n@ elements
+--
+-- > clk100 = Clock 100
+-- >
+-- > bramC40 :: CComp 100 (Unsigned 6, Unsigned 6, Bool, a) a
+-- > bramC40 = blockRamCC clk100 d50
+blockRamCC :: (KnownNat n, KnownNat m, CPack a, Default a)
+           => Clock clk -- ^ 'Clock' to synchronize to
+           -> SNat n    -- ^ Size @n@ of the blockram
+           -> CComp clk (Unsigned m, Unsigned m, Bool, a) a
+blockRamCC clk n = CC ((\(wr,rd,en,din) -> cblockRam clk n wr rd en din) Prelude.. cunpack clk)
+
+{-# INLINABLE cblockRamPow2 #-}
+-- | Create a blockRAM with space for 2^@n@ elements
+--
+-- > bram32 :: Signal (Unsigned 5) -> Signal (Unsigned 5) -> Signal Bool -> Signal a -> Signal a
+-- > bram32 = cblockRamPow2 d32
+cblockRamPow2 :: (KnownNat n, KnownNat (2^n), CPack a, Default a)
+              => Clock clk                -- ^ 'Clock' to synchronize to
+              -> SNat (2^n)               -- ^ Size @2^n@ of the blockram
+              -> CSignal clk (Unsigned n) -- ^ Write address @w@
+              -> CSignal clk (Unsigned n) -- ^ Read address @r@
+              -> CSignal clk Bool         -- ^ Write enable
+              -> CSignal clk a            -- ^ Value to write (at address @w@)
+              -> CSignal clk a            -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle
+cblockRamPow2 = cblockRam
+
+{-# DEPRECATED blockRamPow2CC "'CComp' is deprecated, use 'cblockRamPow2' instead" #-}
+-- | Create a blockRAM with space for 2^@n@ elements
+--
+-- > clk100 = Clock d100
+-- >
+-- > bramC32 :: CComp 100 (Unsigned 5, Unsigned 5, Bool, a) a
+-- > bramC32 = blockRamPow2CC clk100 d32
+blockRamPow2CC :: (KnownNat n, KnownNat (2^n), CPack a, Default a)
+               => Clock clk  -- ^ 'Clock' to synchronize to
+               -> SNat (2^n) -- ^ Size @2^n@ of the blockram
+               -> CComp clk (Unsigned n, Unsigned n, Bool, a) a
+blockRamPow2CC clk n = CC ((\(wr,rd,en,din) -> cblockRamPow2 clk n wr rd en din) Prelude.. cunpack clk)
+
+{-# INLINABLE cwindow #-}
+-- | Give a window over a 'CSignal'
+--
+-- > window4 :: Signal Int -> Vec 4 (Signal Int)
+-- > window4 = window
+--
+-- >>> csimulateP window4 [1,2,3,4,5,...
+-- [<1,0,0,0>, <2,1,0,0>, <3,2,1,0>, <4,3,2,1>, <5,4,3,2>,...
+cwindow :: (KnownNat (n + 1), Default a)
+        => Clock clk                         -- ^ Clock to which the incoming signal is synchronized
+        -> CSignal clk a                     -- ^ Signal to create a window over
+        -> Vec ((n + 1) + 1) (CSignal clk a) -- ^ Window of at least size 2
+cwindow clk x = x :> prev
+  where
+    prev = cregisterP clk (vcopyI def) next
+    next = x +>> prev
+
+{-# INLINABLE cwindowD #-}
+-- | Give a delayed window over a 'CSignal'
+--
+-- > windowD3 :: Signal Int -> Vec 3 (Signal Int)
+-- > windowD3 = windowD
+--
+-- >>> csimulateP windowD3 [1,2,3,4,...
+-- [<0,0,0>, <1,0,0>, <2,1,0>, <3,2,1>, <4,3,2>,...
+cwindowD :: (KnownNat (n + 1), Default a)
+        => Clock clk                    -- ^ Clock to which the incoming signal is synchronized
+        -> CSignal clk a                -- ^ Signal to create a window over
+        -> Vec (n + 1) (CSignal clk a)  -- ^ Window of at least size 1
+cwindowD clk x = prev
+  where
+    prev = cregisterP clk (vcopyI def) next
+    next = x +>> prev
+
+{-# NOINLINE csassert #-}
+-- | Compares the first two arguments for equality and logs a warning when they
+-- are not equal. The second argument is considered the expected value. This
+-- function simply returns the third argument unaltered as its result. This
+-- function is used by 'coutputVerifier'.
+--
+--
+-- This function is translated to the following VHDL:
+--
+-- > csassert_block : block
+-- > begin
+-- >   -- pragma translate_off
+-- >   process(clk_t,reset_t,arg0,arg1) is
+-- >   begin
+-- >     if (rising_edge(clk_t) or rising_edge(reset_t)) then
+-- >       assert (arg0 = arg1) report ("expected: " & to_string (arg1) & \", actual: \" & to_string (arg0)) severity error;
+-- >     end if;
+-- >   end process;
+-- >   -- pragma translate_on
+-- >   result <= arg2;
+-- > end block;
+--
+-- And can, due to the pragmas, be used in synthesizable designs
+csassert :: (Eq a,Show a)
+         => CSignal t a -- ^ Checked value
+         -> CSignal t a -- ^ Expected value
+         -> CSignal t b -- ^ Return valued
+         -> CSignal t b
+csassert = liftA3
+  (\a' b' c' -> if a' == b' then c'
+                            else trace ("\nexpected value: " ++ show b' ++ ", not equal to actual value: " ++ show a') c')
+
+{-# INLINABLE cstimuliGenerator #-}
+-- | To be used as a one of the functions to create the \"magical\" 'testInput'
+-- value, which the CλaSH compilers looks for to create the stimulus generator
+-- for the generated VHDL testbench.
+--
+-- Example:
+--
+-- > clk2 = Clock d2
+-- >
+-- > testInput :: CSignal 2 Int
+-- > testInput = cstimuliGenerator $(v [(1::Int),3..21]) clk2
+--
+-- >>> csample testInput
+-- [1,3,5,7,9,11,13,15,17,19,21,21,21,...
+cstimuliGenerator :: forall l clk a . KnownNat l
+                  => Vec l a        -- ^ Samples to generate
+                  -> Clock clk      -- ^ Clock to synchronize the output signal to
+                  -> CSignal clk a  -- ^ Signal of given samples
+cstimuliGenerator samples clk =
+    let (r,o) = cunpack clk (genT <$> cregister clk (fromInteger (maxIndex samples)) r)
+    in  o
+  where
+    genT :: Unsigned l -> (Unsigned l,a)
+    genT s = (s',samples ! s)
+      where
+        s' = if s > 0 then s - 1
+                      else s
+
+{-# INLINABLE coutputVerifier #-}
+-- | To be used as a functions to generate the \"magical\" 'expectedOutput'
+-- function, which the CλaSH compilers looks for to create the signal verifier
+-- for the generated VHDL testbench.
+--
+-- Example:
+--
+-- > clk7 = Clock d7
+-- >
+-- > expectedOutput :: CSignal 7 Int -> CSignal 7 Bool
+-- > expectedOutput = coutputVerifier $(v ([70,99,2,3,4,5,7,8,9,10]::[Int])) clk7
+--
+-- >>> csample (expectedOutput (cfromList ([0..10] ++ [10,10,10])))
+-- [
+-- expected value: 70, not equal to actual value: 0
+-- False,
+-- expected value: 99, not equal to actual value: 1
+-- False,False,False,False,False,
+-- expected value: 7, not equal to actual value: 6
+-- False,
+-- expected value: 8, not equal to actual value: 7
+-- False,
+-- expected value: 9, not equal to actual value: 8
+-- False,
+-- expected value: 10, not equal to actual value: 9
+-- False,True,True,...
+coutputVerifier :: forall l clk a . (KnownNat l, Eq a, Show a)
+                => Vec l a           -- ^ Samples to compare with
+                -> Clock clk         -- ^ Clock the input signal is synchronized to
+                -> CSignal clk a     -- ^ Signal to verify
+                -> CSignal clk Bool  -- ^ Indicator that all samples are verified
+coutputVerifier samples clk i =
+    let (s,o) = cunpack clk (genT <$> cregister clk (fromInteger (maxIndex samples)) s)
+        (e,f) = cunpack clk o
+    in  csassert i e (cregister clk False f)
+  where
+    genT :: Unsigned l -> (Unsigned l,(a,Bool))
+    genT s = (s',(samples ! s,finished))
+      where
+        s' = if s >= 1 then s - 1
+                       else s
+
+        finished = s == 0
diff --git a/src/CLaSH/Promoted/Bool.hs b/src/CLaSH/Promoted/Bool.hs
deleted file mode 100644
--- a/src/CLaSH/Promoted/Bool.hs
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# LANGUAGE DataKinds      #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TypeFamilies   #-}
-{-# LANGUAGE PolyKinds      #-}
-module CLaSH.Promoted.Bool where
-
--- | Type-level if-then-else
-type family If (x :: Bool) (y :: k) (z :: k) :: k
-  where
-    If True  y z = y
-    If False y z = z
diff --git a/src/CLaSH/Promoted/Nat.hs b/src/CLaSH/Promoted/Nat.hs
--- a/src/CLaSH/Promoted/Nat.hs
+++ b/src/CLaSH/Promoted/Nat.hs
@@ -4,7 +4,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators       #-}
 module CLaSH.Promoted.Nat
-  ( SNat, snat, withSNat
+  ( SNat, snat, withSNat, snatToInteger
   , UNat (..), toUNat, addUNat, multUNat, powUNat
   )
 where
@@ -14,15 +14,24 @@
 import Unsafe.Coerce
 
 -- | Singleton value for a type-level natural number 'n'
+--
+-- * "CLaSH.Promoted.Nat.Literals" contains a list of predefined 'SNat' literals
+-- * "CLaSH.Promoted.Nat.TH" has functions to easily create large ranges of new 'SNat' literals
 data SNat (n :: Nat) = KnownNat n => SNat (Proxy n)
 
--- | Singleton value for a type-level natural number
+instance Show (SNat n) where
+  show (SNat p) = 'd' : show (natVal p)
+
+-- | Create a singleton literal for a type-level natural number
 snat :: KnownNat n => SNat n
 snat = SNat Proxy
 
 -- | Supply a function with a singleton natural 'n' according to the context
 withSNat :: KnownNat n => (SNat n -> a) -> a
 withSNat f = f (SNat Proxy)
+
+snatToInteger :: SNat n -> Integer
+snatToInteger (SNat p) = natVal p
 
 -- | Unary representation of a type-level natural
 data UNat :: Nat -> * where
diff --git a/src/CLaSH/Promoted/Nat/Literals.hs b/src/CLaSH/Promoted/Nat/Literals.hs
--- a/src/CLaSH/Promoted/Nat/Literals.hs
+++ b/src/CLaSH/Promoted/Nat/Literals.hs
@@ -1,7 +1,17 @@
 {-# LANGUAGE TemplateHaskell, DataKinds #-}
--- | Predefined 'SNat' singleton literals
+-- | Predefined 'SNat' singleton literals in the range [0 .. 1024]
+--
+-- Defines:
+--
+-- > d0 = snat :: SNat 0
+-- > d1 = snat :: SNat 1
+-- > d2 = snat :: SNat 2
+-- > ...
+-- > d1024 = snat :: SNat 1024
+--
+-- You can generate more 'SNat' literals using 'decLiteralsD' from "CLaSH.Promoted.Nat.TH"
 module CLaSH.Promoted.Nat.Literals where
 
 import CLaSH.Promoted.Nat.TH
 
-$(decLiteralsD "d" 0 1024)
+$(decLiteralsD 0 1024)
diff --git a/src/CLaSH/Promoted/Nat/TH.hs b/src/CLaSH/Promoted/Nat/TH.hs
--- a/src/CLaSH/Promoted/Nat/TH.hs
+++ b/src/CLaSH/Promoted/Nat/TH.hs
@@ -5,27 +5,33 @@
 
 import CLaSH.Promoted.Nat
 
--- | Create an 'SNat' constant
+-- | Create an 'SNat' literal
 --
--- > $(decLiteralD "d" 1200) == d1200 = snat :: SNat 1200
-decLiteralD :: String
-            -> Integer
+-- > $(decLiteralD "d" 1200)
+--
+-- >>> :t d1200
+-- d1200 :: SNat 1200
+decLiteralD :: Integer
             -> Q [Dec]
-decLiteralD valPrefix n =
-    do let suffix  = if n < 0 then error ("Can't make negative SNat: " ++ show n) else show n
-           valName = mkName $ valPrefix ++ suffix
-       sig   <- sigD valName (appT (conT ''SNat) (litT (numTyLit n)))
-       val   <- valD (varP valName) (normalB [| snat |]) []
-       return [ sig, val ]
+decLiteralD n = do
+  let suffix  = if n < 0 then error ("Can't make negative SNat: " ++ show n) else show n
+      valName = mkName $ 'd':suffix
+  sig   <- sigD valName (appT (conT ''SNat) (litT (numTyLit n)))
+  val   <- valD (varP valName) (normalB [| snat |]) []
+  return [ sig, val ]
 
--- | Create an 'SNat' constants
+-- | Create a range of 'SNat' literals
 --
--- > $(decLiteralsD "d" 1200 1202) == d1200 = snat :: SNat 1200
--- >                                  d1201 = snat :: SNat 1201
--- >                                  d1202 = snat :: SNat 1202
-decLiteralsD :: String
-             -> Integer
+-- > $(decLiteralsD 1200 1202)
+--
+-- >>> :t d1200
+-- d1200 :: SNat 1200
+-- >>> :t d1201
+-- d1201 :: SNat 1201
+-- >>> :t d1202
+-- d1202 :: SNat 1202
+decLiteralsD :: Integer
              -> Integer
              -> Q [Dec]
-decLiteralsD valPrefix from to =
-    fmap concat $ sequence $ [ decLiteralD valPrefix n | n <- [from..to] ]
+decLiteralsD from to =
+    fmap concat $ sequence $ [ decLiteralD n | n <- [from..to] ]
diff --git a/src/CLaSH/Promoted/Ord.hs b/src/CLaSH/Promoted/Ord.hs
--- a/src/CLaSH/Promoted/Ord.hs
+++ b/src/CLaSH/Promoted/Ord.hs
@@ -4,9 +4,8 @@
 {-# LANGUAGE UndecidableInstances #-}
 module CLaSH.Promoted.Ord where
 
+import Data.Type.Bool
 import GHC.TypeLits
-
-import CLaSH.Promoted.Bool
 
 -- | Type-level 'min' function for natural numbers
 type family Min (x :: Nat) (y :: Nat) :: Nat
diff --git a/src/CLaSH/Signal.hs b/src/CLaSH/Signal.hs
deleted file mode 100644
--- a/src/CLaSH/Signal.hs
+++ /dev/null
@@ -1,286 +0,0 @@
-{-# LANGUAGE LambdaCase      #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeFamilies    #-}
-
-module CLaSH.Signal
-  ( Signal
-  , sample
-  , sampleN
-  , fromList
-  , signal
-  , register
-  , simulate
-  , Pack(..)
-  , simulateP
-  , (<^), (^>)
-  )
-where
-
-import Data.Default
-import Control.Applicative
-import Language.Haskell.TH.Syntax(Lift(..))
-
-import CLaSH.Bit            (Bit)
-import CLaSH.Sized.Signed   (Signed)
-import CLaSH.Sized.Unsigned (Unsigned)
-import CLaSH.Sized.Vector   (Vec(..), vmap, vhead, vtail)
-
-{-# NOINLINE register  #-}
-{-# NOINLINE signal    #-}
-{-# NOINLINE mapSignal #-}
-{-# NOINLINE appSignal #-}
-
-infixr 5 :-
--- | A synchronized signal with elements of type @a@
-data Signal a = a :- Signal a
-
--- | Create a 'Signal' from a list
---
--- Every element in the list will correspond to a value of the signal for one
--- clock cycle.
---
--- > sampleN 2 (fromList [1,2,3,4,5]) == [1,2]
-fromList :: [a] -> Signal a
-fromList []     = error "finite list"
-fromList (x:xs) = x :- fromList xs
-
-instance Show a => Show (Signal a) where
-  show (x :- xs) = show x ++ " " ++ show xs
-
-instance Lift a => Lift (Signal a) where
-  lift ~(x :- _) = [| signal x |]
-
-instance Default a => Default (Signal a) where
-  def = signal def
-
--- | Get an infinite list of samples from a 'Signal'
---
--- The elements in the list correspond to the values of the 'Signal' at
--- consecutive clock cycles
---
--- > sample s == [s0, s1, s2, s3, ...
-sample :: Signal a -> [a]
-sample ~(x :- xs) = x : sample xs
-
--- | Get a list of @n@ samples from a 'Signal'
---
--- The elements in the list correspond to the values of the 'Signal' at
--- consecutive clock cycles
---
--- > sampleN 3 s == [s0, s1, s2]
-sampleN :: Int -> Signal a -> [a]
-sampleN 0 _          = []
-sampleN n ~(x :- xs) = x : (sampleN (n-1) xs)
-
--- | Create a constant 'Signal' from a combinational value
---
--- > sample (signal 4) == [4, 4, 4, 4, ...
-signal :: a -> Signal a
-signal a = a :- signal a
-
-mapSignal :: (a -> b) -> Signal a -> Signal b
-mapSignal f (a :- as) = f a :- mapSignal f as
-
-appSignal :: Signal (a -> b) -> Signal a -> Signal b
-appSignal (f :- fs) ~(a :- as) = f a :- appSignal fs as
-
-instance Functor Signal where
-  fmap = mapSignal
-
-instance Applicative Signal where
-  pure  = signal
-  (<*>) = appSignal
-
-unSignal :: Signal a -> a
-unSignal (a :- _) = a
-
-next :: Signal a -> Signal a
-next (_ :- as) = as
-
-diag :: Signal (Signal a) -> Signal a
-diag (xs :- xss) = unSignal xs :- diag (fmap next xss)
-
-instance Monad Signal where
-  return    = signal
-  xs >>= f  = diag (fmap f xs)
-
--- | 'register' @i s@ delays the values in 'Signal' @s@ for one cycle, and sets
--- the value at time 0 to @i@
---
--- > sampleN 3 (register 8 (fromList [1,2,3,4])) == [8,1,2]
-register :: a -> Signal a -> Signal a
-register i s = i :- s
-
--- | Simulate a ('Signal' -> 'Signal') function given a list of samples
---
--- > simulate (register 8) [1, 2, 3, ... == [8, 1, 2, 3, ...
-simulate :: (Signal a -> Signal b) -> [a] -> [b]
-simulate f = sample . f . fromList
-
--- | Conversion between a 'Signal' of a product type (e.g. a tuple) and a
--- product type of 'Signal's
-class Pack a where
-  type SignalP a
-  -- | > pack :: (Signal a, Signal b) -> Signal (a,b)
-  -- However:
-  --
-  -- > pack :: Signal Bit -> Signal Bit
-  pack   :: SignalP a -> Signal a
-  -- | > unpack :: Signal (a,b) -> (Signal a, Signal b)
-  -- However:
-  --
-  -- > unpack :: Signal Bit -> Signal Bit
-  unpack :: Signal a -> SignalP a
-
--- | Simulate a ('SignalP' -> 'SignalP') function given a list of samples
---
--- > simulateP (unpack . register (8,8) . pack) [(1,1), (2,2), (3,3), ... == [(8,8), (1,1), (2,2), (3,3), ...
-simulateP :: (Pack a, Pack b) => (SignalP a -> SignalP b) -> [a] -> [b]
-simulateP f = simulate (pack . f . unpack)
-
-instance Pack Bit where
-  type SignalP Bit = Signal Bit
-  pack   = id
-  unpack = id
-
-instance Pack (Signed n) where
-  type SignalP (Signed n) = Signal (Signed n)
-  pack   = id
-  unpack = id
-
-instance Pack (Unsigned n) where
-  type SignalP (Unsigned n) = Signal (Unsigned n)
-  pack   = id
-  unpack = id
-
-instance Pack Bool where
-  type SignalP Bool = Signal Bool
-  pack   = id
-  unpack = id
-
-instance Pack Integer where
-  type SignalP Integer = Signal Integer
-  pack   = id
-  unpack = id
-
-instance Pack Int where
-  type SignalP Int = Signal Int
-  pack   = id
-  unpack = id
-
-instance Pack Float where
-  type SignalP Float = Signal Float
-  pack   = id
-  unpack = id
-
-instance Pack Double where
-  type SignalP Double = Signal Double
-  pack   = id
-  unpack = id
-
-instance Pack () where
-  type SignalP () = Signal ()
-  pack   = id
-  unpack = id
-
-instance Pack (a,b) where
-  type SignalP (a,b) = (Signal a, Signal b)
-  pack       = uncurry (liftA2 (,))
-  unpack tup = (fmap fst tup, fmap snd tup)
-
-instance Pack (a,b,c) where
-  type SignalP (a,b,c) = (Signal a, Signal b, Signal c)
-  pack (a,b,c) = (,,) <$> a <*> b <*> c
-  unpack tup   = (fmap (\(x,_,_) -> x) tup
-                 ,fmap (\(_,x,_) -> x) tup
-                 ,fmap (\(_,_,x) -> x) tup
-                 )
-
-instance Pack (a,b,c,d) where
-  type SignalP (a,b,c,d) = (Signal a, Signal b, Signal c, Signal d)
-  pack (a,b,c,d) = (,,,) <$> a <*> b <*> c <*> d
-  unpack tup     = (fmap (\(x,_,_,_) -> x) tup
-                   ,fmap (\(_,x,_,_) -> x) tup
-                   ,fmap (\(_,_,x,_) -> x) tup
-                   ,fmap (\(_,_,_,x) -> x) tup
-                   )
-
-instance Pack (a,b,c,d,e) where
-  type SignalP (a,b,c,d,e) = (Signal a, Signal b, Signal c, Signal d, Signal e)
-  pack (a,b,c,d,e) = (,,,,) <$> a <*> b <*> c <*> d <*> e
-  unpack tup       = (fmap (\(x,_,_,_,_) -> x) tup
-                     ,fmap (\(_,x,_,_,_) -> x) tup
-                     ,fmap (\(_,_,x,_,_) -> x) tup
-                     ,fmap (\(_,_,_,x,_) -> x) tup
-                     ,fmap (\(_,_,_,_,x) -> x) tup
-                     )
-
-instance Pack (a,b,c,d,e,f) where
-  type SignalP (a,b,c,d,e,f) = (Signal a, Signal b, Signal c, Signal d, Signal e, Signal f)
-  pack (a,b,c,d,e,f) = (,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f
-  unpack tup         = (fmap (\(x,_,_,_,_,_) -> x) tup
-                       ,fmap (\(_,x,_,_,_,_) -> x) tup
-                       ,fmap (\(_,_,x,_,_,_) -> x) tup
-                       ,fmap (\(_,_,_,x,_,_) -> x) tup
-                       ,fmap (\(_,_,_,_,x,_) -> x) tup
-                       ,fmap (\(_,_,_,_,_,x) -> x) tup
-                       )
-
-instance Pack (a,b,c,d,e,f,g) where
-  type SignalP (a,b,c,d,e,f,g) = (Signal a, Signal b, Signal c, Signal d, Signal e, Signal f, Signal g)
-  pack (a,b,c,d,e,f,g) = (,,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f <*> g
-  unpack tup           = (fmap (\(x,_,_,_,_,_,_) -> x) tup
-                         ,fmap (\(_,x,_,_,_,_,_) -> x) tup
-                         ,fmap (\(_,_,x,_,_,_,_) -> x) tup
-                         ,fmap (\(_,_,_,x,_,_,_) -> x) tup
-                         ,fmap (\(_,_,_,_,x,_,_) -> x) tup
-                         ,fmap (\(_,_,_,_,_,x,_) -> x) tup
-                         ,fmap (\(_,_,_,_,_,_,x) -> x) tup
-                         )
-
-instance Pack (a,b,c,d,e,f,g,h) where
-  type SignalP (a,b,c,d,e,f,g,h) = (Signal a, Signal b, Signal c, Signal d, Signal e, Signal f, Signal g, Signal h)
-  pack (a,b,c,d,e,f,g,h) = (,,,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f <*> g <*> h
-  unpack tup             = (fmap (\(x,_,_,_,_,_,_,_) -> x) tup
-                           ,fmap (\(_,x,_,_,_,_,_,_) -> x) tup
-                           ,fmap (\(_,_,x,_,_,_,_,_) -> x) tup
-                           ,fmap (\(_,_,_,x,_,_,_,_) -> x) tup
-                           ,fmap (\(_,_,_,_,x,_,_,_) -> x) tup
-                           ,fmap (\(_,_,_,_,_,x,_,_) -> x) tup
-                           ,fmap (\(_,_,_,_,_,_,x,_) -> x) tup
-                           ,fmap (\(_,_,_,_,_,_,_,x) -> x) tup
-                           )
-
-instance Pack (Vec n a) where
-  type SignalP (Vec n a) = Vec n (Signal a)
-  pack vs                = vmap unSignal vs :- pack (vmap next vs)
-  unpack (Nil :- _)         = Nil
-  unpack vs@((_ :> _) :- _) = fmap vhead vs :> (unpack (fmap vtail vs))
-
-
--- | Operator lifting, use in conjunction with '(^>)'
---
--- > add2 :: Signal Int -> Signal Int
--- > add2 x = x <^(+)^> (signal 2)
--- >
--- > simulate add2 [1,2,3,... == [3,4,5,...
-(<^) :: Applicative f => f a -> (a -> b -> c) -> f b -> f c
-v <^ f = liftA2 f v
-
--- | Operator lifting, use in conjunction with '(<^)'
---
--- > add2 :: Signal Int -> Signal Int
--- > add2 x = x <^(+)^> (signal 2)
--- >
--- > simulate add2 [1,2,3,... == [3,4,5,...
-(^>) :: Applicative f => (f a -> f b) -> f a -> f b
-f ^> v = f v
-
-instance Num a => Num (Signal a) where
-  (+)         = liftA2 (+)
-  (-)         = liftA2 (-)
-  (*)         = liftA2 (*)
-  negate      = fmap negate
-  abs         = fmap abs
-  signum      = fmap signum
-  fromInteger = signal . fromInteger
diff --git a/src/CLaSH/Signal/Explicit.hs b/src/CLaSH/Signal/Explicit.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Signal/Explicit.hs
@@ -0,0 +1,355 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeFamilies        #-}
+
+module CLaSH.Signal.Explicit
+  ( -- * Explicitly clocked synchronous signal
+    -- $relativeclocks
+    CSignal
+    -- * Clock domain crossing
+  , Clock (..)
+  , veryUnsafeSynchronizer
+  , fromImplicit
+  , fromExplicit
+  -- * Basic circuit functions
+  , csignal
+  , cregister
+  , CPack (..)
+  -- * Simulation functions
+  , csimulate
+  , csimulateP
+    -- * List \<-\> CSignal conversion
+  , csample
+  , csampleN
+  , cfromList
+  )
+where
+
+import Data.Coerce
+import Control.Applicative        (Applicative (..), (<$>), liftA2)
+import GHC.TypeLits               (Nat)
+
+import CLaSH.Bit                  (Bit)
+import CLaSH.Promoted.Nat         (snatToInteger)
+import CLaSH.Sized.Fixed          (Fixed)
+import CLaSH.Sized.Signed         (Signed)
+import CLaSH.Sized.Unsigned       (Unsigned)
+import CLaSH.Sized.Vector         (Vec(..), vmap, vhead, vtail)
+
+import CLaSH.Signal.Implicit
+import CLaSH.Signal.Types
+
+{-# NOINLINE cregister  #-}
+
+{-# NOINLINE veryUnsafeSynchronizer #-}
+{-# NOINLINE fromImplicit           #-}
+{-# NOINLINE fromExplicit           #-}
+
+{- $relativeclocks #relativeclocks#
+CλaSH supports explicitly clocked 'Signal's in the form of: \"@'CSignal' clk a@\",
+where @clk@ is a 'Nat'ural number corresponding to the clock period of the clock
+the signal is synchronized to. NB: \"Bad things\"™  happen when you actually use
+a clock period of @0@, so don't do that!
+
+The clock periods are however dimension-less, they do not refer to any explicit
+time-scale (e.g. nano-seconds). The reason for the lack of an explicit time-scale
+is that the CλaSH compiler would not be able guarantee that the circuit can run
+at the specified frequency.
+
+The clock periods are just there to indicate relative frequency differences
+between two different clocks. That is, a \"@'CSignal' 500 a@\" is synchronized
+to a clock that runs 6.5 times faster than the clock to which a
+\"@'CSignal' 3250 a@\" is synchronized to. NB: You should be judicious using a
+clock with period @1@ as you can never create a clock that runs faster later on!
+-}
+
+-- | Create a 'CSignal' from a list
+--
+-- Every element in the list will correspond to a value of the signal for one
+-- clock cycle.
+--
+-- NB: Simulation only!
+--
+-- >>> csampleN 2 (cfromList [1,2,3,4,5])
+-- [1,2]
+cfromList :: [a] -> CSignal t a
+cfromList = coerce . fromList
+
+-- | Get an infinite list of samples from a 'CSignal'
+--
+-- The elements in the list correspond to the values of the 'CSignal' at
+-- consecutive clock cycles
+--
+-- > csample s == [s0, s1, s2, s3, ...
+csample :: CSignal t a -> [a]
+csample = sample . coerce
+
+-- | Get a list of @n@ samples from a 'CSignal'
+--
+-- The elements in the list correspond to the values of the 'CSignal' at
+-- consecutive clock cycles
+--
+-- > csampleN 3 s == [s0, s1, s2]
+csampleN :: Int -> CSignal t a -> [a]
+csampleN n = sampleN n . coerce
+
+-- | 'cregister' @i s@ delays the values in 'CSignal' @s@ for one cycle, and sets
+-- the value at time 0 to @i@
+--
+-- > clk100 = Clock d100
+--
+-- >>> csampleN 3 (cregister d100 8 (fromList [1,2,3,4]))
+-- [8,1,2]
+cregister :: Clock clk -> a -> CSignal clk a -> CSignal clk a
+cregister _ i s = coerce (register i (coerce s))
+
+-- | Simulate a (@'CSignal' clk1 a -> 'Signal' clk2 b@) function given a list of
+-- samples of type @a@
+--
+-- >>> simulate (register 8) [1, 2, 3, ...
+-- [8, 1, 2, 3, ...
+csimulate :: (CSignal clk1 a -> CSignal clk2 b) -> [a] -> [b]
+csimulate f = csample . f . cfromList
+
+-- | Isomorphism between a @'CSignal' clk@ of a product type (e.g. a tuple) and a
+-- product type of @'CSignal' clk@'s
+class CPack a where
+  type CSignalP (clk :: Nat) a
+  type CSignalP clk a = CSignal clk a
+  -- | Example:
+  --
+  -- > cpack :: Clock clk -> (CSignal clk a, CSignal clk b) -> CSignal clk (a,b)
+  --
+  -- However:
+  --
+  -- > cpack :: Clock clk -> CSignal clk Bit -> CSignal clk Bit
+  cpack   :: Clock clk -> CSignalP clk a -> CSignal clk a
+  -- | Example:
+  --
+  -- > cunpack :: Clock clk -> CSignal clk (a,b) -> (CSignal clk a, CSignal clk b)
+  --
+  -- However:
+  --
+  -- > cunpack :: Clock clk -> CSignal clk Bit -> CSignal clk Bit
+  cunpack :: Clock clk -> CSignal clk a -> CSignalP clk a
+
+-- | Simulate a (@'CSignalP' clk1 a -> 'CSignalP' clk2 b@) function given a list
+-- of samples of type @a@
+--
+-- > clk100 = Clock d100
+--
+-- >>> csimulateP clk100 clk100 (cunpack clk100 . cregister clk100 (8,8) . cpack clk100) [(1,1), (2,2), (3,3), ...
+-- [(8,8), (1,1), (2,2), (3,3), ...
+csimulateP :: (CPack a, CPack b)
+           => Clock clk1 -- ^ 'Clock' of the incoming signal
+           -> Clock clk2 -- ^ 'Clock' of the outgoing signal
+           -> (CSignalP clk1 a -> CSignalP clk2 b) -- ^ Function to simulate
+           -> [a] -> [b]
+csimulateP clk1 clk2 f = csimulate (cpack clk2 . f . cunpack clk1)
+
+instance CPack Bit where
+  cpack   _ = id
+  cunpack _ = id
+
+instance CPack (Signed n) where
+  cpack   _ = id
+  cunpack _ = id
+
+instance CPack (Unsigned n) where
+  cpack   _ = id
+  cunpack _ = id
+
+instance CPack (Fixed frac rep size) where
+  cpack   _ = id
+  cunpack _ = id
+
+instance CPack Bool where
+  cpack   _ = id
+  cunpack _ = id
+
+instance CPack Integer where
+  cpack   _ = id
+  cunpack _ = id
+
+instance CPack Int where
+  cpack   _ = id
+  cunpack _ = id
+
+instance CPack Float where
+  cpack   _ = id
+  cunpack _ = id
+
+instance CPack Double where
+  cpack   _ = id
+  cunpack _ = id
+
+instance CPack () where
+  cpack   _ = id
+  cunpack _ = id
+
+instance CPack (a,b) where
+  type CSignalP t (a,b) = (CSignal t a, CSignal t b)
+  cpack _       = uncurry (liftA2 (,))
+  cunpack _ tup = (fmap fst tup, fmap snd tup)
+
+instance CPack (a,b,c) where
+  type CSignalP t (a,b,c) = (CSignal t a, CSignal t b, CSignal t c)
+  cpack   _ (a,b,c) = (,,) <$> a <*> b <*> c
+  cunpack _ tup     = (fmap (\(x,_,_) -> x) tup
+                      ,fmap (\(_,x,_) -> x) tup
+                      ,fmap (\(_,_,x) -> x) tup
+                      )
+
+instance CPack (a,b,c,d) where
+  type CSignalP t (a,b,c,d) = (CSignal t a, CSignal t b, CSignal t c, CSignal t d)
+  cpack   _ (a,b,c,d) = (,,,) <$> a <*> b <*> c <*> d
+  cunpack _ tup       = (fmap (\(x,_,_,_) -> x) tup
+                        ,fmap (\(_,x,_,_) -> x) tup
+                        ,fmap (\(_,_,x,_) -> x) tup
+                        ,fmap (\(_,_,_,x) -> x) tup
+                        )
+
+instance CPack (a,b,c,d,e) where
+  type CSignalP t (a,b,c,d,e) = (CSignal t a, CSignal t b, CSignal t c, CSignal t d, CSignal t e)
+  cpack _ (a,b,c,d,e) = (,,,,) <$> a <*> b <*> c <*> d <*> e
+  cunpack _ tup       = (fmap (\(x,_,_,_,_) -> x) tup
+                        ,fmap (\(_,x,_,_,_) -> x) tup
+                        ,fmap (\(_,_,x,_,_) -> x) tup
+                        ,fmap (\(_,_,_,x,_) -> x) tup
+                        ,fmap (\(_,_,_,_,x) -> x) tup
+                        )
+
+instance CPack (a,b,c,d,e,f) where
+  type CSignalP t (a,b,c,d,e,f) = (CSignal t a, CSignal t b, CSignal t c, CSignal t d, CSignal t e, CSignal t f)
+  cpack   _ (a,b,c,d,e,f) = (,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f
+  cunpack _ tup           = (fmap (\(x,_,_,_,_,_) -> x) tup
+                            ,fmap (\(_,x,_,_,_,_) -> x) tup
+                            ,fmap (\(_,_,x,_,_,_) -> x) tup
+                            ,fmap (\(_,_,_,x,_,_) -> x) tup
+                            ,fmap (\(_,_,_,_,x,_) -> x) tup
+                            ,fmap (\(_,_,_,_,_,x) -> x) tup
+                            )
+
+instance CPack (a,b,c,d,e,f,g) where
+  type CSignalP t (a,b,c,d,e,f,g) = (CSignal t a, CSignal t b, CSignal t c, CSignal t d, CSignal t e, CSignal t f, CSignal t g)
+  cpack   _ (a,b,c,d,e,f,g) = (,,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f <*> g
+  cunpack _ tup             = (fmap (\(x,_,_,_,_,_,_) -> x) tup
+                              ,fmap (\(_,x,_,_,_,_,_) -> x) tup
+                              ,fmap (\(_,_,x,_,_,_,_) -> x) tup
+                              ,fmap (\(_,_,_,x,_,_,_) -> x) tup
+                              ,fmap (\(_,_,_,_,x,_,_) -> x) tup
+                              ,fmap (\(_,_,_,_,_,x,_) -> x) tup
+                              ,fmap (\(_,_,_,_,_,_,x) -> x) tup
+                              )
+
+instance CPack (a,b,c,d,e,f,g,h) where
+  type CSignalP t (a,b,c,d,e,f,g,h) = (CSignal t a, CSignal t b, CSignal t c, CSignal t d, CSignal t e, CSignal t f, CSignal t g, CSignal t h)
+  cpack   _ (a,b,c,d,e,f,g,h) = (,,,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f <*> g <*> h
+  cunpack _ tup               = (fmap (\(x,_,_,_,_,_,_,_) -> x) tup
+                                ,fmap (\(_,x,_,_,_,_,_,_) -> x) tup
+                                ,fmap (\(_,_,x,_,_,_,_,_) -> x) tup
+                                ,fmap (\(_,_,_,x,_,_,_,_) -> x) tup
+                                ,fmap (\(_,_,_,_,x,_,_,_) -> x) tup
+                                ,fmap (\(_,_,_,_,_,x,_,_) -> x) tup
+                                ,fmap (\(_,_,_,_,_,_,x,_) -> x) tup
+                                ,fmap (\(_,_,_,_,_,_,_,x) -> x) tup
+                                )
+
+instance CPack (Vec n a) where
+  type CSignalP t (Vec n a) = Vec n (CSignal t a)
+  cpack clk vs = mkCSignal (vmap (shead . coerce) vs) (cpack clk (vmap cstail vs))
+  cunpack _      (CSignal (Nil :- _))      = Nil
+  cunpack clk vs@(CSignal ((_ :> _) :- _)) = fmap vhead vs :> cunpack clk (fmap vtail vs)
+
+-- | Synchronisation function that is basically a represented by a (bundle of)
+-- wire(s) in hardware. This function should only be used as part of a proper
+-- synchronisation component, such as a dual flip-flop synchronizer, or a FIFO
+-- with an asynchronous memory element:
+--
+-- > dualFlipFlop :: Clock clk1 -> Clock clk2
+-- >              -> CSignal clk1 Bit -> CSignal clk2 Bit
+-- > dualFlipFlop clk1 clk2 = cregister clk2 L . cregister clk2 L . veryUnsafeSynchronizer clk1 clk2
+--
+-- The 'veryUnsafeSynchronizer' works in such a way that, given 2 clocks:
+--
+-- > clk7 = Clock d7
+-- > clk2 = Clock d2
+--
+-- Oversampling followed by compression is the identity function plus 2 initial values:
+--
+-- > cregister clk7 i $
+-- > veryUnsafeSynchronizer clk2 clk7 $
+-- > cregister clk2 j $
+-- > veryUnsafeSynchronizer clk7 clk2 $
+-- > cregister clk7 k s
+-- >
+-- > ==
+-- >
+-- > i :- j :- s
+--
+-- Something we can easily observe:
+--
+-- > oversampling = cregister clk2 99 . veryUnsafeSynchronizer clk7 clk2 . cregister clk7 50
+-- > almostId     = cregister clk7 70 . veryUnsafeSynchronizer clk2 clk7
+-- >              . cregister clk2 99 . veryUnsafeSynchronizer clk7 clk2 . cregister clk7 50
+-- >
+--
+-- >>> csample (oversampling (cfromList [1..10]))
+-- [99, 50,1,1,1,2,2,2,2, 3,3,3,4,4,4,4, 5,5,5,6,6,6,6, 7,7,7,8,8,8,8, 9,9,9,10,10,10,10, ...
+-- >>> csample (almostId (cfromList [1..10]))
+-- [70, 99,1,2,3,4,5,6,7,8,9,10,...
+veryUnsafeSynchronizer :: Clock clk1 -- ^ 'Clock' of the incoming signal
+                       -> Clock clk2 -- ^ 'Clock' of the outgoing signal
+                       -> CSignal clk1 a
+                       -> CSignal clk2 a
+veryUnsafeSynchronizer (Clock clk1) (Clock clk2) s = s'
+  where
+    t1    = fromInteger (snatToInteger clk1)
+    t2    = fromInteger (snatToInteger clk2)
+    s' | t1 < t2   = compress   t2 t1 s
+       | t1 > t2   = oversample t1 t2 s
+       | otherwise = same s
+
+same :: CSignal clk1 a -> CSignal clk2 a
+same (CSignal s) = CSignal s
+
+oversample :: Int -> Int -> CSignal clk1 a -> CSignal clk2 a
+oversample high low (CSignal (s :- ss)) = CSignal (s :- oversampleS (reverse (repSchedule high low)) ss)
+
+oversampleS :: [Int] -> Signal a -> Signal a
+oversampleS sched = oversample' sched
+  where
+    oversample' []     s       = oversampleS sched s
+    oversample' (d:ds) (s:-ss) = prefixN d s (oversample' ds ss)
+
+    prefixN 0 _ s = s
+    prefixN n x s = x :- prefixN (n-1) x s
+
+compress :: Int -> Int -> CSignal clk1 a -> CSignal clk2 a
+compress high low (CSignal s) = CSignal (compressS (repSchedule high low) s)
+
+compressS :: [Int] -> Signal a -> Signal a
+compressS sched = compress' sched
+  where
+    compress' []     s           = compressS sched s
+    compress' (d:ds) ss@(s :- _) = s :- compress' ds (dropS d ss)
+
+    dropS 0 s         = s
+    dropS n (_ :- ss) = dropS (n-1) ss
+
+repSchedule :: Int -> Int -> [Int]
+repSchedule high low = take low $ repSchedule' low high 1
+  where
+    repSchedule' cnt th rep
+      | cnt < th  = repSchedule' (cnt+low) th (rep + 1)
+      | otherwise = rep : repSchedule' (cnt + low) (th + high) 1
+
+-- | Implicitly clocked signals have a clock with period 1000
+fromImplicit :: Signal a -> CSignal 1000 a
+fromImplicit s = CSignal s
+
+-- | Implicitly clocked signals have a clock with period 1000
+fromExplicit :: CSignal 1000 a -> Signal a
+fromExplicit (CSignal s) = s
diff --git a/src/CLaSH/Signal/Implicit.hs b/src/CLaSH/Signal/Implicit.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Signal/Implicit.hs
@@ -0,0 +1,248 @@
+{-# LANGUAGE LambdaCase      #-}
+{-# LANGUAGE TypeFamilies    #-}
+
+module CLaSH.Signal.Implicit
+  ( -- * Implicitly clocked synchronous signal
+    Signal
+    -- * Basic circuit functions
+  , signal
+  , register
+  , Pack(..)
+  , (<^), (^>)
+    -- * Simulation functions
+  , simulate
+  , simulateP
+    -- * List \<-\> Signal conversion
+  , sample
+  , sampleN
+  , fromList
+  )
+where
+
+import Control.Applicative
+
+import CLaSH.Bit            (Bit)
+import CLaSH.Sized.Signed   (Signed)
+import CLaSH.Sized.Unsigned (Unsigned)
+import CLaSH.Sized.Vector   (Vec(..), vmap, vhead, vtail)
+
+import CLaSH.Signal.Types
+
+{-# NOINLINE register  #-}
+
+-- | Create a 'Signal' from a list
+--
+-- Every element in the list will correspond to a value of the signal for one
+-- clock cycle.
+--
+-- NB: Simulation only!
+--
+-- >>> sampleN 2 (fromList [1,2,3,4,5])
+-- [1,2]
+fromList :: [a] -> Signal a
+fromList []     = error "finite list"
+fromList (x:xs) = x :- fromList xs
+
+-- | Get an infinite list of samples from a 'Signal'
+--
+-- The elements in the list correspond to the values of the 'Signal' at
+-- consecutive clock cycles
+--
+-- > sample s == [s0, s1, s2, s3, ...
+sample :: Signal a -> [a]
+sample ~(x :- xs) = x : sample xs
+
+-- | Get a list of @n@ samples from a 'Signal'
+--
+-- The elements in the list correspond to the values of the 'Signal' at
+-- consecutive clock cycles
+--
+-- > sampleN 3 s == [s0, s1, s2]
+sampleN :: Int -> Signal a -> [a]
+sampleN 0 _          = []
+sampleN n ~(x :- xs) = x : (sampleN (n-1) xs)
+
+-- | 'register' @i s@ delays the values in 'Signal' @s@ for one cycle, and sets
+-- the value at time 0 to @i@
+--
+-- >>> sampleN 3 (register 8 (fromList [1,2,3,4]))
+-- [8,1,2]
+register :: a -> Signal a -> Signal a
+register i s = i :- s
+
+-- | Simulate a (@'Signal' a -> 'Signal' b@) function given a list of samples of
+-- type @a@
+--
+-- >>> simulate (register 8) [1, 2, 3, ...
+-- [8, 1, 2, 3, ...
+simulate :: (Signal a -> Signal b) -> [a] -> [b]
+simulate f = sample . f . fromList
+
+-- | Isomorphism between a 'Signal' of a product type (e.g. a tuple) and a
+-- product type of 'Signal's
+class Pack a where
+  type SignalP a
+  -- | Example:
+  --
+  -- > pack :: (Signal a, Signal b) -> Signal (a,b)
+  --
+  -- However:
+  --
+  -- > pack :: Signal Bit -> Signal Bit
+  pack   :: SignalP a -> Signal a
+  -- | Example:
+  --
+  -- > unpack :: Signal (a,b) -> (Signal a, Signal b)
+  --
+  -- However:
+  --
+  -- > unpack :: Signal Bit -> Signal Bit
+  unpack :: Signal a -> SignalP a
+
+-- | Simulate a (@'SignalP' a -> 'SignalP' b@) function given a list of samples
+-- of type @a@
+--
+-- >>> simulateP (unpack . register (8,8) . pack) [(1,1), (2,2), (3,3), ...
+-- [(8,8), (1,1), (2,2), (3,3), ...
+simulateP :: (Pack a, Pack b) => (SignalP a -> SignalP b) -> [a] -> [b]
+simulateP f = simulate (pack . f . unpack)
+
+instance Pack Bit where
+  type SignalP Bit = Signal Bit
+  pack   = id
+  unpack = id
+
+instance Pack (Signed n) where
+  type SignalP (Signed n) = Signal (Signed n)
+  pack   = id
+  unpack = id
+
+instance Pack (Unsigned n) where
+  type SignalP (Unsigned n) = Signal (Unsigned n)
+  pack   = id
+  unpack = id
+
+instance Pack Bool where
+  type SignalP Bool = Signal Bool
+  pack   = id
+  unpack = id
+
+instance Pack Integer where
+  type SignalP Integer = Signal Integer
+  pack   = id
+  unpack = id
+
+instance Pack Int where
+  type SignalP Int = Signal Int
+  pack   = id
+  unpack = id
+
+instance Pack Float where
+  type SignalP Float = Signal Float
+  pack   = id
+  unpack = id
+
+instance Pack Double where
+  type SignalP Double = Signal Double
+  pack   = id
+  unpack = id
+
+instance Pack () where
+  type SignalP () = Signal ()
+  pack   = id
+  unpack = id
+
+instance Pack (a,b) where
+  type SignalP (a,b) = (Signal a, Signal b)
+  pack       = uncurry (liftA2 (,))
+  unpack tup = (fmap fst tup, fmap snd tup)
+
+instance Pack (a,b,c) where
+  type SignalP (a,b,c) = (Signal a, Signal b, Signal c)
+  pack (a,b,c) = (,,) <$> a <*> b <*> c
+  unpack tup   = (fmap (\(x,_,_) -> x) tup
+                 ,fmap (\(_,x,_) -> x) tup
+                 ,fmap (\(_,_,x) -> x) tup
+                 )
+
+instance Pack (a,b,c,d) where
+  type SignalP (a,b,c,d) = (Signal a, Signal b, Signal c, Signal d)
+  pack (a,b,c,d) = (,,,) <$> a <*> b <*> c <*> d
+  unpack tup     = (fmap (\(x,_,_,_) -> x) tup
+                   ,fmap (\(_,x,_,_) -> x) tup
+                   ,fmap (\(_,_,x,_) -> x) tup
+                   ,fmap (\(_,_,_,x) -> x) tup
+                   )
+
+instance Pack (a,b,c,d,e) where
+  type SignalP (a,b,c,d,e) = (Signal a, Signal b, Signal c, Signal d, Signal e)
+  pack (a,b,c,d,e) = (,,,,) <$> a <*> b <*> c <*> d <*> e
+  unpack tup       = (fmap (\(x,_,_,_,_) -> x) tup
+                     ,fmap (\(_,x,_,_,_) -> x) tup
+                     ,fmap (\(_,_,x,_,_) -> x) tup
+                     ,fmap (\(_,_,_,x,_) -> x) tup
+                     ,fmap (\(_,_,_,_,x) -> x) tup
+                     )
+
+instance Pack (a,b,c,d,e,f) where
+  type SignalP (a,b,c,d,e,f) = (Signal a, Signal b, Signal c, Signal d, Signal e, Signal f)
+  pack (a,b,c,d,e,f) = (,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f
+  unpack tup         = (fmap (\(x,_,_,_,_,_) -> x) tup
+                       ,fmap (\(_,x,_,_,_,_) -> x) tup
+                       ,fmap (\(_,_,x,_,_,_) -> x) tup
+                       ,fmap (\(_,_,_,x,_,_) -> x) tup
+                       ,fmap (\(_,_,_,_,x,_) -> x) tup
+                       ,fmap (\(_,_,_,_,_,x) -> x) tup
+                       )
+
+instance Pack (a,b,c,d,e,f,g) where
+  type SignalP (a,b,c,d,e,f,g) = (Signal a, Signal b, Signal c, Signal d, Signal e, Signal f, Signal g)
+  pack (a,b,c,d,e,f,g) = (,,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f <*> g
+  unpack tup           = (fmap (\(x,_,_,_,_,_,_) -> x) tup
+                         ,fmap (\(_,x,_,_,_,_,_) -> x) tup
+                         ,fmap (\(_,_,x,_,_,_,_) -> x) tup
+                         ,fmap (\(_,_,_,x,_,_,_) -> x) tup
+                         ,fmap (\(_,_,_,_,x,_,_) -> x) tup
+                         ,fmap (\(_,_,_,_,_,x,_) -> x) tup
+                         ,fmap (\(_,_,_,_,_,_,x) -> x) tup
+                         )
+
+instance Pack (a,b,c,d,e,f,g,h) where
+  type SignalP (a,b,c,d,e,f,g,h) = (Signal a, Signal b, Signal c, Signal d, Signal e, Signal f, Signal g, Signal h)
+  pack (a,b,c,d,e,f,g,h) = (,,,,,,,) <$> a <*> b <*> c <*> d <*> e <*> f <*> g <*> h
+  unpack tup             = (fmap (\(x,_,_,_,_,_,_,_) -> x) tup
+                           ,fmap (\(_,x,_,_,_,_,_,_) -> x) tup
+                           ,fmap (\(_,_,x,_,_,_,_,_) -> x) tup
+                           ,fmap (\(_,_,_,x,_,_,_,_) -> x) tup
+                           ,fmap (\(_,_,_,_,x,_,_,_) -> x) tup
+                           ,fmap (\(_,_,_,_,_,x,_,_) -> x) tup
+                           ,fmap (\(_,_,_,_,_,_,x,_) -> x) tup
+                           ,fmap (\(_,_,_,_,_,_,_,x) -> x) tup
+                           )
+
+instance Pack (Vec n a) where
+  type SignalP (Vec n a) = Vec n (Signal a)
+  pack vs                = vmap shead vs :- pack (vmap stail vs)
+  unpack (Nil :- _)         = Nil
+  unpack vs@((_ :> _) :- _) = fmap vhead vs :> (unpack (fmap vtail vs))
+
+
+-- | Operator lifting, use in conjunction with ('^>')
+--
+-- > add2 :: Signal Int -> Signal Int
+-- > add2 x = x <^(+)^> (signal 2)
+--
+-- >>> simulate add2 [1,2,3,...
+-- [3,4,5,...
+(<^) :: Applicative f => f a -> (a -> b -> c) -> f b -> f c
+v <^ f = liftA2 f v
+
+-- | Operator lifting, use in conjunction with ('<^')
+--
+-- > add2 :: Signal Int -> Signal Int
+-- > add2 x = x <^(+)^> (signal 2)
+--
+-- >>> simulate add2 [1,2,3,...
+-- [3,4,5,...
+(^>) :: Applicative f => (f a -> f b) -> f a -> f b
+f ^> v = f v
diff --git a/src/CLaSH/Signal/Types.hs b/src/CLaSH/Signal/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Signal/Types.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures             #-}
+{-# LANGUAGE TemplateHaskell            #-}
+module CLaSH.Signal.Types where
+
+import Data.Coerce                (coerce)
+import Data.Default               (Default (..))
+import Control.Applicative        (Applicative (..), liftA2)
+import GHC.TypeLits               (Nat)
+import Language.Haskell.TH.Syntax (Lift (..))
+
+import CLaSH.Promoted.Nat  (SNat)
+
+infixr 5 :-
+-- | A synchronized signal with samples of type @a@, implicitly synchronized to
+-- an unnamed global clock
+data Signal a = a :- Signal a
+
+-- | A synchronized signal with samples of type @a@, explicitly synchronized to
+-- a clock with period @clk@
+newtype CSignal (clk :: Nat) a = CSignal (Signal a)
+  deriving (Show,Default,Lift,Functor,Applicative)
+
+-- | A clock with period @clk@
+newtype Clock (clk :: Nat) = Clock (SNat clk)
+
+instance Show a => Show (Signal a) where
+  show (x :- xs) = show x ++ " " ++ show xs
+
+instance Lift a => Lift (Signal a) where
+  lift ~(x :- _) = [| signal x |]
+
+instance Default a => Default (Signal a) where
+  def = signal def
+
+{-# NOINLINE signal    #-}
+{-# NOINLINE mapSignal #-}
+{-# NOINLINE appSignal #-}
+
+-- | Create a constant 'Signal' from a combinational value
+--
+-- >>> sample (signal 4)
+-- [4, 4, 4, 4, ...
+signal :: a -> Signal a
+signal a = let s = a :- s in s
+
+mapSignal :: (a -> b) -> Signal a -> Signal b
+mapSignal f (a :- as) = f a :- mapSignal f as
+
+appSignal :: Signal (a -> b) -> Signal a -> Signal b
+appSignal (f :- fs) ~(a :- as) = f a :- appSignal fs as
+
+instance Functor Signal where
+  fmap = mapSignal
+
+instance Applicative Signal where
+  pure  = signal
+  (<*>) = appSignal
+
+shead :: Signal a -> a
+shead (x :- _)  = x
+
+stail :: Signal a -> Signal a
+stail (_ :- xs) = xs
+
+mkCSignal :: a -> CSignal clk a -> CSignal clk a
+mkCSignal a (CSignal s) = CSignal (a :- s)
+
+cstail :: CSignal t a -> CSignal t a
+cstail (CSignal s) = CSignal (stail s)
+
+-- | Create a constant 'CSignal' from a combinational value
+--
+-- >>> csample (csignal 4)
+-- [4, 4, 4, 4, ...
+csignal :: a -> CSignal t a
+csignal a = coerce (signal a)
+
+instance Num a => Num (Signal a) where
+  (+)         = liftA2 (+)
+  (-)         = liftA2 (-)
+  (*)         = liftA2 (*)
+  negate      = fmap negate
+  abs         = fmap abs
+  signum      = fmap signum
+  fromInteger = signal . fromInteger
+
+instance Num a => Num (CSignal t a) where
+  (+)         = liftA2 (+)
+  (-)         = liftA2 (-)
+  (*)         = liftA2 (*)
+  negate      = fmap negate
+  abs         = fmap abs
+  signum      = fmap signum
+  fromInteger = csignal . fromInteger
diff --git a/src/CLaSH/Sized/Fixed.hs b/src/CLaSH/Sized/Fixed.hs
--- a/src/CLaSH/Sized/Fixed.hs
+++ b/src/CLaSH/Sized/Fixed.hs
@@ -1,157 +1,522 @@
-{-# LANGUAGE DataKinds            #-}
-{-# LANGUAGE FlexibleContexts     #-}
-{-# LANGUAGE KindSignatures       #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE TemplateHaskell      #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+{-# OPTIONS_GHC -fexpose-all-unfoldings -fno-strictness #-}
+
+-- | Fixed point numbers
+--
+-- * The 'Num' operators for the given types saturate on overflow,
+--   and use truncation as the rounding method.
+--
+-- * Use @$$('fLit' d)@ to create 'Fixed' point number literals.
+-- * Use <#constraintsynonyms Constraint synonyms> when writing type signatures
+--   for polymorphic functions that use 'Fixed' point numbers.
+--
+-- BEWARE: rounding by truncation introduces a sign bias!
+--
+-- * Truncation for positive numbers effectively results in: round towards zero.
+-- * Truncation for negative numbers effectively results in: round towards -infinity.
 module CLaSH.Sized.Fixed
-  ( -- * Signed fixed point
+  ( -- * 'SFixed': 'Signed' 'Fixed' point numbers
     SFixed, sf, unSF
-    -- * Unsigned fixed point
+    -- * 'UFixed': 'Unsigned' 'Fixed' point numbers
   , UFixed, uf, unUF
+    -- * 'Fixed' point literals
+  , fLit
+    -- * 'Fixed' point wrapper
+  , Fixed (..), resizeF, fracShift, satN2
+    -- * Constraint synonyms
+    -- $constraintsynonyms
+
+    -- ** Constraint synonyms for 'SFixed'
+  , NumSFixed, AddSFixed, MultSFixed, ResizeSFC
+    -- ** Constraint synonyms for 'UFixed'
+  , NumUFixed, AddUFixed, MultUFixed, ResizeUFC
+    -- ** Constraint synonyms for 'Fixed' wrapper
+  , NumFixed, AddFixed, MultFixed, ResizeFC, SatN2C
+    -- ** Constraint synonyms for 'Signed' and 'Unsigned'
+  , SatN2SC, SatN2UC
+    -- * Proxy
+  , asFracProxy, asRepProxy
   )
 where
 
 import Control.Arrow
 import Data.Bits
 import Data.Default
-import Data.Function
 import Data.List
 import Data.Maybe
 import Data.Proxy
 import Data.Ratio
+import Data.Typeable
 import GHC.TypeLits
 import Language.Haskell.TH
 import Language.Haskell.TH.Syntax(Lift(..))
 
+import CLaSH.Bit
 import CLaSH.Class.BitVector
 import CLaSH.Class.Num
-import CLaSH.Signal
+import CLaSH.Promoted.Nat
+import CLaSH.Promoted.Ord
 import CLaSH.Sized.Signed
 import CLaSH.Sized.Unsigned
+import CLaSH.Sized.Vector
 
--- | Fixed point signed integer with @i@ integer bits and @f@ fractional bits
+-- | 'Fixed'-point number
 --
--- For now, overflow behaviour for the 'Num' functions is wrap-around, not saturate
-newtype SFixed (i :: Nat) (f :: Nat) = SF { unSF :: Signed   (i + f) }
+-- Where:
+--
+-- * @frac@ denotes the position of the virtual @point@ counting from the LSB
+--
+-- * @rep@ is the underlying representation
+--
+-- * @size@ is the number of bits used to represent the number
+--
+-- The 'Num' operators for this type saturate on overflow,
+-- and use truncation as the rounding method.
+newtype Fixed (frac :: Nat) (rep :: Nat -> *) (size :: Nat) = Fixed { unFixed :: rep size }
   deriving (Eq,Ord)
 
--- | Fixed point unsigned integer with @i@ integer bits and @f@ fractional bits
+-- | Signed 'Fixed'-point number, with @int@ integer bits (including sign-bit)
+-- and @frac@ fractional bits.
 --
--- For now, overflow behaviour for the 'Num' functions is wrap-around, not saturate
-newtype UFixed (i :: Nat) (f :: Nat) = UF { unUF :: Unsigned (i + f) }
-  deriving (Eq,Ord)
+-- * The range 'SFixed' @int@ @frac@ numbers is: [-(2^(@int@ -1)) .. 2^(@int@-1) - 2^-@frac@ ]
+-- * The resolution of 'SFixed' @int@ @frac@ numbers is: 2^@frac@
+-- * The 'Num' operators for this type saturate on overflow,
+--   and use truncation as the rounding method.
+--
+-- >>>  maxBound :: SFixed 3 4
+-- 3.9375
+-- >>> minBound :: SFixed 3 4
+-- -4.0
+-- >>> (1 :: SFixed 3 4) + (2 :: SFixed 3 4)
+-- 3.0
+-- >>> (2 :: SFixed 3 4) + (3 :: SFixed 3 4)
+-- 3.9375
+-- >>> (-2 :: SFixed 3 4) + (-3 :: SFixed 3 4)
+-- -4.0
+-- >>> ($$(fLit 1.375) :: SFixed 3 4) * ($$(fLit -0.8125) :: SFixed 3 4)
+-- -1.125
+-- >>> ($$(fLit 1.375) :: SFixed 3 4) `mult` ($$(fLit -0.8125) :: SFixed 3 4) :: SFixed 6 8
+-- -1.1171875
+-- >>> (2 :: SFixed 3 4) `plus` (3 :: SFixed 3 4) :: SFixed 4 4
+-- 5.0
+-- >>> (-2 :: SFixed 3 4) `plus` (-3 :: SFixed 3 4) :: SFixed 4 4
+-- -5.0
+type SFixed int frac = Fixed frac Signed (int + frac)
 
-fracShift :: KnownNat n => proxy n -> Int
-fracShift = fromInteger . natVal
+-- | Unsigned 'Fixed'-point number, with @int@ integer bits and @frac@ fractional bits
+--
+-- * The range 'UFixed' @int@ @frac@ numbers is: [0 .. 2^@int@ - 2^-@frac@ ]
+-- * The resolution of 'UFixed' @int@ @frac@ numbers is: 2^@frac@
+-- * The 'Num' operators for this type saturate on overflow,
+--   and use truncation as the rounding method.
+--
+-- >>> maxBound :: UFixed 3 4
+-- 7.9375
+-- >>> minBound :: UFixed 3 4
+-- 0.0
+-- >>> (1 :: UFixed 3 4) + (2 :: UFixed 3 4)
+-- 3.0
+-- >>> (2 :: UFixed 3 4) + (6 :: UFixed 3 4)
+-- 7.9375
+-- >>> (1 :: UFixed 3 4) - (3 :: UFixed 3 4)
+-- 0.0
+-- >>> ($$(fLit 1.375) :: UFixed 3 4) * ($$(fLit 0.8125) :: UFixed 3 4)
+-- 1.0625
+-- >>> ($$(fLit 1.375) :: UFixed 3 4) `mult` ($$(fLit 0.8125) :: UFixed 3 4) :: UFixed 6 8
+-- 1.1171875
+-- >>> (2 :: UFixed 3 4) `plus` (6 :: UFixed 3 4) :: UFixed 4 4
+-- 8.0
+--
+-- However, 'minus' does not saturate to 'minBound' on underflow:
+--
+-- >>> (1 :: UFixed 3 4) `minus` (3 :: UFixed 3 4) :: UFixed 4 4
+-- 14.0
+type UFixed int frac = Fixed frac Unsigned (int + frac)
 
-sf :: Signed (i + f) -> SFixed i f
-sf = SF
+-- | Treat a 'Signed' integer as a @Signed@ 'Fixed'-@point@ integer
+--
+-- >>> sf d4 (-22 :: Signed 7)
+-- -1.375
+sf :: SNat frac           -- ^ Position of the virtual @point@
+   -> Signed (int + frac) -- ^ The 'Signed' integer
+   -> SFixed int frac
+sf _ fRep = Fixed fRep
 
-uf :: Unsigned (i + f) -> UFixed i f
-uf = UF
+-- | See the underlying representation of a Signed Fixed-point integer
+unSF :: SFixed int frac
+     -> Signed (int + frac)
+unSF (Fixed fRep) = fRep
 
-showFixed :: (Bits a, KnownNat n, Show a, Integral a) =>
-             (proxy n -> a) -> proxy n -> [Char]
-showFixed unRep f = show i ++ "." ++ (uncurry pad . second (show . numerator) .
-                                      fromJust . find ((==1) . denominator . snd) .
-                                      iterate (succ *** (*10)) . (,) 0 $ (nom % denom))
+-- | Treat an 'Unsigned' integer as a @Unsigned@ 'Fixed'-@point@ number
+--
+-- >>> uf d4 (92 :: Unsigned 7)
+-- 5.75
+uf :: SNat frac             -- ^ Position of the virtual @point@
+   -> Unsigned (int + frac) -- ^ The 'Unsigned' integer
+   -> UFixed int frac
+uf _ fRep = Fixed fRep
+
+-- | See the underlying representation of an Unsigned Fixed-point integer
+unUF :: UFixed int frac
+     -> Unsigned (int + frac)
+unUF (Fixed fRep) = fRep
+
+asFracProxy :: Fixed frac rep size -> Proxy frac
+asFracProxy _ = Proxy
+
+asRepProxy :: Fixed frac rep size -> Proxy rep
+asRepProxy _ = Proxy
+
+-- | Get the position of the virtual @point@ of a 'Fixed'-@point@ number
+fracShift :: KnownNat frac => Fixed frac rep size -> Int
+fracShift f = fromInteger (natVal (asFracProxy f))
+
+instance ( Show (rep size), Bits (rep size), KnownNat frac
+         , Integral (rep size)
+         ) => Show (Fixed frac rep size) where
+  show f@(Fixed fRep) = i ++ "." ++ (uncurry pad . second (show . numerator) .
+                                          fromJust . find ((==1) . denominator . snd) .
+                                          iterate (succ *** (*10)) . (,) 0 $ (nom % denom))
     where
       pad n str = replicate (n - length str) '0' ++ str
+
       nF        = fracShift f
-      rep       = unRep f
-      i         = rep `shiftR` nF
-      nom       = toInteger rep .&. ((2 ^ nF) - 1)
+      fRepI     = toInteger fRep
+      fRepI_abs = abs fRepI
+      i         = if fRepI < 0 then '-' : show (fRepI_abs `shiftR` nF)
+                               else show (fRepI `shiftR` nF)
+      nom       = if fRepI < 0 then fRepI_abs .&. ((2 ^ nF) - 1)
+                               else fRepI .&. ((2 ^ nF) - 1)
       denom     = 2 ^ nF
 
-instance (KnownNat (i + f), KnownNat f) => Show (SFixed i f) where
-  show = showFixed unSF
+{- $constraintsynonyms #constraintsynonyms#
+Writing polymorphic functions over fixed point numbers can be a potentially
+verbose due to the many class constraints induced by the functions and operators
+of this module.
 
-instance (KnownNat (i + f), KnownNat f) => Show (UFixed i f) where
-  show = showFixed unUF
+Writing a simple multiply-and-accumulate function can already give rise to many
+lines of constraints:
 
-multFixedS :: (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f)
-           => SFixed i f -> SFixed i f -> SFixed i f
-multFixedS (SF a) (SF b) = res
-  where
-    resM = mult a b
-    resS = resM `shiftR` (fracShift res)
-    res  = SF (resizeS resS)
+@
+mac :: ( 1 <= (int + frac), (((int + frac) + 1) + 1) ~ ((int + frac) + 2)
+       , KnownNat (frac + frac), KnownNat ((int + frac) + (int + frac))
+       , KnownNat ((int + frac) + 2), KnownNat (int + frac), KnownNat frac
+       )
+    => SFixed int frac
+    -> SFixed int frac
+    -> SFixed int frac
+    -> SFixed int frac
+mac s x y = s + (x * y)
+@
 
-multFixedU :: (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f)
-           => UFixed i f -> UFixed i f -> UFixed i f
-multFixedU (UF a) (UF b) = res
-  where
-    resM = mult a b
-    resS = resM `shiftR` (fracShift res)
-    res  = UF (resizeU resS)
+But with constraint synonyms, you can write the type signature like this:
 
-fixedFromInteger :: (Bits a, KnownNat n, Num a)
-                 => (a -> proxy n) -> Integer -> proxy n
-fixedFromInteger toF i = res
-  where
-    res = toF (fromInteger i `shiftL` fracShift res)
+@
+mac :: NumSFixed int frac
+    => SFixed int frac
+    -> SFixed int frac
+    -> SFixed int frac
+    -> SFixed int frac
+mac s x y = s + (x * y)
+@
 
-instance (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f) => Num (SFixed i f) where
-  (+)           = (SF .) . on (+) unSF
-  (*)           = multFixedS
-  (-)           = (SF .) . on (-) unSF
-  negate        = SF . negate . unSF
-  abs           = SF . abs . unSF
-  signum        = SF . signum . unSF
-  fromInteger   = fixedFromInteger SF
+Where 'NumSFixed' refers to the @Constraints@ needed by the operators of
+the 'Num' class for the 'SFixed' datatype.
+-}
 
-instance (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f) => Num (UFixed i f) where
-  (+)           = (UF .) . on (+) unUF
-  (*)           = multFixedU
-  (-)           = (UF .) . on (-) unUF
-  negate        = UF . negate . unUF
-  abs           = UF . abs . unUF
-  signum        = UF . signum . unUF
-  fromInteger   = fixedFromInteger UF
+-- | Constraint for the 'Mult' instance of 'Fixed'
+type MultFixed rep (frac1 :: Nat) (frac2 :: Nat) (size1 :: Nat) (size2 :: Nat)
+  = ( Mult    (rep size1) (rep size2)
+    , MResult (rep size1) (rep size2) ~ rep (size1 + size2)
+    )
 
-instance BitVector (SFixed i f) where
-  type BitSize (SFixed i f) = i + f
-  toBV   (SF s) = toBV s
-  fromBV bv     = SF (fromBV bv)
+-- | Constraint for the 'Mult' instance of 'SFixed'
+type MultSFixed int1 frac1 int2 frac2 = MultFixed Signed frac1 frac2 (int1 + frac1) (int2 + frac2)
 
-instance BitVector (UFixed i f) where
-  type BitSize (UFixed i f) = i + f
-  toBV   (UF s) = toBV s
-  fromBV bv     = UF (fromBV bv)
+-- | Constraint for the 'Mult' instance of 'UFixed'
+type MultUFixed int1 frac1 int2 frac2 = MultFixed Unsigned frac1 frac2 (int1 + frac1) (int2 + frac2)
 
-instance Pack (SFixed i f) where
-  type SignalP (SFixed i f) = Signal (SFixed i f)
-  pack   = id
-  unpack = id
+-- | When used in a polymorphic setting, use the following <CLaSH-Sized-Fixed.html#constraintsynonyms Constraint synonyms>
+-- for less verbose type signatures:
+--
+-- * @'MultFixed' rep frac1 frac2 size1 size2@ for: 'Fixed'
+-- * @'MultSFixed' int1 frac1 int2 frac2@      for: 'SFixed'
+-- * @'MultUFixed' int1 frac1 int2 frac2@      for: 'UFixed'
+instance MultFixed rep frac1 frac2 size1 size2 => Mult (Fixed frac1 rep size1) (Fixed frac2 rep size2) where
+  type MResult (Fixed frac1 rep size1) (Fixed frac2 rep size2) = Fixed (frac1 + frac2) rep (size1 + size2)
+  mult (Fixed fRep1) (Fixed fRep2) = Fixed (mult fRep1 fRep2)
 
-instance Pack (UFixed i f) where
-  type SignalP (UFixed i f) = Signal (UFixed i f)
-  pack   = id
-  unpack = id
+-- | Constraint for the 'Add' instance of 'Fixed'
+type AddFixed rep (frac1 :: Nat) (frac2 :: Nat) (size1 :: Nat) (size2 :: Nat)
+  = ( ResizeFC rep frac1 (Max frac1 frac2) size1 ((Max size1 size2) + 1)
+    , ResizeFC rep frac2 (Max frac1 frac2) size2 ((Max size1 size2) + 1)
+    , Num (rep (Max size1 size2 + 1))
+    )
 
-instance (KnownNat i, KnownNat f, KnownNat (i + f)) => Lift (SFixed i f) where
-  lift s@(SF i) = sigE [| SF i |] (decSFixed (natVal (asProxy s)) (natVal s))
-    where
-      asProxy :: SFixed n a -> Proxy n
-      asProxy _ = Proxy
+-- | Constraint for the 'Add' instance of 'SFixed'
+type AddSFixed int1 frac1 int2 frac2 = AddFixed Signed frac1 frac2 (int1 + frac1) (int2 + frac2)
 
-instance (KnownNat i, KnownNat f, KnownNat (i + f)) => Lift (UFixed i f) where
-  lift s@(UF i) = sigE [| UF i |] (decUFixed (natVal (asProxy s)) (natVal s))
-    where
-      asProxy :: UFixed n a -> Proxy n
-      asProxy _ = Proxy
+-- | Constraint for the 'Add' instance of 'UFixed'
+type AddUFixed int1 frac1 int2 frac2 = AddFixed Unsigned frac1 frac2 (int1 + frac1) (int2 + frac2)
 
-decSFixed :: Integer -> Integer -> TypeQ
-decSFixed i f = appT (appT (conT ''SFixed) (litT $ numTyLit i)) (litT $ numTyLit f)
+-- | When used in a polymorphic setting, use the following <CLaSH-Sized-Fixed.html#constraintsynonyms Constraint synonyms>
+-- for less verbose type signatures:
+--
+-- * @'AddFixed'  rep frac1 frac2 size1 size2@ for: 'Fixed'
+-- * @'AddSFixed' int1 frac1 int2 frac2@       for: 'SFixed'
+-- * @'AddUFixed' int1 frac1 int2 frac2@       for: 'UFixed'
+instance AddFixed rep frac1 frac2 size1 size2 => Add (Fixed frac1 rep size1) (Fixed frac2 rep size2) where
+  type AResult (Fixed frac1 rep size1) (Fixed frac2 rep size2) = Fixed (Max frac1 frac2) rep ((Max size1 size2) + 1)
+  plus f1 f2  = let (Fixed f1R) = resizeF f1 :: Fixed (Max frac1 frac2) rep ((Max size1 size2) + 1)
+                    (Fixed f2R) = resizeF f2 :: Fixed (Max frac1 frac2) rep ((Max size1 size2) + 1)
+                in  Fixed (f1R + f2R)
+  minus f1 f2 = let (Fixed f1R) = resizeF f1 :: Fixed (Max frac1 frac2) rep ((Max size1 size2) + 1)
+                    (Fixed f2R) = resizeF f2 :: Fixed (Max frac1 frac2) rep ((Max size1 size2) + 1)
+                in  Fixed (f1R - f2R)
 
-decUFixed :: Integer -> Integer -> TypeQ
-decUFixed i f = appT (appT (conT ''SFixed) (litT $ numTyLit i)) (litT $ numTyLit f)
+-- | Constraint for the 'Num' instance of 'Fixed'
+type NumFixed (frac :: Nat) rep (size :: Nat)
+  = ( SatN2C   rep size
+    , ResizeFC rep (frac + frac) frac (size + size) size
+    , Num      (rep size)
+    , Num      (rep (size + 2))
+    , Mult     (rep size) (rep size)
+    , MResult  (rep size) (rep size) ~ rep (size + size)
+    )
 
-instance KnownNat (i + f) => Default (SFixed i f) where
-  def = SF 0
+-- | Constraint for the 'Num' instance of 'SFixed'
+type NumSFixed int frac = ( 1 <= (int + frac), (((int + frac) + 1) + 1) ~ ((int + frac) + 2)
+                          , KnownNat (frac + frac), KnownNat ((int + frac) + (int + frac))
+                          , KnownNat ((int + frac) + 2), KnownNat (int + frac), KnownNat frac
+                          )
+-- | Constraint for the 'Num' instance of 'UFixed'
+type NumUFixed int frac = ( 1 <= (int + frac), (((int + frac) + 1) + 1) ~ ((int + frac) + 2)
+                          , KnownNat (frac + frac), KnownNat ((int + frac) + (int + frac))
+                          , KnownNat ((int + frac) + 2), KnownNat (int + frac), KnownNat frac
+                          )
 
-instance KnownNat (i + f) => Default (UFixed i f) where
-  def = UF 0
+-- | The operators of this instance saturate on overflow, and use truncation as the rounding method.
+--
+-- When used in a polymorphic setting, use the following <CLaSH-Sized-Fixed.html#constraintsynonyms Constraint synonyms>
+-- for less verbose type signatures:
+--
+-- * @'NumFixed' frac rep size@ for: @'Fixed' frac rep size@
+-- * @'NumSFixed' int frac@     for: @'SFixed' int frac@
+-- * @'NumUFixed' int frac@     for: @'UFixed' int frac@
+instance (NumFixed frac rep size) => Num (Fixed frac rep size) where
+  (Fixed a) + (Fixed b) = Fixed (satN2 (resize a + resize b))
+  (Fixed a) * (Fixed b) = resizeF (Fixed (a `mult` b) :: Fixed (frac + frac) rep (size + size))
+  (Fixed a) - (Fixed b) = Fixed (satN2 (resize a - resize b))
+  negate (Fixed a)      = Fixed (satN2 (negate (resize a)))
+  abs (Fixed a)         = Fixed (satN2 (abs (resize a)))
+  signum (Fixed a)      = Fixed (signum a)
+  fromInteger i         = let fSH = fromInteger (natVal (Proxy :: Proxy frac))
+                              res = Fixed (fromInteger i `shiftL` fSH)
+                          in  res
+
+instance (BitVector (rep size)) => BitVector (Fixed frac rep size) where
+  type BitSize (Fixed frac rep size) = BitSize (rep size)
+  toBV (Fixed fRep) = toBV fRep
+  fromBV bv         = Fixed (fromBV bv)
+
+instance (Lift (rep size), KnownNat frac, KnownNat size, Typeable rep) =>
+         Lift (Fixed frac rep size) where
+  lift f@(Fixed fRep) = sigE [| Fixed fRep |] (decFixed (natVal (asFracProxy f)) (typeRep (asRepProxy f)) (natVal f))
+
+decFixed :: Integer -> TypeRep -> Integer -> TypeQ
+decFixed f r s = do
+  foldl appT (conT ''Fixed) [litT (numTyLit f), conT (mkName (show r)), litT (numTyLit s)]
+
+instance Default (rep size) => Default (Fixed frac rep size) where
+  def = Fixed def
+
+instance Bounded (rep size) => Bounded (Fixed frac rep size) where
+  minBound = Fixed minBound
+  maxBound = Fixed maxBound
+
+-- | Constraint for the 'resizeF' function
+type ResizeFC rep frac1 frac2 size1 size2
+  = ( Bounded (rep size2), Eq (rep size1), Ord (rep size1)
+    , Num (rep size1), Bits (rep size1), Resize rep
+    , KnownNat size2, KnownNat size1, Bits (rep size2)
+    , KnownNat frac2, KnownNat frac1, Bounded (rep size1)
+    )
+
+-- | Constraint for the 'resizeF' function, specialized for 'SFixed'
+type ResizeSFC int1 frac1 int2 frac2 = (KnownNat (int2 + frac2), KnownNat (int1 + frac1), KnownNat frac1, KnownNat frac2)
+
+-- | Constraint for the 'resizeF' function, specialized for 'UFixed'
+type ResizeUFC int1 frac1 int2 frac2 = (KnownNat (int2 + frac2), KnownNat (int1 + frac1), KnownNat frac1, KnownNat frac2)
+
+-- | Saturating resize operation, truncates for rounding
+--
+-- >>> $$(fLit 0.8125) :: SFixed 3 4
+-- 0.8125
+-- >>> resizeF ($$(fLit 0.8125) :: SFixed 3 4) :: SFixed 2 3
+-- 0.75
+-- >>> $$(fLit 3.4) :: SFixed 3 4
+-- 3.375
+-- >>> resizeF ($$(fLit 3.4) :: SFixed 3 4) :: SFixed 2 3
+-- 1.875
+-- >>> maxBound :: SFixed 2 3
+-- 1.875
+--
+-- When used in a polymorphic setting, use the following <#constraintsynonyms Constraint synonyms>
+-- for less verbose type signatures:
+--
+-- * @'ResizeFC'  rep frac1 frac2 size1 size2@ for: @'Fixed' frac1 rep size1 -> 'Fixed' frac2 rep size2@
+-- * @'ResizeSFC' int1 frac1 int2 frac2@       for: @'SFixed' int1 frac1 -> 'SFixed' int2 frac2@
+-- * @'ResizeUFC' int1 frac1 int2 frac2@       for: @'UFixed' int1 frac1 -> 'UFixed' int2 frac2@
+resizeF :: forall frac1 frac2 rep size1 size2 .
+           ResizeFC rep frac1 frac2 size1 size2
+        => Fixed frac1 rep size1
+        -> Fixed frac2 rep size2
+resizeF (Fixed fRep) = Fixed sat
+  where
+    argSZ = natVal (Proxy :: Proxy size1)
+    resSZ = natVal (Proxy :: Proxy size2)
+
+    argFracSZ = fromInteger (natVal (Proxy :: Proxy frac1))
+    resFracSZ = fromInteger (natVal (Proxy :: Proxy frac2))
+
+    -- All size and frac comparisons and related if-then-else statements should
+    -- be optimized away by the compiler
+    sat = if argSZ <= resSZ
+            -- if the argument is smaller than the result, resize before shift
+            then if argFracSZ <= resFracSZ
+                    then resize fRep `shiftL` (resFracSZ - argFracSZ)
+                    else resize fRep `shiftR` (argFracSZ - resFracSZ)
+            -- if the argument is bigger than the result, shift before resize
+            else let fMax = maxBound
+                     fMin = minBound
+                     mask = complement (resize fMax) :: rep size1
+                 in if argFracSZ <= resFracSZ
+                       then let shiftedL         = fRep `shiftL` (resFracSZ - argFracSZ)
+                                shiftedL_masked  = shiftedL .&. mask
+                                shiftedL_resized = resize shiftedL
+                            in if fRep >= 0
+                                  then if shiftedL_masked == 0
+                                          then shiftedL_resized
+                                          else fMax
+                                  else if shiftedL_masked == mask
+                                          then shiftedL_resized
+                                          else fMin
+                       else let shiftedR         = fRep `shiftR` (argFracSZ - resFracSZ)
+                                shiftedR_masked  = shiftedR .&. mask
+                                shiftedR_resized = resize shiftedR
+                            in if fRep >= 0
+                                  then if shiftedR_masked == 0
+                                          then shiftedR_resized
+                                          else fMax
+                                  else if shiftedR_masked == mask
+                                          then shiftedR_resized
+                                          else fMin
+
+-- | Constraint for the 'satN2' function
+type SatN2C rep n
+  = ( 1 <= n
+    , ((n + 1) + 1) ~ (n + 2)
+    , BitVector (rep n)
+    , BitVector (rep (n + 2))
+    , BitSize   (rep n) ~ n
+    , BitSize   (rep (n + 2)) ~ (n + 2)
+    , KnownNat  n
+    , KnownNat  (n + 2)
+    , Bounded   (rep n)
+    , Bits      (rep (n + 2))
+    )
+
+-- | Constraint for the 'satN2' function, specialized for 'Signed'
+type SatN2SC n = (1 <= n, ((n + 1) + 1) ~ (n + 2), KnownNat n, KnownNat (n + 2))
+
+-- | Constraint for the 'satN2' function, specialized for 'Unsigned'
+type SatN2UC n = (1 <= n, ((n + 1) + 1) ~ (n + 2), KnownNat n, KnownNat (n + 2))
+
+-- | Resize an (N+2)-bits number to an N-bits number, saturates to
+-- 'minBound' or 'maxBound' when the argument does not fit within
+-- the representations bounds of the result.
+--
+-- Uses cheaper saturation than 'resizeF', which is made possible by knowing
+-- that we only reduce the size by 2 bits.
+--
+-- >>> (2 :: Unsigned 2) + (3 :: Unsigned 2)
+-- 1
+-- >>> satN2 (resize (2 :: Unsigned 2) + resize (3 :: Unsigned 2)) :: Unsigned 2
+-- 3
+-- >>> satN2 (resize (1 :: Unsigned 2) + resize (1 :: Unsigned 2)) :: Unsigned 2
+-- 2
+-- >>> (2 :: Unsigned 2) - (3 :: Unsigned 2)
+-- 3
+-- >>> satN2 (resize (2 :: Unsigned 2) - resize (3 :: Unsigned 2)) :: Unsigned 2
+-- 0
+-- >>> (2 :: Signed 3) + (3 :: Signed 3)
+-- -3
+-- >>> satN2 (resize (2 :: Signed 3) + resize (3 :: Signed 3)) :: Signed 3
+-- 3
+--
+-- When used in a polymorphic setting, use the following <#constraintsynonyms Constraint synonyms>
+-- for less verbose type signatures:
+--
+-- * 'SatN2C'  for: @rep (n+2) -> rep n@
+-- * 'SatN2SC' for: @'Signed' (n+2) -> 'Signed' n@
+-- * 'SatN2UC' for: @'Unsigned' (n+2) -> 'Unsigned' n@
+satN2 :: SatN2C rep n
+      => rep (n + 2)
+      -> rep n
+satN2 rep = if isSigned rep
+              then case (cS,sn) of
+                     (L,H) -> maxBound
+                     (H,L) -> minBound
+                     _     -> fromBV s
+              else case (cS,cU) of
+                     (H,H) -> minBound
+                     (L,H) -> maxBound
+                     _     -> fromBV s
+  where
+    repBV = toBV rep
+    cS    = vhead repBV
+    cU    = vhead (vtail repBV)
+    s     = vtail (vtail repBV)
+    sn    = vhead' s
+
+-- | Convert, at compile-time, a 'Double' literal to a 'Fixed'-point literal.
+-- The conversion saturates on overflow, and uses truncation as its rounding method.
+--
+-- So when you type:
+--
+-- > n = $$(fLit 2.2867) :: SFixed 4 4
+--
+-- The compiler sees:
+--
+-- > n = Fixed (fromInteger 45) :: SFixed 4 4
+--
+-- Upon evaluation you see that the value is rounded / truncated in accordance
+-- to the fixed point representation:
+--
+-- >>> n
+-- 2.8125
+fLit :: forall frac rep size .
+        (KnownNat frac, Num (rep size), Bounded (rep size), Integral (rep size))
+     => Double
+     -> Q (TExp (Fixed frac rep size))
+fLit a = [|| Fixed (fromInteger sat) ||]
+  where
+    rMax      = toInteger (maxBound :: rep size)
+    rMin      = toInteger (minBound :: rep size)
+    sat       = if truncated > rMax
+                   then rMax
+                   else if truncated < rMin
+                           then rMin
+                           else truncated
+    truncated = truncate shifted :: Integer
+    shifted   = a * (2 ^ (natVal (Proxy :: Proxy frac)))
diff --git a/src/CLaSH/Sized/Signed.hs b/src/CLaSH/Sized/Signed.hs
--- a/src/CLaSH/Sized/Signed.hs
+++ b/src/CLaSH/Sized/Signed.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DeriveDataTypeable    #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE KindSignatures        #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -10,13 +11,13 @@
 
 module CLaSH.Sized.Signed
   ( Signed
-  , resizeS
   , resizeS_wrap
   )
 where
 
 import Data.Bits
 import Data.Default
+import Data.Typeable
 import Language.Haskell.TH
 import Language.Haskell.TH.Syntax(Lift(..))
 import GHC.TypeLits
@@ -27,8 +28,15 @@
 import CLaSH.Promoted.Ord
 import CLaSH.Sized.Vector
 
--- | Arbitrary-width signed integer represented by @n@ bits
+-- | Arbitrary-width signed integer represented by @n@ bits, including the sign bit.
+--
+-- Uses standard 2-complements representation. Meaning that, given @n@ bits,
+-- a 'Signed' @n@ number has a range of: [-(2^(@n@-1)) .. 2^(@n@-1)-1]
+--
+-- NB: The 'Num' operators perform @wrap-around@ on overflow. If you want saturation
+-- on overflow, check out the 'CLaSH.Sized.Fixed.satN2' function in "CLaSH.Sized.Fixed".
 newtype Signed (n :: Nat) = S Integer
+  deriving Typeable
 
 instance Eq (Signed n) where
   (==) = eqS
@@ -69,6 +77,7 @@
 {-# NOINLINE maxBoundS #-}
 maxBoundS = let res = S $ 2 ^ (natVal res - 1) - 1 in res
 
+-- | Operators do @wrap-around@ on overflow
 instance KnownNat n => Num (Signed n) where
   (+)         = plusS
   (-)         = minS
@@ -248,7 +257,7 @@
 
 {-# NOINLINE finiteBitSizeS #-}
 finiteBitSizeS :: KnownNat n => Signed n -> Int
-finiteBitSizeS i = let res = fromInteger (natVal i) in res
+finiteBitSizeS = fromInteger . natVal
 
 instance Show (Signed n) where
   show (S n) = show n
@@ -284,11 +293,6 @@
                     ]
 
 {-# NOINLINE resizeS #-}
--- | A sign-preserving resize operation
---
--- Increasing the size of the number replicates the sign bit to the left.
--- Truncating a number to length L keeps the sign bit and the rightmost L-1 bits.
---
 resizeS :: (KnownNat n, KnownNat m) => Signed n -> Signed m
 resizeS s@(S n) | n' <= m'  = extend
                 | otherwise = trunc
@@ -305,6 +309,12 @@
 --
 -- Increasing the size of the number replicates the sign bit to the left.
 -- Truncating a number of length N to a length L just removes the leftmost N-L bits.
---
 resizeS_wrap :: KnownNat m => Signed n -> Signed m
 resizeS_wrap (S n) = fromIntegerS_inlineable n
+
+-- | A sign-preserving resize operation
+--
+-- Increasing the size of the number replicates the sign bit to the left.
+-- Truncating a number to length L keeps the sign bit and the rightmost L-1 bits.
+instance Resize Signed where
+  resize = resizeS
diff --git a/src/CLaSH/Sized/Unsigned.hs b/src/CLaSH/Sized/Unsigned.hs
--- a/src/CLaSH/Sized/Unsigned.hs
+++ b/src/CLaSH/Sized/Unsigned.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DeriveDataTypeable    #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE KindSignatures        #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -10,12 +11,12 @@
 
 module CLaSH.Sized.Unsigned
   ( Unsigned
-  , resizeU
   )
 where
 
 import Data.Bits
 import Data.Default
+import Data.Typeable
 import Language.Haskell.TH
 import Language.Haskell.TH.Syntax(Lift(..))
 import GHC.TypeLits
@@ -27,7 +28,13 @@
 import CLaSH.Sized.Vector
 
 -- | Arbitrary-width unsigned integer represented by @n@ bits
+--
+-- Given @n@ bits, an 'Unsigned' @n@ number has a range of: [0 .. 2^@n@-1]
+--
+-- NB: The 'Num' operators perform @wrap-around@ on overflow. If you want saturation
+-- on overflow, check out the 'CLaSH.Sized.Fixed.satN2' function in "CLaSH.Sized.Fixed".
 newtype Unsigned (n :: Nat) = U Integer
+  deriving Typeable
 
 instance Eq (Unsigned n) where
   (==) = eqU
@@ -66,6 +73,7 @@
 maxBoundU :: KnownNat n => Unsigned n
 maxBoundU = let res = U ((2 ^ natVal res) - 1) in res
 
+-- | Operators do @wrap-around@ on overflow
 instance KnownNat n => Num (Unsigned n) where
   (+)         = plusU
   (-)         = minU
@@ -263,11 +271,13 @@
                     ]
 
 {-# NOINLINE resizeU #-}
--- | A resize operation that is zero-extends on extension, and wraps on truncation.
+resizeU :: KnownNat m => Unsigned n -> Unsigned m
+resizeU (U n) = fromIntegerU_inlineable n
+
+-- | A resize operation that zero-extends on extension, and wraps on truncation.
 --
 -- Increasing the size of the number extends with zeros to the left.
 -- Truncating a number of length N to a length L just removes the left
 -- (most significant) N-L bits.
---
-resizeU :: KnownNat m => Unsigned n -> Unsigned m
-resizeU (U n) = fromIntegerU_inlineable n
+instance Resize Unsigned where
+  resize = resizeU
diff --git a/src/CLaSH/Sized/Vector.hs b/src/CLaSH/Sized/Vector.hs
--- a/src/CLaSH/Sized/Vector.hs
+++ b/src/CLaSH/Sized/Vector.hs
@@ -10,22 +10,32 @@
 {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
 
 module CLaSH.Sized.Vector
-  ( Vec(..), (<:)
+  ( -- * 'Vec'tor constructors
+    Vec(..), (<:)
+    -- * Standard 'Vec'tor functions
+    -- ** Extracting sub-'Vec'tors
   , vhead, vtail, vlast, vinit
-  , (+>>), (<<+), (<++>), vconcat
+  , vtake, vtakeI, vdrop, vdropI, vexact, vselect, vselectI
+    -- ** Combining 'Vec'tors
+  , (+>>), (<<+), (<++>), vconcat, vzip, vunzip
+    -- ** Splitting 'Vec'tors
   , vsplit, vsplitI, vunconcat, vunconcatI, vmerge
-  , vreverse, vmap, vzipWith
+    -- ** Applying functions to 'Vec'tor elements
+  , vmap, vzipWith
   , vfoldr, vfoldl, vfoldr1, vfoldl1
-  , vzip, vunzip
+    -- ** Indexing 'Vec'tors
   , (!), vreplace, maxIndex, vlength
-  , vtake, vtakeI, vdrop, vdropI, vexact, vselect, vselectI
+    -- ** Generating 'Vec'tors
   , vcopy, vcopyI, viterate, viterateI, vgenerate, vgenerateI
-  , toList, v, lazyV, asNatProxy
+    -- ** Misc
+  , vreverse, toList, v, lazyV, asNatProxy
+    -- * Alternative 'Vec'tor functions
+  , vhead'
   )
 where
 
 import Control.Applicative
-import Data.Traversable
+-- import Data.Traversable
 import Data.Foldable              hiding (toList)
 import Data.Proxy
 import GHC.TypeLits
@@ -35,6 +45,16 @@
 
 import CLaSH.Promoted.Nat
 
+-- | Fixed size vectors
+--
+-- * Lists with their length encoded in their type
+-- * 'Vec'tor elements have a descending subscript starting from 'maxIndex' ('vlength' - 1)
+--   and ending at 0
+--
+-- >>> (3:>4:>5:>Nil)
+-- <3,4,5>
+-- >>> :t (3:>4:>5:>Nil)
+-- (3:>4:>5:>Nil) :: Num a => Vec 3 a
 data Vec :: Nat -> * -> * where
   Nil  :: Vec 0 a
   (:>) :: a -> Vec n a -> Vec (n + 1) a
@@ -56,37 +76,58 @@
   pure  = vcopyI
   (<*>) = vzipWith ($)
 
-instance Traversable (Vec n) where
-  traverse _ Nil       = pure Nil
-  traverse f (x :> xs) = (:>) <$> f x <*> traverse f xs
+-- instance Traversable (Vec n) where
+--   traverse _ Nil       = pure Nil
+--   traverse f (x :> xs) = (:>) <$> f x <*> traverse f xs
 
 instance Foldable (Vec n) where
-  foldMap = foldMapDefault
+  foldr = vfoldr
 
 instance Functor (Vec n) where
-  fmap = fmapDefault
+  fmap = vmap
 
 {-# NOINLINE vhead #-}
 -- | Extract the first element of a vector
 --
--- > vhead (1:>2:>3:>Nil) == 1
--- > vhead Nil            == TYPE ERROR
+-- >>> vhead (1:>2:>3:>Nil)
+-- 1
+-- >>> vhead Nil
+--   <interactive>
+--       Couldn't match type ‘1’ with ‘0’
+--       Expected type: Vec (0 + 1) a
+--         Actual type: Vec 0 a
+--       In the first argument of ‘vhead’, namely ‘Nil’
+--       In the expression: vhead Nil
 vhead :: Vec (n + 1) a -> a
 vhead (x :> _) = x
 
 {-# NOINLINE vtail #-}
 -- | Extract the elements after the head of a vector
 --
--- > vtail (1:>2:>3:>Nil) == (2:>3:>Nil)
--- > vtail Nil            == TYPE ERROR
+-- >>> vtail (1:>2:>3:>Nil)
+-- <2,3>
+-- >>> vtail Nil
+--   <interactive>
+--       Couldn't match type ‘1’ with ‘0’
+--       Expected type: Vec (0 + 1) a
+--         Actual type: Vec 0 a
+--       In the first argument of ‘vtail’, namely ‘Nil’
+--       In the expression: vtail Nil
 vtail :: Vec (n + 1) a -> Vec n a
 vtail (_ :> xs) = unsafeCoerce xs
 
 {-# NOINLINE vlast #-}
 -- | Extract the last element of a vector
 --
--- > vlast (1:>2:>3:>Nil) == 3
--- > vlast Nil            == TYPE ERROR
+-- >>> vlast (1:>2:>3:>Nil)
+-- 3
+-- >>> vlast Nil
+--   <interactive>
+--       Couldn't match type ‘1’ with ‘0’
+--       Expected type: Vec (0 + 1) a
+--         Actual type: Vec 0 a
+--       In the first argument of ‘vlast’, namely ‘Nil’
+--       In the expression: vlast Nil
 vlast :: Vec (n + 1) a -> a
 vlast (x :> Nil)     = x
 vlast (_ :> y :> ys) = vlast (y :> ys)
@@ -94,8 +135,15 @@
 {-# NOINLINE vinit #-}
 -- | Extract all the elements of a vector except the last element
 --
--- > vinit (1:>2:>3:>Nil) == (1:>2:>Nil)
--- > vinit Nil            == TYPE ERROR
+-- >>> vinit (1:>2:>3:>Nil)
+-- <1,2>
+-- >>> vinit Nil
+--   <interactive>
+--       Couldn't match type ‘1’ with ‘0’
+--       Expected type: Vec (0 + 1) a
+--         Actual type: Vec 0 a
+--       In the first argument of ‘vinit’, namely ‘Nil’
+--       In the expression: vinit Nil
 vinit :: Vec (n + 1) a -> Vec n a
 vinit (_ :> Nil)     = unsafeCoerce Nil
 vinit (x :> y :> ys) = unsafeCoerce (x :> vinit (y :> ys))
@@ -112,8 +160,10 @@
 -- | Add an element to the head of the vector, and extract all elements of the
 -- resulting vector except the last element
 --
--- > 1 +>> (3:>4:>5:>Nil) == (1:>3:>4:>Nil)
--- > 1 +>> Nil            == Nil
+-- >>> 1 +>> (3:>4:>5:>Nil)
+-- <1,3,4>
+-- >>> 1 +>> Nil
+-- <>
 (+>>) :: a -> Vec n a -> Vec n a
 s +>> xs = shiftIntoL s xs
 
@@ -127,8 +177,10 @@
 {-# INLINEABLE (<:) #-}
 -- | Add an element to the tail of the vector
 --
--- > (3:>4:>5:>Nil) <: 1 == (3:>4:>5:>1:>Nil)
--- > Nil            <: 1 == (1:>Nil)
+-- >>> (3:>4:>5:>Nil) <: 1
+-- <3,4,5,1>
+-- >>> :t (3:>4:>5:>Nil) <: 1
+-- (3:>4:>5:>Nil) <: 1 :: Num a => Vec 4 a
 (<:) :: Vec n a -> a -> Vec (n + 1) a
 xs <: s = snoc s xs
 
@@ -144,8 +196,10 @@
 -- | Add an element to the tail of the vector, and extract all elements of the
 -- resulting vector except the first element
 --
--- > (3:>4:>5:>Nil) <<+ 1 == (4:>5:>1:>Nil)
--- > Nil            <<+ 1 == Nil
+-- >>> (3:>4:>5:>Nil) <<+ 1
+-- <4,5,1>
+-- >>> Nil <<+ 1
+-- <>
 (<<+) :: Vec n a -> a -> Vec n a
 xs <<+ s = shiftIntoR s xs
 
@@ -159,15 +213,18 @@
 {-# INLINE (<++>) #-}
 -- | Append two vectors
 --
--- > (1:>2:>3:>Nil) <++> (7:>8:>Nil) = (1:>2:>3:>7:>8:>Nil)
+-- >>> (1:>2:>3:>Nil) <++> (7:>8:>Nil)
+-- <1,2,3,7,8>
 (<++>) :: Vec n a -> Vec m a -> Vec (n + m) a
 xs <++> ys = vappend xs ys
 
 {-# NOINLINE vsplit #-}
 -- | Split a vector into two vectors at the given point
 --
--- > vsplit (snat :: SNat 3) (1:>2:>3:>7:>8:>Nil) == (1:>2:>3:>Nil, 7:>8:>Nil)
--- > vsplit d3               (1:>2:>3:>7:>8:>Nil) == (1:>2:>3:>Nil, 7:>8:>Nil)
+-- >>> vsplit (snat :: SNat 3) (1:>2:>3:>7:>8:>Nil)
+-- (<1,2,3>, <7,8>)
+-- >>> vsplit d3 (1:>2:>3:>7:>8:>Nil)
+-- (<1,2,3>, <7,8>)
 vsplit :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
 vsplit n xs = vsplitU (toUNat n) xs
 
@@ -179,17 +236,17 @@
 {-# INLINEABLE vsplitI #-}
 -- | Split a vector into two vectors where the length of the two is determined
 -- by the context
+--
+-- >>> vsplitI (1:>2:>3:>7:>8:>Nil) :: (Vec 2 Int, Vec 3 Int)
+-- (<1,2>,<3,7,8>)
 vsplitI :: KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a)
 vsplitI = withSNat vsplit
 
 {-# NOINLINE vconcat #-}
 -- | Concatenate a vector of vectors
 --
--- > vunconcat ((1:>2:>3:>Nil)    :>
--- >            (4:>5:>6:>Nil)    :>
--- >            (7:>8:>9:>Nil)    :>
--- >            (10:>11:>12:>Nil) :>
--- >            Nil)                  == (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)
+-- >>> vconcat ((1:>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil)
+-- <1,2,3,4,5,6,7,8,9,10,11,12>
 vconcat :: Vec n (Vec m a) -> Vec (n * m) a
 vconcat Nil       = Nil
 vconcat (x :> xs) = unsafeCoerce (vappend x (vconcat xs))
@@ -198,10 +255,8 @@
 -- | Split a vector of (n * m) elements into a vector of vectors with length m,
 -- where m is given
 --
--- > vunconcat d4 (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) == ((1:>2:>3:>4:>Nil)    :>
--- >                                                               (5:>6:>7:>8:>Nil)    :>
--- >                                                               (9:>10:>11:>12:>Nil) :>
--- >                                                               Nil)
+-- >>> vunconcat d4 (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)
+-- <<1,2,3,4>,<5,6,7,8>,<9,10,11,12>>
 vunconcat :: KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a)
 vunconcat n xs = vunconcatU (withSNat toUNat) (toUNat n) xs
 
@@ -213,20 +268,26 @@
 {-# INLINEABLE vunconcatI #-}
 -- | Split a vector of (n * m) elements into a vector of vectors with length m,
 -- where m is determined by the context
+--
+-- >>> vunconcatI (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) :: Vec 2 (Vec 6 Int)
+-- <<1,2,3,4,5,6>,<7,8,9,10,11,12>>
 vunconcatI :: (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a)
 vunconcatI = withSNat vunconcat
 
 {-# NOINLINE vmerge #-}
 -- | Merge two vectors, alternating their elements, i.e.,
 --
--- > vmerge (xn :> ... :> x2 :> x1 :> Nil)  (yn :> ... :> y2 :> y1 :> Nil) == (xn :> yn :> ... :> x2 :> y2 :> x1 :> y1 :> Nil)
---
+-- >>> vmerge (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> 7 :> 8 :> Nil)
+-- <1,5,2,6,3,7,4,8>
 vmerge :: Vec n a -> Vec n a -> Vec (n + n) a
 vmerge Nil       Nil       = Nil
 vmerge (x :> xs) (y :> ys) = unsafeCoerce (x :> y :> (vmerge xs (unsafeCoerce ys)))
 
 {-# NOINLINE vreverse #-}
 -- | Returns the elements in a list in reverse order
+--
+-- >>> vreverse (1:>2:>3:>4:>Nil)
+-- <4,3,2,1>
 vreverse :: Vec n a -> Vec n a
 vreverse Nil        = Nil
 vreverse (x :> xs)  = vreverse xs <: x
@@ -297,7 +358,8 @@
 {-# NOINLINE vzip #-}
 -- | 'vzip' takes two lists and returns a list of corresponding pairs.
 --
--- > vzip (xn :> ... :> x2 :> x1 :> Nil) (yn :> ... :> y2 :> y1 :> Nil) == ((xn,yn) :> ... :> ... (x2,y2) :> (x1,y1) :> Nil)
+-- >>> vzip (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil)
+-- <(1,4),(2,3),(3,2),(4,1)>
 vzip :: Vec n a -> Vec n b -> Vec n (a,b)
 vzip Nil       Nil       = Nil
 vzip (x :> xs) (y :> ys) = (x,y) :> (vzip xs (unsafeCoerce ys))
@@ -306,7 +368,8 @@
 -- | 'vunzip' transforms a list of pairs into a list of first components
 -- and a list of second components.
 --
--- > vunzip ((xn,yn) :> ... :> ... (x2,y2) :> (x1,y1) :> Nil) == (xn :> ... :> x2 :> x1 :> Nil, yn :> ... :> y2 :> y1 :> Nil)
+-- >>> vunzip ((1,4):>(2,3):>(3,2):>(4,1):>Nil)
+-- (<1,2,3,4>,<4,3,2,1>)
 vunzip :: Vec n (a,b) -> (Vec n a, Vec n b)
 vunzip Nil = (Nil,Nil)
 vunzip ((a,b) :> xs) = let (as,bs) = vunzip xs
@@ -328,24 +391,30 @@
 -- | Vector index (subscript) operator, descending from 'maxIndex', where the
 -- last element has subscript 0.
 --
--- > (1:>2:>3:>4:>5:>Nil) ! 4        == 1
--- > (1:>2:>3:>4:>5:>Nil) ! maxIndex == 1
--- > (1:>2:>3:>4:>5:>Nil) ! 1        == 4
--- > (1:>2:>3:>4:>5:>Nil) ! 14       == RUNTIME ERROR: Out of bounds
+-- >>> (1:>2:>3:>4:>5:>Nil) ! 4
+-- 1
+-- >>> (1:>2:>3:>4:>5:>Nil) ! maxIndex
+-- 1
+-- >>> (1:>2:>3:>4:>5:>Nil) ! 1
+-- 4
+-- >>> (1:>2:>3:>4:>5:>Nil) ! 14
+-- *** Exception: index out of bounds
 (!) :: (KnownNat n, Integral i) => Vec n a -> i -> a
 xs ! i = vindex_integer xs (toInteger i)
 
 {-# NOINLINE maxIndex #-}
 -- | Index (subscript) of the head of the 'Vec'tor
 --
--- > maxIndex (6 :> 7 :> 8 :> Nil) == 2
+-- >>> maxIndex (6 :> 7 :> 8 :> Nil)
+-- 2
 maxIndex :: KnownNat n => Vec n a -> Integer
 maxIndex = subtract 1 . vlength
 
 {-# NOINLINE vlength #-}
 -- | Length of a 'Vec'tor as an Integer
 --
--- > vlength (6 :> 7 :> 8 :> Nil) == 3
+-- >>> vlength (6 :> 7 :> 8 :> Nil)
+-- 3
 vlength :: KnownNat n => Vec n a -> Integer
 vlength = natVal . asNatProxy
 
@@ -364,51 +433,85 @@
   Nothing -> error "index out of bounds"
 
 {-# INLINEABLE vreplace #-}
--- | Replace an element of a vector at the given index (subscript), NB: vector
--- elements have a descending subscript starting from 'maxIndex' and ending at 0
+-- | Replace an element of a vector at the given index (subscript).
 --
--- > vreplace (1:>2:>3:>4:>5:>Nil) 3 7 == (1:>7:>3:>4:>5:>Nil)
--- > vreplace (1:>2:>3:>4:>5:>Nil) 0 7 == (1:>2:>3:>4:>7:>Nil)
--- > vreplace (1:>2:>3:>4:>5:>Nil) 9 7 == RUNTIME ERROR: Out of bounds
+-- NB: vector elements have a descending subscript starting from 'maxIndex' and
+-- ending at 0
+--
+-- >>> vreplace (1:>2:>3:>4:>5:>Nil) 3 7
+-- <1,7,3,4,5>
+-- >>> vreplace (1:>2:>3:>4:>5:>Nil) 0 7
+-- <1,2,3,4,7>
+-- >>> vreplace (1:>2:>3:>4:>5:>Nil) 9 7
+-- <*** Exception: index out of bounds
 vreplace :: (KnownNat n, Integral i) => Vec n a -> i -> a -> Vec n a
 vreplace xs i y = vreplace_integer xs (toInteger i) y
 
 {-# NOINLINE vtake #-}
 -- | 'vtake' @n@, applied to a vector @xs@, returns the @n@-length prefix of @xs@
 --
--- > vtake (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil) == (1:>2:>3:>Nil)
--- > vtake d3               (1:>2:>3:>4:>5:>Nil) == (1:>2:>3:>Nil)
--- > vtake d0               (1:>2:>Nil)          == Nil
--- > vtake d4               (1:>2:>Nil)          == TYPE ERROR
+-- >>> vtake (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
+-- <1,2,3>
+-- >>> vtake d3               (1:>2:>3:>4:>5:>Nil)
+-- <1,2,3>
+-- >>> vtake d0               (1:>2:>Nil)
+-- <>
+-- >>> vtake d4               (1:>2:>Nil)
+--   <interactive>
+--       Couldn't match type ‘4 + n0’ with ‘2’
+--       The type variable ‘n0’ is ambiguous
+--       Expected type: Vec (4 + n0) a
+--         Actual type: Vec (1 + 1) a
+--       In the second argument of ‘vtake’, namely ‘(1 :> 2 :> Nil)’
+--       In the expression: vtake d4 (1 :> 2 :> Nil)
+--       In an equation for ‘it’: it = vtake d4 (1 :> 2 :> Nil)
 vtake :: SNat m -> Vec (m + n) a -> Vec m a
 vtake n = fst . vsplit n
 
 {-# INLINEABLE vtakeI #-}
 -- | 'vtakeI' @xs@, returns the prefix of @xs@ as demanded by the context
+--
+-- >>> vtakeI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
+-- <1,2>
 vtakeI :: KnownNat m => Vec (m + n) a -> Vec m a
 vtakeI = withSNat vtake
 
 {-# NOINLINE vdrop #-}
 -- | 'vdrop' @n xs@ returns the suffix of @xs@ after the first @n@ elements
 --
--- > vdrop (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil) == (4:>5:>Nil)
--- > vdrop d3               (1:>2:>3:>4:>5:>Nil) == (4:>5:>Nil)
--- > vdrop d0               (1:>2:>Nil)          == (1:>2:>Nil)
--- > vdrop d4               (1:>2:>Nil)          == TYPE ERROR
+-- >>> vdrop (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
+-- <4,5>
+-- >>> vdrop d3               (1:>2:>3:>4:>5:>Nil)
+-- <4,5>
+-- >>> vdrop d0               (1:>2:>Nil)
+-- <1,2>
+-- >>> vdrop d4               (1:>2:>Nil)
+--   <interactive>
+--       Couldn't match expected type ‘2’ with actual type ‘4 + n0’
+--       The type variable ‘n0’ is ambiguous
+--       In the first argument of ‘print’, namely ‘it’
+--       In a stmt of an interactive GHCi command: print it
 vdrop :: SNat m -> Vec (m + n) a -> Vec n a
 vdrop n = snd . vsplit n
 
 {-# INLINEABLE vdropI #-}
 -- | 'vdropI' @xs@, returns the suffix of @xs@ as demanded by the context
+--
+-- >>> vdropI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
+-- <4,5>
 vdropI :: KnownNat m => Vec (m + n) a -> Vec n a
 vdropI = withSNat vdrop
 
 {-# NOINLINE vexact #-}
--- | 'vexact' @n xs@ returns @n@'th element of @xs@, NB: vector elements
--- have a descending subscript starting from 'maxIndex' and ending at 0
+-- | 'vexact' @n xs@ returns @n@'th element of @xs@
 --
--- > vexact (snat :: SNat 1) (1:>2:>3:>4:>5:>Nil) == 4
--- > vexact d1               (1:>2:>3:>4:>5:>Nil) == 4
+-- NB: vector elements have a descending subscript starting from 'maxIndex' and
+-- ending at 0
+--
+-- >>> vexact (snat :: SNat 1) (1:>2:>3:>4:>5:>Nil)
+-- 4
+-- >>> vexact d1               (1:>2:>3:>4:>5:>Nil)
+-- 4
 vexact :: SNat m -> Vec (m + (n + 1)) a -> a
 vexact n xs = vhead $ snd $ vsplit n (vreverse xs)
 
@@ -416,8 +519,10 @@
 -- | 'vselect' @f s n xs@ selects @n@ elements with stepsize @s@ and
 -- offset @f@ from @xs@
 --
--- > vselect (snat :: SNat 1) (snat :: SNat 2) (snat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil) == (2:>4:>6:>Nil)
--- > vselect d1 d2 d3                                           (1:>2:>3:>4:>5:>6:>7:>8:>Nil) == (2:>4:>6:>Nil)
+-- >>> vselect (snat :: SNat 1) (snat :: SNat 2) (snat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
+-- <2,4,6>
+-- >>> vselect d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
+-- <2,4,6>
 vselect :: ((f + (s * n) + 1) <= i)
         => SNat f
         -> SNat s
@@ -433,6 +538,9 @@
 {-# NOINLINE vselectI #-}
 -- | 'vselectI' @f s xs@ selects as many elements as demanded by the context
 -- with stepsize @s@ and offset @f@ from @xs@
+--
+-- >>> vselectI d1 d2 (1:>2:>3:>4:>5:>6:>7:>8:>Nil) :: Vec 2 Int
+-- <2,4>
 vselectI :: ((f + (s * n) + 1) <= i, KnownNat (n + 1))
          => SNat f
          -> SNat s
@@ -443,8 +551,10 @@
 {-# NOINLINE vcopy #-}
 -- | 'vcopy' @n a@ returns a vector that has @n@ copies of @a@
 --
--- > vcopy (snat :: SNat 3) 6 == (6:>6:>6:>Nil)
--- > vcopy d3 6               == (6:>6:>6:>Nil)
+-- >>> vcopy (snat :: SNat 3) 6
+-- <6,6,6>
+-- >>> vcopy d3 6
+-- <6,6,6>
 vcopy :: SNat n -> a -> Vec n a
 vcopy n a = vreplicateU (toUNat n) a
 
@@ -455,6 +565,9 @@
 {-# INLINEABLE vcopyI #-}
 -- | 'vcopyI' @a@ creates a vector with as many copies of @a@ as demanded by the
 -- context
+--
+-- >>> vcopy 6 :: Vec 5 Int
+-- <6,6,6,6,6>
 vcopyI :: KnownNat n => a -> Vec n a
 vcopyI = withSNat vcopy
 
@@ -474,6 +587,8 @@
 {-# INLINEABLE viterateI #-}
 -- | 'viterate' @f x@ returns a vector starting with @x@ followed by @n@
 -- repeated applications of @f@ to @x@, where @n@ is determined by the context
+--
+-- > viterateI f x :: Vec 3 a == (x :> f x :> f (f x) :> Nil)
 viterateI :: KnownNat n => (a -> a) -> a -> Vec n a
 viterateI = withSNat viterate
 
@@ -489,17 +604,27 @@
 {-# INLINEABLE vgenerateI #-}
 -- | 'vgenerate' @f x@ returns a vector with @n@ repeated applications of @f@
 -- to @x@, where @n@ is determined by the context
+--
+-- > vgenerateI f x :: Vec 3 a == (f x :> f (f x) :> f (f (f x)) :> Nil)
 vgenerateI :: KnownNat n => (a -> a) -> a -> Vec n a
 vgenerateI = withSNat vgenerate
 
 {-# INLINEABLE toList #-}
 -- | Convert a vector to a list
+--
+-- >>> toList (1:>2:>3:>Nil)
+-- [1,2,3]
 toList :: Vec n a -> [a]
 toList = vfoldr (:) []
 
 -- | Create a vector literal from a list literal
 --
 -- > $(v [1::Signed 8,2,3,4,5]) == (8:>2:>3:>4:>5:>Nil) :: Vec 5 (Signed 8)
+--
+-- >>> [1 :: Signed 8,2,3,4,5]
+-- [1,2,3,4,5]
+-- >>> $(v [1::Signed 8,2,3,4,5])
+-- <1,2,3,4,5>
 v :: Lift a => [a] -> ExpQ
 v []     = [| Nil |]
 v (x:xs) = [| x :> $(v xs) |]
@@ -526,8 +651,8 @@
 --
 -- Will not terminate because 'vzipWith' is too strict in its left argument:
 --
--- > *Main> sortV (4 :> 1 :> 2 :> 3 :> Nil)
--- > <*** Exception: <<loop>>
+-- >>> sortV (4 :> 1 :> 2 :> 3 :> Nil)
+-- <*** Exception: <<loop>>
 --
 -- In this case, adding 'lazyV' on 'vzipWith's left argument:
 --
@@ -539,8 +664,8 @@
 --
 -- Results in a successful computation:
 --
--- > *Main> sortVL (4 :> 1 :> 2 :> 3 :> Nil)
--- > <1,2,3,4>
+-- >>> sortVL (4 :> 1 :> 2 :> 3 :> Nil)
+-- <1,2,3,4>
 lazyV :: KnownNat n
       => Vec n a
       -> Vec n a
@@ -549,3 +674,11 @@
     lazyV' :: Vec n a -> Vec n a -> Vec n a
     lazyV' Nil       _  = Nil
     lazyV' (_ :> xs) ys = vhead ys :> lazyV' xs (vtail ys)
+
+{-# NOINLINE vhead' #-}
+-- | Same as 'vhead', but with a "@(1 <= n)@" constraint and "@Vec n a@" argument,
+-- instead of a "@Vec (n + 1) a@" argument
+vhead' :: (1 <= n)
+       => Vec n a
+       -> a
+vhead' (x :> _) = x
diff --git a/src/CLaSH/Tutorial.hs b/src/CLaSH/Tutorial.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Tutorial.hs
@@ -0,0 +1,860 @@
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+
+{-|
+Copyright : © Christiaan Baaij, 2014
+Licence   : Creative Commons 4.0 (CC BY-NC 4.0) (http://creativecommons.org/licenses/by-nc/4.0/)
+-}
+module CLaSH.Tutorial (
+  -- * Introduction
+  -- $introduction
+
+  -- * Installation
+  -- $installation
+
+  -- * Working with this tutorial
+  -- $working
+
+  -- * Your first circuit
+  -- $mac_example
+
+  -- *** Sequential circuit
+  -- $mac2
+
+  -- *** Creating VHDL
+  -- $mac3
+
+  -- *** Circuit testbench
+  -- $mac4
+
+  -- *** Alternative specifications
+  -- $mac5
+
+  -- * Higher-order functions
+  -- $higher_order
+
+  -- * Composition of sequential circuits
+  -- $composition_sequential
+
+  -- * Conclusion
+  -- $conclusion
+
+  -- * Troubleshooting
+  -- $errorsandsolutions
+
+  -- * Unsupported Haskell features
+  -- $unsupported
+  )
+where
+
+import CLaSH.Prelude
+import CLaSH.Prelude.Explicit
+
+{- $introduction
+CλaSH (pronounced ‘clash’) is a functional hardware description language that
+borrows both its syntax and semantics from the functional programming language
+Haskell. The merits of using a functional language to describe hardware comes
+from the fact that combinational circuits can be directly modeled as
+mathematical functions and that functional languages lend themselves very well
+at describing and (de-)composing mathematical functions.
+
+Although we say that CλaSH borrows the semantics of Haskell, that statement
+should be taken with a grain of salt. What we mean to say is that the CλaSH
+compiler views a circuit description as /structural/ description. This means,
+in an academic handwavy way, that every function denotes a component and every
+function application denotes an instantiation of said component. Now, this has
+consequences on how we view /recursive/ functions: structurally, a recursive
+function would denote an /infinitely/ deep / structured component, something
+that cannot be turned into an actual circuit (See also <#unsupported Unsupported Haskell features>).
+Of course there are variants of recursion that cab be completely unfolded at
+compile-time with a finite amount of steps and hence could be converted to a
+realisable circuit. Sadly, this last feature is missing in the current version
+of the compiler.
+
+On the other hand, Haskell's by-default non-strict evaluation corresponds very
+well to the simulation of the feedback loops which are ubiquitous in digital
+circuits. That is, when we take our structural view to circuit descriptions,
+value-recursion corresponds directly to a feedback loop:
+
+@
+counter = s
+  where
+    s = register 0 (s + 1)
+@
+
+Over time, you will get a better feeling of what exact the consequences are of
+taking a \structural\ view on circuit descriptions. What is always important to
+remember is that every applied functions results in an instantiated component,
+and also that the compiler will never infer / invent more logic than what is
+specified in the circuit description.
+
+With that out of the way, let us continue with installing CλaSH and building
+our first circuit.
+-}
+
+{- $installation
+The CλaSH compiler and Prelude library for circuit design only work with the
+<http://haskell.org/ghc GHC> Haskell compiler version 7.8.1 and up.
+
+  (1) Install __GHC (version 7.8.1 or higher)__
+
+      * Download and install <http://www.haskell.org/ghc/download GHC for your platform>.
+        Unix user can use @./configure prefix=\<LOCATION\>@ to set the installation
+        location.
+
+      * Make sure that the @bin@ directory of __GHC__ is in your @PATH@.
+
+  (2) Install __Cabal__
+
+      * Windows:
+
+          * Download the binary for <http://www.haskell.org/cabal/download.html cabal-install>
+          * Put the binary in a location mentioned in your @PATH@
+
+      * Unix:
+
+          * Download the sources for <http://hackage.haskell.org/package/cabal-install cabal-install>
+          * Unpack (@tar xf@) the archive and @cd@ to the directory
+          * Run @sh bootstrap.sh@
+          * Follow the instructions to add @cabal@ to your @PATH@
+
+      * Run @cabal update@
+
+  (3) Install __CλaSH__
+
+      * Run @cabal install clash-ghc@
+
+  (4) Verify that everything is working by:
+
+      * Downloading the <https://raw.github.com/christiaanb/clash2/master/examples/FIR.hs Fir.hs> example
+      * Run @clash --interactive FIR.hs@
+      * Execute, in the interpreter, the @:vhdl@ command.
+      * Exit the interpreter using @:q@
+      * Examin the VHDL code in the @vhdl@ directory
+
+-}
+
+{- $working
+This tutorial can be followed best whilst having the CλaSH interpreter running
+at the same time. If you followed the installation instructions, you already
+know how to start the CλaSH compiler in interpretive mode:
+
+@
+clash --interactive
+@
+
+For those familiar with Haskell/GHC, this is indeed just @GHCi@, with one added
+command (@:vhdl@). You can load files into the interpreter using the
+@:l \<FILENAME\>@ command. Now, depending on your choice in editor, the following
+@edit-load-run@ cycle probably work best for you:
+
+  * __Commandline (e.g. emacs, vim):__
+
+      * You can run system commands using @:!@, for example @:! touch \<FILENAME\>@
+      * Set the /editor/ mode to your favourite editor using: @:set editor \<EDITOR\>@
+      * You can load files using @:l@ as noted above.
+      * You can go into /editor/ mode using: @:e@
+      * Leave the editor mode by quitting the editor (e.g. @:wq@ in @vim@)
+
+  * __GUI (e.g. SublimeText, Notepad++):__
+
+      * Just create new files in your editor.
+      * Load the files using @:l@ as noted above.
+      * Once a file has been edited and saved, type @:r@ to reload the files in
+        the interpreter
+
+You are of course free to deviate from these suggestions as you see fit :-) It
+is just recommended that you have the CλaSH interpreter open during this
+tutorial.
+-}
+
+{- $mac_example
+The very first circuit that we will build is the \"classic\" multiply-and-accumulate
+(MAC) circuit. This circuit is as simple as it sounds, it multiplies its inputs
+and accumulates them. Before we describe any logic, we must first create the
+file we will be working on and input some preliminaries:
+
+  * Create the file:
+
+      @
+      MAC.hs
+      @
+
+  * Write on the first line the module header:
+
+      @
+      module MAC where
+      @
+
+      Module names must always start with a __C__apital letter. Also make sure that
+      the file name corresponds to the module name.
+
+  * Add the import statement for the CλaSH prelude library:
+
+      @
+      import CLaSH.Prelude
+      @
+
+      This imports all the necessary functions and datatypes for circuit description.
+
+We can now finally start describing the logic of our circuit, starting with just
+the multiplication and addition:
+
+@
+ma acc (x,y) = acc + x * y
+@
+
+If you followed the instructions of running the interpreter side-by-side, you
+can already test this function:
+
+>>> ma 4 (8,9)
+76
+>>> ma 2 (3,4)
+14
+
+We can also examine the inferred type of @ma@ in the interpreter:
+
+>>> :t ma
+ma :: Num a => a -> a -> a
+
+Talking about /types/ also brings us to one of the most important parts of this
+tutorial: /types/ and /synchronous sequential logic/. Especially how we can
+always determine, through the types of a specification, if it describes
+combinational logic or (synchronous) sequential logic. We do this by examining
+the type of one of the sequential primitives, the @register@ function:
+
+@
+register :: a -> Signal a -> Signal a
+regiser i s = ...
+@
+
+Where we see that the second argument and the result are not just of the
+/polymorphic/ @a@ type, but of the type: @'Signal' a@. All (synchronous)
+sequential circuits work on values of type @'Signal' a@. Combinational
+circuits always work on values of, well, not of type @'Signal' a@. A 'Signal'
+is an (infinite) list of samples, where the samples correspond to the values
+of the 'Signal' at discrete, consecutive, ticks of the /clock/. All (sequential)
+components in the circuit are synchronized to this global /clock/. For the
+rest of this tutorial, and probably at any moment where you will be working with
+CλaSH, you should probably not actively think about 'Signal's as infinite lists
+of samples, but just as values that are manipulated by sequential circuits. To
+make this even easier, it actually not possible to manipulate the underlying
+representation directly: you can only modify 'Signal' values through a set of
+primitives such as the 'register' function above.
+
+Now, let us get back to the functionality of the 'register' function: it is
+a simple @latch@ that only changes state at the tick of the global /clock/, and
+it has an initial value @a@ which is its output at time 0. We can further
+examine the 'register' function by taking a look at the first 4 samples of the
+'register' functions applied to a constant signal with the value 8:
+
+>>> sampleN 4 (register 0 (signal 8))
+[0,8,8,8]
+
+Where we see that the initial value of the signal is the specified 0 value,
+followed by 8's.
+-}
+
+{- $mac2
+The 'register' function is our primary sequential building block to capture
+/state/. It is used internally by one of the "CLaSH.Prelude" function that we
+will use to describe our MAC circuit. Note that the following paragraphs will
+only show one of many ways to specify a sequential circuit, at the section we
+will show a couple more.
+
+A principled way to describe a sequential circuit is to use one of the classic
+machine models, within the CλaSH prelude library offer standard function to
+support the <http://en.wikipedia.org/wiki/Mealy_machine Mealy machine>.
+To improve sharing, we will combine the transition function and output function
+into one. This gives rise to the following Mealy specification of the MAC
+circuit:
+
+@
+macT acc (x,y) = (acc',o)
+  where
+    acc' = ma acc (x,y)
+    o    = acc
+@
+
+Note that the @where@ clause and explicit tuple are just for demonstrative
+purposes, without loss of sharing we could've also written:
+
+@
+macT acc inp = (ma acc inp,acc)
+@
+
+Going back to the original specification we note the following:
+
+  * 'acc' is the current /state/ of the circuit.
+  * '(x,y)' is its input.
+  * 'acc'' is the updated, or next, /state/.
+  * 'o' is the output.
+
+When we examine the type of 'macT' we see that is still completely combinational:
+
+>>> :t macT
+macT :: Num t => t -> (t, t) -> (t, t)
+
+The "CLaSH.Prelude" library contains a function that creates a sequential
+circuit from a combinational circuit that has the same Mealy machine type /
+shape of 'macT':
+
+@
+(\<^\>) :: (Pack i, Pack o)
+      => (s -> i -> (s,o))
+      -> s
+      -> (SignalP i -> SignalP o)
+f \<^\> initS = ...
+@
+
+The complete sequential MAC circuit can now be specified as:
+
+@
+mac = macT \<^\> 0
+@
+
+Where the LHS of '<^>' is our 'macT' function, and the RHS is the initial state,
+in this case 0. We can see it is functioning correctly in our interpreter:
+
+>>> take 4 $ simulateP mac [(1::Int,1),(2,2),(3,3),(4,4)] :: [Int]
+[0,1,5,14]
+
+Where we simulate our sequential circuit over a list of input samples and take
+the first 4 output samples. We have now completed our first sequential circuit
+and have made an initial confirmation that it is working as expected.
+
+The observant reader already saw that the '<^>' operator does not create a
+function that works on 'Signal's, but on on 'SignalP's. Indeed, when we look at
+the type of our 'mac' circuit:
+
+>>> :t mac
+mac :: (Pack o, Num o) => (Signal o, Signal o) -> SignalP o
+
+We see that our 'mac' function work on a two-tuple of 'Signal's and not on a
+'Signal' of a two-tuple. Indeed, the CλaSH prelude library defines that:
+
+@
+type instance SignalP (a,b) = (Signal a, Signal b)
+@
+
+'SignalP' is an <http://www.haskell.org/ghc/docs/latest/html/users_guide/type-families.html#assoc-decl associcated type family>
+belonging to the 'Pack' <http://en.wikipedia.org/wiki/Type_class type class>,
+which, together with 'pack' and 'unpack' defines the isomorphism between a
+product type of 'Signal's and a 'Signal' of a product type. That is, while
+@(Signal a, Signal b)@ and @Signal (a,b)@ are not equal, they are /isomorphic/
+and can be converted from on to the other using 'pack' and 'unpack'. Instances
+of this 'Pack' type-class are defined as /isomorphisms/ for:
+
+  * All tuples until and including 8-tuples
+  * The 'Vec'tor type
+
+But they are defined as /identities/ for:
+
+  * All elementary / primitive types such as: 'Bit', 'Bool', @'Signed' n@, etc.
+
+That is:
+
+@
+instance Pack Bool where
+  type SignalP Bool = Signal Bool
+  pack :: SignalP Bool -> Signal Bool
+  pack = 'id'
+  unpack :: Signal Bool -> SignalP Bool
+  unpack = 'id'
+@
+
+We will see later why this 'Pack' type class is so convenient, for now, you just
+have to remember that it exists. And more importantly, that you understand that
+a product type of 'Signal's is not equal to a 'Signal' of a product type, but
+that the functions of the 'Pack' type class allow easy conversion between the
+two.
+-}
+
+{- $mac3
+We are now almost at the point that we can create actual hardware, in the form
+of a <http://en.wikipedia.org/wiki/VHDL VHDL> netlist, from our sequential
+circuit specification. The first thing we have to do is create a function
+called 'topEntity' and ensure that it has a __monomorphic__ type. In our case
+that means that we have to give it an explicit type annotation. It might now
+always be needed, you can always check the type with the @:t@ command and see
+if the function is monomorphic:
+
+@
+topEntity :: (Signal (Signed 9),Signal (Signed 9)) -> Signal (Signed 9)
+topEntity = mac
+@
+
+Which makes our circuit work on 9-bit signed integers. Including the above
+definition, our complete @MAC.hs@ should now have the following content:
+
+@
+module MAC where
+
+import CLaSH.Prelude
+
+ma acc (x,y) = acc + x * y
+
+macT acc (x,y) = (acc',o)
+  where
+    acc' = ma acc (x,y)
+    o    = acc
+
+mac = macT \<^\> 0
+
+topEntity :: (Signal (Signed 9),Signal (Signed 9)) -> Signal (Signed 9)
+topEntity = mac
+@
+
+The 'topEntity' function is the starting point for the CλaSH compiler to
+transform your circuit description into a VHDL netlist. It must meet the
+following restrictions in order for the CλaSH compiler to work:
+
+  * It must be completely monomorphic
+  * It must be completely first-order
+
+Our 'topEntity' meets those restrictions, and so we can convert it successfully
+to VHDL by executing the @:vhdl@ command in the interpreter. This will create
+a directory called 'vhdl', which contains a directory called @MAC@, which
+ultimately contains all the generated VHDL files. You can now load these files
+(except @testbench.vhdl@) into your favourite VHDL synthesis tool, marking
+@topEntity_0.vhdl@ as the file containing the top level entity.
+-}
+
+{- $mac4
+There are multiple reasons as to why might you want to create a so-called
+/testbench/ for the VHDL:
+
+  * You want to compare post-synthesis / post-place&route behaviour to that of
+    the behaviour of the original VHDL.
+  * Need representative stimuli for your dynamic power calculations
+  * Verify that the VHDL output of the CλaSH compiler has the same behaviour as
+    the Haskell / CλaSH specification.
+
+For these purposes, you can have CλaSH compiler generate a @testbench.vhdl@
+file which contains a stimulus generator and an expected output verifier. The
+CλaSH compiler looks for the following functions to generate these to aspects:
+
+  1. @testInput@ for the stimulus generator.
+  2. @expectedOutput@ for the output verification.
+
+Given a 'topEntity' with the type:
+
+@
+topEntity :: SignalP a -> SignalP b
+@
+
+Where @a@ and @b@ are placeholders for monomorphics types: the 'topEntity' is
+not allowed to be polymorphic. So given the above type for the 'topEntity', the
+type of 'testInput' should be:
+
+@
+testInput :: Signal a
+@
+
+And the type of 'expectedOutput' should be:
+
+@
+expectedOutput :: Signal b -> Signal Bool
+@
+
+Where the 'expectedOutput' function should assert to 'True' once it has verified
+all expected values. The "CLaSH.Prelude" module contains two standard functions
+to serve the above purpose, but a user is free to use any CλaSH specification
+to describe these two functions. For this tutorial we will be using the
+functions specified in the "CLaSH.Prelude" module, which are 'stimuliGenerator'
+and 'outputVerifier':
+
+@
+testInput :: Signal (Signed 9,Signed 9)
+testInput = stimuliGenerator $(v [(1,1) :: (Signed 9,Signed 9),(2,2),(3,3),(4,4)])
+
+expectedOutput :: Signal (Signed 9) -> Signal Bool
+expectedOutput = outputVerifier $(v [0 :: Signed 9,1,5,14])
+@
+
+This will create a stimulus generator that creates the same inputs as we used
+earlier for the simulation of the circuit, and creates an output verifier that
+compares against the results we got from our earlier simulation. We can even
+simulate the behaviour of the /testbench/:
+
+>>> sampleN 7 $ expectedOutput (topEntity $ unpack testInput)
+[False,False,False,False,
+expected value: 14, not equal to actual value: 30
+True,
+expected value: 14, not equal to actual value: 46
+True,
+expected value: 14, not equal to actual value: 62
+True]
+
+We can see that for the first 4 samples, everything is working as expected,
+after which warnings are being reported. The reason is that 'stimuliGenerator'
+will keep on producing the last sample, (4,4), while the 'outputVerifier' will
+keep on expecting the last sample, 14. In the VHDL testbench these errors won't
+show, as the the global clock will be stopped after 4 ticks.
+
+You should now again run @:vhdl@ in the interpreter; this time the compiler
+will take a bit longer to generate all the circuits. After it is finished you
+can load all the files in your favourite VHDL simulation tool that has support
+for VHDL-2008. VHDL-2008 support is required because the output verifier will
+use the VHDL-2008-only @to_string@ function. Once all files are loaded into
+the VHDL simulator, run the simulation on the @testbench@ entity. On questasim /
+modelsim: doing a @run -all@ will finish once the output verifier will assert
+its output to @true@. The generated testbench, modulo the clock signal
+generator(s), is completely synthesizable. This means that if you want to test
+your circuit on an FPGA, you will only have to replace the clock signal
+generator(s) by actual clock sources, such as an onboard PLL.
+
+This concludes the main part of this section on \"Your first circuit\", read on
+for alternative specifications for the same 'mac' circuit, or just skip to the
+next section where we will describe another DSP classic: an FIR filter structure.
+-}
+
+{- $mac5
+* __'Num' instance__:
+
+    @'Signal' a@ is also also considered a 'Num'eric type as long as @a@ is also.
+    This means that we can also use the standard numeric operators, such as ('*')
+    and ('+'), directly on signals. An alternative specification of the 'mac'
+    circuit will also use the 'register' function directly:
+
+    @
+    macN (x,y) = acc
+      where
+        acc = register 0 (acc + x * y)
+    @
+
+* __'Applicative' interface__:
+
+    We can also mix the combinational 'ma' function, with the sequential
+    'register' function, by lifting the 'ma' function to the sequential 'Signal'
+    domain using the operators of the 'Applicative' type class:
+
+    @
+    macA (x,y) = acc
+      where
+        acc  = register 0 acc'
+        acc' = ma \<$\> acc \<*\> pack (x,y)
+    @
+
+* __<http://hackage.haskell.org/package/mtl/docs/Control-Monad-State-Lazy.html#t:State State> Monad__
+
+    We can also implement the original 'macT' function as a <http://hackage.haskell.org/package/mtl/docs/Control-Monad-State-Lazy.html#t:State State>
+    monadic computation. First we must an extra import statement, right after
+    the import of "CLaSH.Prelude":
+
+    @
+    import Control.Monad.State
+    @
+
+    We can then implement macT as follows:
+
+    @
+    macTS (x,y) = do
+      acc <- get
+      put (acc + x * y)
+      return acc
+    @
+
+    We can use the '<^>' operator again, although we will have to change
+    position of the arguments and result:
+
+    @
+    asStateM f i = g \<^\> i
+      where
+        g s x = let (o,s') = runState (f x) s
+                in  (s',o)
+    @
+
+    We can then create the complete 'mac' circuit as:
+
+    @
+    macS = asStateM macTS 0
+    @
+-}
+
+{- $higher_order
+An FIR filter is defined as: the dot-product of a set of filter coefficients and
+a window over the input, where the size of the window matches the number
+of coefficients.
+
+@
+dotp as bs = vfoldl (+) 0 (vzipWith (*) as bs)
+
+fir coeffs x_t = y_t
+  where
+    y_t = dotp coeffs xs
+    xs  = window x_t
+
+topEntity :: Signal (Signed 16) -> Signal (Signed 16)
+topEntity = fir $(v [0::Signal (Signed 16),1,2,3])
+@
+
+Here we can see that, although the CλaSH compiler does not support recursion,
+many of the regular patterns that we often encounter in circuit design are
+already captured by the higher-order functions that are present for the 'Vec'tor
+type.
+-}
+
+{- $composition_sequential
+
+First we define some types:
+
+@
+module CalculatorTypes where
+
+import CLaSH.Prelude
+
+type Word = Signed 4
+data OPC a = ADD | MUL | Imm a | Pop | Push
+
+deriveLift ''OPC
+@
+
+Now we define the actual calculator:
+
+@
+module Calculator where
+
+import CLaSH.Prelude
+import CalculatorTypes
+
+(.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d
+(f .: g) a b = f (g a b)
+
+infixr 9 .:
+
+alu :: Num a => OPC a -> a -> a -> Maybe a
+alu ADD     = Just .: (+)
+alu MUL     = Just .: (*)
+alu (Imm i) = const . const (Just i)
+alu _       = const . const Nothing
+
+pu :: (Num a, Num b)
+   => (OPC a -> a -> a -> Maybe a)
+   -> (a, a, b)       -- Current state
+   -> (a, OPC a)      -- Input
+   -> ( (a, a, b)     -- New state
+      , (b, Maybe a)  -- Output
+      )
+pu alu (op1,op2,cnt) (dmem,Pop)  = ((dmem,op1,cnt-1),(cnt,Nothing))
+pu alu (op1,op2,cnt) (dmem,Push) = ((op1,op2,cnt+1) ,(cnt,Nothing))
+pu alu (op1,op2,cnt) (dmem,opc)  = ((op1,op2,cnt)   ,(cnt,alu opc op1 op2))
+
+datamem :: (KnownNat n, Integral i)
+        => Vec n a       -- Current state
+        -> (i, Maybe a)  -- Input
+        -> (Vec n a, a)  -- (New state, Output)
+datamem mem (addr,Nothing)  = (mem                  ,mem ! addr)
+datamem mem (addr,Just val) = (vreplace mem addr val,mem ! addr)
+
+topEntity :: Signal (OPC Word) -> Signal (Maybe Word)
+topEntity i = val
+  where
+    (addr,val) = (pu alu \<^\> (0,0,0 :: Unsigned 3)) (mem,i)
+    mem        = (datamem \<^\> initMem) (addr,val)
+    initMem    = vcopy d8 0
+@
+
+Here we can finally see the advantage of having the '<^>' return a function
+of type @'SignalP' i -> 'SignalP' o@:
+
+  * We can use normal pattern matching to get parts of the result, and,
+  * We can use normal tuple-constructors to build the input values for the
+    circuits.
+-}
+
+{- $conclusion
+For now, this is the end of this tutorial. We will be adding updates over time,
+so check back from time to time. For now we recommend that you continue with
+exploring the "CLaSH.Prelude" module however, and like that hopefully get a feel
+of what CλaSH is capable of.
+-}
+
+{- $errorsandsolutions
+A list often encountered errors and their solutions:
+
+* __Type error: Couldn't match expected type ‘Signal (a,b)’ with actual type__
+  __‘(Signal a, Signal b)’__:
+
+    Signals of product types and product types (to which tuples belong) of
+    signals are __isomorphic__ due to synchronisity principle, but are not
+    (structurally) equal. Use the 'pack' function to convert from a product type
+    to the signal type. So if your code which gives the error looks like:
+
+    @
+    ... = f a b (c,d)
+    @
+
+    add the 'pack' function like so:
+
+    @
+    ... = f a b (pack (c,d))
+    @
+
+    Product types supported by 'pack' are:
+
+    * All tuples until and including 8-tuples
+    * The 'Vec'tor type
+
+    NB: Use 'cpack' when you are using explicitly clocked 'CSignal's
+
+* __Type error: Couldn't match expected type ‘(Signal a, Signal b)’ with__
+  __ actual type ‘Signal (a,b)’__:
+
+    Product types (to which tuples belong) of signals and signals of product
+    types are __isomorphic__ due to synchronisity principle, but are not
+    (structurally) equal. Use the 'unpack' function to convert from a signal
+    type to the product type. So if your code which gives the error looks like:
+
+    @
+    (c,d) = f a b
+    @
+
+    add the 'unpack' function like so:
+
+    @
+    (c,d) = unpack (f a b)
+    @
+
+    Product types supported by 'unpack' are:
+
+    * All tuples until and including 8-tuples
+    * The 'Vec'tor type
+
+    NB: Use 'cunpack' when you are using explicitly clocked 'CSignal's
+
+* __CLaSH.Normalize(94): Expr belonging to bndr: \<FUNCTION\> remains__
+  __recursive after normalization__:
+
+    * If you actually wrote a recursive function, rewrite it to a non-recursive
+      one :-)
+
+    * You defined a recursively defined value, but left it polymorphic:
+
+    @
+    topEntity x y = acc
+    where
+      acc = register 3 (x*y + acc)
+    @
+
+    The above function, works for any number-like type. This means that @acc@ is
+    a recursively defined __polymorphic__ value. Adding a monomorphic type
+    annotation makes the error go away.
+
+    @
+    topEntity :: Signal (Signed 8) -> Signal (Signed 8) -> Signal (Signed 8)
+    topEntity x y = acc
+    where
+      acc = register 3 (x*y + acc)
+    @
+
+* __CLaSH.Normalize.Transformations(155): InlineNonRep: \<FUNCTION\> already__
+  __inlined 100 times in:\<FUNCTION\>, \<TYPE\>__:
+
+    You left the @topEntity@ function polymorphic or higher-order: use
+    @:t topEntity@ to check if the type is indeed polymorphic or higher-order.
+    If it is, add a monomorphic type signature, and / or supply higher-order
+    arguments.
+
+* __Can't make testbench for: \<LONG_VERBATIM_COMPONENT_DESCRIPTION\>__:
+
+    * Don't worry, it's actually only a warning.
+
+    * The @topEntity@ function does __not__ have exactly 1 argument. If your
+      @topEntity@ has no arguments, you're out of luck for now. If it has
+      multiple arguments, consider bundling them in a tuple.
+
+*  __\<*** Exception: \<\<loop\>\>__
+
+    You are using value-recursion, but one of the 'Vec'tor functions that you
+    are using is too /strict/ in one of the recursive arguments. For example:
+
+    @
+    -- Bubble sort for 1 iteration
+    sortV xs = vmap fst sorted <: (snd (vlast sorted))
+     where
+       lefts  = vhead xs :> vmap snd (vinit sorted)
+       rights = vtail xs
+       sorted = vzipWith compareSwapL lefts rights
+
+    -- Compare and swap
+    compareSwapL a b = if a < b then (a,b)
+                                else (b,a)
+    @
+
+    Will not terminate because 'vzipWith' is too strict in its left argument:
+
+    >>> sortV (4 :> 1 :> 2 :> 3 :> Nil)
+    <*** Exception: <<loop>>
+
+    In this case, adding 'lazyV' on 'vzipWith's left argument:
+
+    @
+    sortVL xs = vmap fst sorted <: (snd (vlast sorted))
+     where
+       lefts  = vhead xs :> vmap snd (vinit sorted)
+       rights = vtail xs
+       sorted = vzipWith compareSwapL (lazyV lefts) rights
+    @
+
+    Results in a successful computation:
+
+    >>> sortVL (4 :> 1 :> 2 :> 3 :> Nil)
+    <1,2,3,4>
+-}
+
+{- $unsupported #unsupported#
+Here is a list of Haskell features which the CλaSH compiler cannot synthesize
+to VHDL (for now):
+
+  [@Recursive functions@]
+
+    Although it seems rather bad that a compiler for a
+    functional language does not support recursion, this bug/feature of the
+    CλaSH compiler is amortized by the builtin knowledge of all the functions
+    listed in "CLaSH.Sized.Vector". And as you saw in this tutorial, the
+    higher-order functions of "CLaSH.Sized.Vector" can cope with many of the
+    recursive design patterns found in circuit design.
+
+    Also note that although recursive functions are not supported, recursively
+    (tying-the-knot) defined values are supported (as long as these values do
+    not have a function type). An example that uses recursively defined values
+    is the following function that performs one iteration of bubble sort:
+
+    @
+    sortVL xs = vmap fst sorted <: (snd (vlast sorted))
+     where
+       lefts  = vhead xs :> vmap snd (vinit sorted)
+       rights = vtail xs
+       sorted = vzipWith compareSwapL (lazyV lefts) rights
+    @
+
+    Where we can clearly see that 'lefts' and 'sorted' are defined in terms of
+    each other.
+
+  [@Recursive datatypes@]
+
+    The CλaSH compiler needs to be able to determine a bit-size for any value
+    that will be represented in the eventual circuit. More specifically, we need
+    to know the maximum number of bits needed to represent a value. While this
+    is trivial for values of the elementary types, sum types, and product types,
+    putting a fixed upper bound on recursive types is not (always) feasible.
+    This means that the ubiquitous list type is unsupported! The only recursive
+    type that is currently supported by the CλaSH compiler is the 'Vec'tor type,
+    for which the compiler has hard-coded knowledge.
+
+    For \"easy\" 'Vec'tor literals you should use Template Haskell splices and
+    the 'v' /meta/-function that as we have seen earlier in this tutorial.
+
+  [@GADT pattern matching@]
+
+    While pattern matching for regular ADTs is supported, pattern matching for
+    GADTs is __not__. The 'Vec'tor type, which is also a GADT, is __no__
+    exception! You can use the extraction and indexing functions of
+    "CLaSH.Sized.Vector" to get access to individual ranges / elements of a
+    'Vec'tor.
+
+  [@Floating point types@]
+
+    There is no support for the 'Float' and 'Double' type, if you need numbers
+    with a /fractional/ part you can use the 'Fixed' point type.
+-}