diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c)2013, University of Twente
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of University of Twente nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,2 @@
+= WARNING =
+Only works with latest version of GHC-HEAD (https://github.com/ghc/ghc)!
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/clash-prelude.cabal b/clash-prelude.cabal
new file mode 100644
--- /dev/null
+++ b/clash-prelude.cabal
@@ -0,0 +1,43 @@
+Name:                 clash-prelude
+Version:              0.2
+Synopsis:             CAES Language for Synchronous Hardware
+-- Description:
+Homepage:             http://clash.ewi.utwente.nl/
+bug-reports:          http://github.com/christiaanb/clash-prelude/issues
+License:              BSD3
+License-file:         LICENSE
+Author:               Christiaan Baaij
+Maintainer:           Christiaan Baaij <christiaan.baaij@gmail.com>
+Copyright:            Copyright (C) 2013-2014 University of Twente
+Category:             Hardware
+Build-type:           Simple
+
+Extra-source-files:   README.md
+
+Cabal-version:        >=1.10
+
+source-repository head
+  type: git
+  location: git://github.com/christiaanb/clash-prelude.git
+
+Library
+  HS-Source-Dirs:     src
+
+  default-language:   Haskell2010
+  ghc-options:        -Wall -fwarn-tabs
+
+  Exposed-modules:    CLaSH.Bit
+                      CLaSH.Class.BitVector
+                      CLaSH.Prelude
+                      CLaSH.Promoted.Bool
+                      CLaSH.Promoted.Nat
+                      CLaSH.Promoted.Ord
+                      CLaSH.Signal
+                      CLaSH.Sized.Signed
+                      CLaSH.Sized.Unsigned
+                      CLaSH.Sized.Vector
+
+  Build-depends:      base                 >= 4.7.0.0 && < 5,
+                      data-default         >= 0.5.3,
+                      template-haskell     >= 2.9.0.0,
+                      th-lift              >= 0.5.6
diff --git a/src/CLaSH/Bit.hs b/src/CLaSH/Bit.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Bit.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -fno-warn-missing-methods #-}
+
+module CLaSH.Bit
+  (Bit(..))
+where
+
+import Data.Bits
+import Data.Default
+import Language.Haskell.TH.Lift
+
+data Bit = H | L
+
+instance Eq Bit where
+  (==) = eqBit
+
+{-# NOINLINE eqBit #-}
+eqBit :: Bit -> Bit -> Bool
+eqBit L L = True
+eqBit H H = True
+eqBit _ _ = False
+
+instance Show Bit where
+  show H = "1"
+  show L = "0"
+
+instance Default Bit where
+  def = L
+
+deriveLift ''Bit
+
+{-# NOINLINE bAnd #-}
+bAnd :: Bit -> Bit -> Bit
+bAnd H H = H
+bAnd _ _ = L
+
+{-# NOINLINE bOr #-}
+bOr :: Bit -> Bit -> Bit
+bOr L L  = L
+bOr _ _  = H
+
+{-# NOINLINE bXor #-}
+bXor :: Bit -> Bit -> Bit
+bXor L L = L
+bXor H H = L
+bXor _ _ = H
+
+{-# NOINLINE bNot #-}
+bNot :: Bit -> Bit
+bNot L = H
+bNot H = L
+
+instance Bits Bit where
+  (.&.)        = bAnd
+  (.|.)        = bOr
+  xor          = bXor
+  complement   = bNot
+  bit          = const H
+  testBit H _  = True
+  testBit _ _  = False
+  bitSizeMaybe = const (Just 1)
+  isSigned     = const False
+  popCount H   = 1
+  popCount _   = 0
diff --git a/src/CLaSH/Class/BitVector.hs b/src/CLaSH/Class/BitVector.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Class/BitVector.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies     #-}
+module CLaSH.Class.BitVector where
+
+import CLaSH.Bit
+import CLaSH.Sized.Vector
+import GHC.TypeLits
+
+class BitVector a where
+  type BitSize a :: Nat
+  toBV   :: KnownNat (BitSize a) => a -> Vec (BitSize a) Bit
+  fromBV :: KnownNat (BitSize a) => Vec (BitSize a) Bit -> a
diff --git a/src/CLaSH/Prelude.hs b/src/CLaSH/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Prelude.hs
@@ -0,0 +1,123 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE TypeOperators       #-}
+
+{-# OPTIONS_GHC -O0 -fno-omit-interface-pragmas #-}
+
+module CLaSH.Prelude
+  ( module Exported
+  , module CLaSH.Prelude
+  )
+where
+
+import Control.Arrow         as Exported
+import Control.Applicative   as Exported
+import Control.Category      as Category
+import Data.Bits             as Exported
+import Data.Default          as Exported
+import CLaSH.Class.BitVector as Exported
+import CLaSH.Promoted.Bool   as Exported
+import CLaSH.Promoted.Nat    as Exported
+import CLaSH.Promoted.Ord    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
+
+{-# INLINABLE window #-}
+window :: (KnownNat (n + 1), Default a)
+       => Signal a
+       -> Vec ((n + 1) + 1) (Signal a)
+window x = x :> prev
+  where
+    prev = registerP (vcopyI def) next
+    next = x +>> prev
+
+{-# INLINABLE windowP #-}
+windowP :: (KnownNat (n + 1), Default a)
+        => Signal a
+        -> Vec (n + 1) (Signal a)
+windowP x = prev
+  where
+    prev = registerP (vcopyI def) next
+    next = x +>> prev
+
+{-# INLINABLE (<^>) #-}
+(<^>) :: (Pack i, Pack o)
+      => (s -> i -> (s,o))
+      -> s
+      -> (SignalP i -> SignalP o)
+f <^> iS = \i -> let (s',o) = unpack $ f <$> s <*> (pack i)
+                     s      = register iS s'
+                 in unpack o
+
+{-# INLINABLE registerP #-}
+registerP :: Pack a => a -> SignalP a -> SignalP a
+registerP i = unpack Prelude.. register i Prelude.. pack
+
+{-# NOINLINE blockRam #-}
+blockRam :: forall n m a . (KnownNat n, KnownNat m, Pack a)
+         => SNat n
+         -> Signal (Unsigned m)
+         -> Signal (Unsigned m)
+         -> Signal Bool
+         -> Signal a
+         -> Signal a
+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")
+
+    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
+
+{-# INLINABLE blockRamPow2 #-}
+blockRamPow2 :: (KnownNat n, KnownNat (n^2), Pack a)
+             => (SNat ((n^2) :: Nat))
+             -> Signal (Unsigned n)
+             -> Signal (Unsigned n)
+             -> Signal Bool
+             -> Signal a
+             -> Signal a
+blockRamPow2 = blockRam
+
+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
+
+instance ArrowLoop Comp where
+  loop (C f) = C $ simpleLoop (unpack Prelude.. f Prelude.. pack)
+    where
+      simpleLoop g b = let ~(c,d) = g (b,d)
+                       in c
+
+registerC :: a -> Comp a a
+registerC = C Prelude.. register
+
+simulateC :: Comp a b -> [a] -> [b]
+simulateC f = simulate (asFunction f)
+
+{-# INLINABLE (^^^) #-}
+(^^^) :: (s -> i -> (s,o)) -> s -> Comp i o
+f ^^^ sI = C $ \i -> let (s',o) = unpack $ f <$> s <*> i
+                         s      = register sI s'
+                     in  o
diff --git a/src/CLaSH/Promoted/Bool.hs b/src/CLaSH/Promoted/Bool.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Promoted/Bool.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeFamilies   #-}
+{-# LANGUAGE PolyKinds      #-}
+module CLaSH.Promoted.Bool where
+
+type family If (x :: Bool) (y :: k) (z :: k) :: k
+
+type instance If True  y z = y
+type instance If False y z = z
diff --git a/src/CLaSH/Promoted/Nat.hs b/src/CLaSH/Promoted/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Promoted/Nat.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
+module CLaSH.Promoted.Nat
+  ( SNat, snat, withSNat, fromSNat
+  , UNat (..), toUNat, addUNat, multUNat, powUNat
+  )
+where
+
+import Data.Proxy
+import GHC.TypeLits
+import Unsafe.Coerce
+
+data SNat (n :: Nat) = KnownNat n => SNat (Proxy n)
+
+snat :: KnownNat n => SNat n
+snat = SNat Proxy
+
+withSNat :: KnownNat n => (SNat n -> a) -> a
+withSNat f = f (SNat Proxy)
+
+data UNat :: Nat -> * where
+  UZero :: UNat 0
+  USucc :: UNat n -> UNat (n + 1)
+
+fromSNat :: SNat n -> Integer
+fromSNat (SNat p) = natVal p
+
+{-# NOINLINE fromSNat #-}
+toUNat :: SNat n -> UNat n
+toUNat (SNat p) = fromI (natVal p)
+  where
+    fromI :: Integer -> UNat m
+    fromI 0 = unsafeCoerce UZero
+    fromI n = unsafeCoerce (USucc (fromI (n - 1)))
+
+addUNat :: UNat n -> UNat m -> UNat (n + m)
+addUNat UZero     y     = y
+addUNat x         UZero = x
+addUNat (USucc x) y     = unsafeCoerce (USucc (addUNat x y))
+
+multUNat :: UNat n -> UNat m -> UNat (n * m)
+multUNat UZero      _     = UZero
+multUNat _          UZero = UZero
+multUNat (USucc x) y      = unsafeCoerce (addUNat y (multUNat x y))
+
+powUNat :: UNat n -> UNat m -> UNat (n ^ m)
+powUNat _ UZero     = USucc UZero
+powUNat x (USucc y) = unsafeCoerce (multUNat x (powUNat x y))
diff --git a/src/CLaSH/Promoted/Ord.hs b/src/CLaSH/Promoted/Ord.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Promoted/Ord.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+module CLaSH.Promoted.Ord where
+
+import GHC.TypeLits
+
+import CLaSH.Promoted.Bool
+
+type family Min (x :: Nat) (y :: Nat) :: Nat
+type instance Min x y = If (x <=? y) x y
+
+type family Max (x :: Nat) (y :: Nat) :: Nat
+type instance Max x y = If (x <=? y) y x
diff --git a/src/CLaSH/Signal.hs b/src/CLaSH/Signal.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Signal.hs
@@ -0,0 +1,227 @@
+{-# LANGUAGE LambdaCase      #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies    #-}
+
+module CLaSH.Signal
+  ( Signal
+  , fromList
+  , signal
+  , sample
+  , 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 :-
+data Signal a = a :- Signal a
+
+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
+
+sample :: Int -> Signal a -> [a]
+sample 0 _         = []
+sample n ~(x :- xs) = x : (sample (n-1) xs)
+
+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 :: a -> Signal a -> Signal a
+register i s = i :- s
+
+simulate :: (Signal a -> Signal b) -> [a] -> [b]
+simulate f as = sample (length as) (f (fromList as))
+
+class Pack a where
+  type SignalP a
+  pack   :: SignalP a -> Signal a
+  unpack :: Signal a -> SignalP a
+
+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))
+
+(<^) :: Applicative f => f a -> (a -> b -> c) -> f b -> f c
+v <^ f = liftA2 f v
+
+(^>) :: 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/Sized/Signed.hs b/src/CLaSH/Sized/Signed.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Sized/Signed.hs
@@ -0,0 +1,269 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeOperators       #-}
+
+{-# OPTIONS_GHC -fno-warn-missing-methods #-}
+
+module CLaSH.Sized.Signed
+  ( Signed
+  , resizeS
+  , resizeS_wrap
+  )
+where
+
+import Data.Bits
+import Data.Default
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax(Lift(..))
+import GHC.TypeLits
+
+import CLaSH.Bit
+import CLaSH.Class.BitVector
+import CLaSH.Promoted.Nat
+import CLaSH.Sized.Vector
+
+newtype Signed (n :: Nat) = S Integer
+
+instance Eq (Signed n) where
+  (==) = eqS
+
+{-# NOINLINE eqS #-}
+eqS :: (Signed n) -> (Signed n) -> Bool
+(S n) `eqS` (S m) = n == m
+
+instance Ord (Signed n) where
+  (<)  = ltS
+  (>=) = geS
+  (>)  = gtS
+  (<=) = leS
+
+ltS,geS,gtS,leS :: Signed n -> Signed n -> Bool
+{-# NOINLINE ltS #-}
+ltS (S n) (S m) = n < m
+{-# NOINLINE geS #-}
+geS (S n) (S m) = n >= m
+{-# NOINLINE gtS #-}
+gtS (S n) (S m) = n > m
+{-# NOINLINE leS #-}
+leS (S n) (S m) = n <= m
+
+instance KnownNat n => Enum (Signed n) where
+  succ           = plusS (fromIntegerS 1)
+  pred           = minS (fromIntegerS 1)
+  toEnum         = fromIntegerS . toInteger
+  fromEnum       = fromEnum . toIntegerS
+
+instance KnownNat n => Bounded (Signed n) where
+  minBound = minBoundS
+  maxBound = maxBoundS
+
+minBoundS,maxBoundS :: forall n . KnownNat n => Signed n
+{-# NOINLINE minBoundS #-}
+minBoundS = S $ negate $ 2 ^ (fromSNat (snat :: SNat n) -1)
+{-# NOINLINE maxBoundS #-}
+maxBoundS = S $ 2 ^ (fromSNat (snat :: SNat n) - 1) - 1
+
+instance KnownNat n => Num (Signed n) where
+  (+)         = plusS
+  (-)         = minS
+  (*)         = timesS
+  negate      = negateS
+  abs         = absS
+  signum      = signumS
+  fromInteger = fromIntegerS
+
+plusS,minS,timesS :: KnownNat n => Signed n -> Signed n -> Signed n
+{-# NOINLINE plusS #-}
+plusS (S a) (S b) = fromIntegerS_inlineable $ a + b
+
+{-# NOINLINE minS #-}
+minS (S a) (S b) = fromIntegerS_inlineable $ a - b
+
+{-# NOINLINE timesS #-}
+timesS (S a) (S b) = fromIntegerS_inlineable $ a * b
+
+negateS,absS,signumS :: KnownNat n => Signed n -> Signed n
+{-# NOINLINE negateS #-}
+negateS (S n) = fromIntegerS_inlineable (0 - n)
+
+{-# NOINLINE absS #-}
+absS (S n) = fromIntegerS_inlineable (abs n)
+
+{-# NOINLINE signumS #-}
+signumS (S n) = fromIntegerS_inlineable (signum n)
+
+fromIntegerS,fromIntegerS_inlineable :: forall n . KnownNat n => Integer -> Signed (n :: Nat)
+{-# NOINLINE fromIntegerS #-}
+fromIntegerS = fromIntegerS_inlineable
+{-# INLINABLE fromIntegerS_inlineable #-}
+fromIntegerS_inlineable i
+    | nS == 0   = S 0
+    | otherwise = res
+  where
+    nS  = fromSNat (snat :: SNat n)
+    sz  = 2 ^ (nS - 1)
+    res = case divMod i sz of
+            (s,i') | even s    -> S i'
+                   | otherwise -> S (i' - sz)
+
+instance KnownNat n => Real (Signed n) where
+  toRational = toRational . toIntegerS
+
+instance KnownNat n => Integral (Signed n) where
+  quot      = quotS
+  rem       = remS
+  div       = divS
+  mod       = modS
+  quotRem   = quotRemS
+  divMod    = divModS
+  toInteger = toIntegerS
+
+quotS,remS,divS,modS :: KnownNat n => Signed n -> Signed n -> Signed n
+{-# NOINLINE quotS #-}
+quotS = (fst.) . quotRemS_inlineable
+{-# NOINLINE remS #-}
+remS = (snd.) . quotRemS_inlineable
+{-# NOINLINE divS #-}
+divS = (fst.) . divModS_inlineable
+{-# NOINLINE modS #-}
+modS = (snd.) . divModS_inlineable
+
+quotRemS,divModS :: KnownNat n => Signed n -> Signed n -> (Signed n, Signed n)
+quotRemS n d = (n `quotS` d,n `remS` d)
+divModS n d  = (n `divS` d,n `modS` d)
+
+quotRemS_inlineable,divModS_inlineable :: KnownNat n => Signed n -> Signed n -> (Signed n, Signed n)
+{-# INLINEABLE quotRemS_inlineable #-}
+(S a) `quotRemS_inlineable` (S b) = let (a',b') = a `quotRem` b
+                                    in (fromIntegerS_inlineable a', fromIntegerS_inlineable b')
+{-# INLINEABLE divModS_inlineable #-}
+(S a) `divModS_inlineable` (S b) = let (a',b') = a `divMod` b
+                                   in (fromIntegerS_inlineable a', fromIntegerS_inlineable b')
+
+{-# NOINLINE toIntegerS #-}
+toIntegerS :: Signed n -> Integer
+toIntegerS (S n) = n
+
+instance KnownNat n => Bits (Signed n) where
+  (.&.)          = andS
+  (.|.)          = orS
+  xor            = xorS
+  complement     = complementS
+  bit            = bitS
+  testBit        = testBitS
+  bitSizeMaybe   = Just . finiteBitSizeS
+  isSigned       = const True
+  shiftL         = shiftLS
+  shiftR         = shiftRS
+  rotateL        = rotateLS
+  rotateR        = rotateRS
+  popCount       = popCountS
+
+andS,orS,xorS :: KnownNat n => Signed n -> Signed n -> Signed n
+{-# NOINLINE andS #-}
+(S a) `andS` (S b) = fromIntegerS_inlineable (a .&. b)
+{-# NOINLINE orS #-}
+(S a) `orS` (S b)  = fromIntegerS_inlineable (a .|. b)
+{-# NOINLINE xorS #-}
+(S a) `xorS` (S b) = fromIntegerS_inlineable (xor a b)
+
+{-# NOINLINE complementS #-}
+complementS :: KnownNat n => Signed n -> Signed n
+complementS = fromBitVector . vmap complement . toBitVector
+
+{-# NOINLINE bitS #-}
+bitS :: KnownNat n => Int -> Signed n
+bitS = fromIntegerS_inlineable . bit
+
+{-# NOINLINE testBitS #-}
+testBitS :: Signed n -> Int -> Bool
+testBitS (S n) i = testBit n i
+
+shiftLS,shiftRS,rotateLS,rotateRS :: KnownNat n => Signed n -> Int -> Signed n
+{-# NOINLINE shiftLS #-}
+shiftLS _ b | b < 0  = error "'shiftL'{Signed} undefined for negative numbers"
+shiftLS (S n) b      = fromIntegerS_inlineable (shiftL n b)
+{-# NOINLINE shiftRS #-}
+shiftRS _ b | b < 0  = error "'shiftR'{Signed} undefined for negative numbers"
+shiftRS (S n) b      = fromIntegerS_inlineable (shiftR n b)
+{-# NOINLINE rotateLS #-}
+rotateLS _ b | b < 0 = error "'shiftL'{Signed} undefined for negative numbers"
+rotateLS n b         = let b' = b `mod` finiteBitSizeS n
+                       in shiftL n b' .|. shiftR n (finiteBitSizeS n - b')
+{-# NOINLINE rotateRS #-}
+rotateRS _ b | b < 0 = error "'shiftR'{Signed} undefined for negative numbers"
+rotateRS n b         = let b' = b `mod` finiteBitSizeS n
+                       in shiftR n b' .|. shiftL n (finiteBitSizeS n - b')
+
+{-# NOINLINE popCountS #-}
+popCountS :: Signed n -> Int
+popCountS (S n) = popCount n
+
+instance KnownNat n => FiniteBits (Signed n) where
+  finiteBitSize = finiteBitSizeS
+
+{-# NOINLINE finiteBitSizeS #-}
+finiteBitSizeS :: forall n . KnownNat n => Signed n -> Int
+finiteBitSizeS _ = fromInteger $ fromSNat (snat :: SNat n)
+
+instance Show (Signed n) where
+  show (S n) = show n
+
+instance KnownNat n => Default (Signed n) where
+  def = fromIntegerS 0
+
+instance KnownNat n => Lift (Signed n) where
+  lift (S i) = sigE [| fromIntegerS i |] (decSigned $ fromSNat (snat :: (SNat n)))
+
+decSigned :: Integer -> TypeQ
+decSigned n = appT (conT ''Signed) (litT $ numTyLit n)
+
+instance BitVector (Signed n) where
+  type BitSize (Signed n) = n
+  toBV   = toBitVector
+  fromBV = fromBitVector
+
+{-# NOINLINE toBitVector #-}
+toBitVector :: KnownNat n => Signed n -> Vec n Bit
+toBitVector (S m) = vreverse $ vmap (\x -> if odd x then H else L) $ viterateI (`div` 2) m
+
+{-# NOINLINE fromBitVector #-}
+fromBitVector :: KnownNat n => Vec n Bit -> Signed n
+fromBitVector = fromBitList . reverse . toList
+
+{-# INLINABLE fromBitList #-}
+fromBitList :: KnownNat n => [Bit] -> Signed n
+fromBitList l = fromIntegerS_inlineable
+              $ sum [ n
+                    | (n,b) <- zip (iterate (*2) 1) l
+                    , b == H
+                    ]
+
+{-# 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 :: forall n m . (KnownNat n, KnownNat m) => Signed n -> Signed m
+resizeS s@(S n) | n' <= m'  = fromIntegerS_inlineable n
+                | otherwise = case l of
+                    (x:xs) -> fromBitList $ reverse $ x : (drop (n' - m') xs)
+                    _      -> error "resizeS impossible case: empty list"
+  where
+    n' = fromInteger $ fromSNat (snat :: SNat n) :: Int
+    m' = fromInteger $ fromSNat (snat :: SNat m) :: Int
+    l  = toList $ toBitVector s
+
+{-# NOINLINE resizeS_wrap #-}
+-- | A resize operation that is sign-preserving on extension, but wraps on truncation.
+--
+-- 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@(S n) = fromIntegerS_inlineable n
diff --git a/src/CLaSH/Sized/Unsigned.hs b/src/CLaSH/Sized/Unsigned.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Sized/Unsigned.hs
@@ -0,0 +1,227 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeOperators       #-}
+
+{-# OPTIONS_GHC -fno-warn-missing-methods #-}
+
+module CLaSH.Sized.Unsigned
+  ( Unsigned
+  , resizeU
+  )
+where
+
+import Data.Bits
+import Data.Default
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax(Lift(..))
+import GHC.TypeLits
+
+import CLaSH.Bit
+import CLaSH.Class.BitVector
+import CLaSH.Promoted.Nat
+import CLaSH.Sized.Vector
+
+newtype Unsigned (n :: Nat) = U Integer
+
+instance Eq (Unsigned n) where
+  (==) = eqU
+
+{-# NOINLINE eqU #-}
+eqU :: (Unsigned n) -> (Unsigned n) -> Bool
+(U n) `eqU` (U m) = n == m
+
+instance Ord (Unsigned n) where
+  (<)  = ltU
+  (>=) = geU
+  (>)  = gtU
+  (<=) = leU
+
+ltU,geU,gtU,leU :: Unsigned n -> Unsigned n -> Bool
+{-# NOINLINE ltU #-}
+ltU (U n) (U m) = n < m
+{-# NOINLINE geU #-}
+geU (U n) (U m) = n >= m
+{-# NOINLINE gtU #-}
+gtU (U n) (U m) = n > m
+{-# NOINLINE leU #-}
+leU (U n) (U m) = n <= m
+
+instance KnownNat n => Enum (Unsigned n) where
+  succ           = plusU (fromIntegerU 1)
+  pred           = minU (fromIntegerU 1)
+  toEnum         = fromIntegerU . toInteger
+  fromEnum       = fromEnum . toIntegerU
+
+instance KnownNat n => Bounded (Unsigned n) where
+  minBound = fromIntegerU 0
+  maxBound = maxBoundU
+
+{-# NOINLINE maxBoundU #-}
+maxBoundU :: forall n . KnownNat n => Unsigned n
+maxBoundU = U $ (2 ^ fromSNat (snat :: SNat n)) - 1
+
+instance KnownNat n => Num (Unsigned n) where
+  (+)         = plusU
+  (-)         = minU
+  (*)         = timesU
+  negate      = id
+  abs         = id
+  signum      = signumU
+  fromInteger = fromIntegerU
+
+plusU,minU,timesU :: KnownNat n => Unsigned n -> Unsigned n -> Unsigned n
+{-# NOINLINE plusU #-}
+plusU (U a) (U b) = fromIntegerU_inlineable $ a + b
+
+{-# NOINLINE minU #-}
+minU (U a) (U b) = fromIntegerU_inlineable $ a - b
+
+{-# NOINLINE timesU #-}
+timesU (U a) (U b) = fromIntegerU_inlineable $ a * b
+
+{-# NOINLINE signumU #-}
+signumU :: Unsigned n -> Unsigned n
+signumU (U 0) = (U 0)
+signumU (U _) = (U 1)
+
+fromIntegerU,fromIntegerU_inlineable :: forall n . KnownNat n => Integer -> Unsigned (n :: Nat)
+{-# NOINLINE fromIntegerU #-}
+fromIntegerU = fromIntegerU_inlineable
+{-# INLINABLE fromIntegerU_inlineable #-}
+fromIntegerU_inlineable i = U $ i `mod` (2 ^ fromSNat (snat :: SNat n))
+
+instance KnownNat n => Real (Unsigned n) where
+  toRational = toRational . toIntegerU
+
+instance KnownNat n => Integral (Unsigned n) where
+  quot      = quotU
+  rem       = remU
+  div       = quotU
+  mod       = modU
+  quotRem   = quotRemU
+  divMod    = divModU
+  toInteger = toIntegerU
+
+quotU,remU,modU :: KnownNat n => Unsigned n -> Unsigned n -> Unsigned n
+{-# NOINLINE quotU #-}
+quotU = (fst.) . quotRemU_inlineable
+{-# NOINLINE remU #-}
+remU = (snd.) . quotRemU_inlineable
+{-# NOINLINE modU #-}
+(U a) `modU` (U b) = fromIntegerU_inlineable (a `mod` b)
+
+quotRemU,divModU :: KnownNat n => Unsigned n -> Unsigned n -> (Unsigned n, Unsigned n)
+quotRemU n d = (n `quotU` d,n `remU` d)
+divModU n d  = (n `quotU` d,n `modU` d)
+
+{-# INLINEABLE quotRemU_inlineable #-}
+quotRemU_inlineable :: KnownNat n => Unsigned n -> Unsigned n -> (Unsigned n, Unsigned n)
+(U a) `quotRemU_inlineable` (U b) = let (a',b') = a `quotRem` b
+                                    in (fromIntegerU_inlineable a', fromIntegerU_inlineable b')
+
+{-# NOINLINE toIntegerU #-}
+toIntegerU :: Unsigned n -> Integer
+toIntegerU (U n) = n
+
+instance KnownNat n => Bits (Unsigned n) where
+  (.&.)          = andU
+  (.|.)          = orU
+  xor            = xorU
+  complement     = complementU
+  bit            = bitU
+  testBit        = testBitU
+  bitSizeMaybe   = Just . finiteBitSizeU
+  isSigned       = const False
+  shiftL         = shiftLU
+  shiftR         = shiftRU
+  rotateL        = rotateLU
+  rotateR        = rotateRU
+  popCount       = popCountU
+
+andU,orU,xorU :: KnownNat n => Unsigned n -> Unsigned n -> Unsigned n
+{-# NOINLINE andU #-}
+(U a) `andU` (U b) = fromIntegerU_inlineable (a .&. b)
+{-# NOINLINE orU #-}
+(U a) `orU` (U b)  = fromIntegerU_inlineable (a .|. b)
+{-# NOINLINE xorU #-}
+(U a) `xorU` (U b) = fromIntegerU_inlineable (xor a b)
+
+{-# NOINLINE complementU #-}
+complementU :: KnownNat n => Unsigned n -> Unsigned n
+complementU = fromBitVector . vmap complement . toBitVector
+
+{-# NOINLINE bitU #-}
+bitU :: KnownNat n => Int -> Unsigned n
+bitU = fromIntegerU_inlineable . bit
+
+{-# NOINLINE testBitU #-}
+testBitU :: Unsigned n -> Int -> Bool
+testBitU (U n) i = testBit n i
+
+shiftLU,shiftRU,rotateLU,rotateRU :: KnownNat n => Unsigned n -> Int -> Unsigned n
+{-# NOINLINE shiftLU #-}
+shiftLU _ b | b < 0  = error "'shiftL'{Unsigned} undefined for negative numbers"
+shiftLU (U n) b      = fromIntegerU_inlineable (shiftL n b)
+{-# NOINLINE shiftRU #-}
+shiftRU _ b | b < 0  = error "'shiftR'{Unsigned} undefined for negative numbers"
+shiftRU (U n) b      = fromIntegerU_inlineable (shiftR n b)
+{-# NOINLINE rotateLU #-}
+rotateLU _ b | b < 0 = error "'shiftL'{Unsigned} undefined for negative numbers"
+rotateLU n b         = let b' = b `mod` finiteBitSizeU n
+                       in shiftL n b' .|. shiftR n (finiteBitSizeU n - b')
+{-# NOINLINE rotateRU #-}
+rotateRU _ b | b < 0 = error "'shiftR'{Unsigned} undefined for negative numbers"
+rotateRU n b         = let b' = b `mod` finiteBitSizeU n
+                       in shiftR n b' .|. shiftL n (finiteBitSizeU n - b')
+
+{-# NOINLINE popCountU #-}
+popCountU :: Unsigned n -> Int
+popCountU (U n) = popCount n
+
+instance KnownNat n => FiniteBits (Unsigned n) where
+  finiteBitSize  = finiteBitSizeU
+
+{-# NOINLINE finiteBitSizeU #-}
+finiteBitSizeU :: forall n . KnownNat n => Unsigned n -> Int
+finiteBitSizeU _ = fromInteger $ fromSNat (snat :: SNat n)
+
+instance forall n . KnownNat n => Lift (Unsigned n) where
+  lift (U i) = sigE [| fromIntegerU i |] (decUnsigned $ fromSNat (snat :: (SNat n)))
+
+decUnsigned :: Integer -> TypeQ
+decUnsigned n = appT (conT ''Unsigned) (litT $ numTyLit n)
+
+instance Show (Unsigned n) where
+  show (U n) = show n
+
+instance KnownNat n => Default (Unsigned n) where
+  def = fromIntegerU 0
+
+instance BitVector (Unsigned n) where
+  type BitSize (Unsigned n) = n
+  toBV   = toBitVector
+  fromBV = fromBitVector
+
+{-# NOINLINE toBitVector #-}
+toBitVector :: KnownNat n => Unsigned n -> Vec n Bit
+toBitVector (U m) = vreverse $ vmap (\x -> if odd x then H else L) $ viterateI (`div` 2) m
+
+{-# NOINLINE fromBitVector #-}
+fromBitVector :: KnownNat n => Vec n Bit -> Unsigned n
+fromBitVector = fromBitList . reverse . toList
+
+{-# INLINABLE fromBitList #-}
+fromBitList :: KnownNat n => [Bit] -> Unsigned n
+fromBitList l = fromIntegerU_inlineable
+              $ sum [ n
+                    | (n,b) <- zip (iterate (*2) 1) l
+                    , b == H
+                    ]
+
+{-# NOINLINE resizeU #-}
+resizeU :: KnownNat m => Unsigned n -> Unsigned m
+resizeU (U n) = fromIntegerU_inlineable n
diff --git a/src/CLaSH/Sized/Vector.hs b/src/CLaSH/Sized/Vector.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Sized/Vector.hs
@@ -0,0 +1,327 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ExplicitForAll      #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeOperators       #-}
+
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
+
+module CLaSH.Sized.Vector
+  ( Vec(..), (<:)
+  , vhead, vtail, vlast, vinit
+  , (+>>), (<<+), (<++>), vconcat
+  , vsplit, vsplitI, vunconcat, vunconcatI, vmerge
+  , vreverse, vmap, vzipWith
+  , vfoldr, vfoldl, vfoldr1, vfoldl1
+  , vzip, vunzip
+  , (!), vreplace
+  , vtake, vtakeI, vdrop, vdropI, vexact, vselect, vselectI
+  , vcopy, vcopyI, viterate, viterateI, vgenerate, vgenerateI
+  , toList, v
+  )
+where
+
+import Control.Applicative
+import Data.Traversable
+import Data.Foldable hiding (toList)
+import GHC.TypeLits
+import Language.Haskell.TH (ExpQ)
+import Language.Haskell.TH.Syntax (Lift(..))
+import Unsafe.Coerce (unsafeCoerce)
+
+import CLaSH.Promoted.Nat
+
+data Vec :: Nat -> * -> * where
+  Nil  :: Vec 0 a
+  (:>) :: a -> Vec n a -> Vec (n + 1) a
+
+infixr 5 :>
+
+instance Show a => Show (Vec n a) where
+  show vs = "<" ++ punc vs ++ ">"
+    where
+      punc :: Show a => Vec m a -> String
+      punc Nil        = ""
+      punc (x :> Nil) = show x
+      punc (x :> xs)  = show x ++ "," ++ punc xs
+
+instance Eq a => Eq (Vec n a) where
+  v1 == v2 = vfoldr (&&) True (vzipWith (==) v1 v2)
+
+instance KnownNat n => Applicative (Vec n) where
+  pure  = vcopyI
+  (<*>) = vzipWith ($)
+
+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
+
+instance Functor (Vec n) where
+  fmap = fmapDefault
+
+{-# NOINLINE vhead #-}
+vhead :: Vec (n + 1) a -> a
+vhead (x :> _) = x
+
+{-# NOINLINE vtail #-}
+vtail :: Vec (n + 1) a -> Vec n a
+vtail (_ :> xs) = unsafeCoerce xs
+
+{-# NOINLINE vlast #-}
+vlast :: Vec (n + 1) a -> a
+vlast (x :> Nil)     = x
+vlast (_ :> y :> ys) = vlast (y :> ys)
+
+{-# NOINLINE vinit #-}
+vinit :: Vec (n + 1) a -> Vec n a
+vinit (_ :> Nil)     = unsafeCoerce Nil
+vinit (x :> y :> ys) = unsafeCoerce (x :> vinit (y :> ys))
+
+{-# NOINLINE shiftIntoL #-}
+shiftIntoL :: a -> Vec n a -> Vec n a
+shiftIntoL _ Nil       = Nil
+shiftIntoL s (x :> xs) = s :> (vinit (x:>xs))
+
+infixr 4 +>>
+{-# INLINEABLE (+>>) #-}
+(+>>) :: a -> Vec n a -> Vec n a
+s +>> xs = shiftIntoL s xs
+
+{-# NOINLINE snoc #-}
+snoc :: a -> Vec n a -> Vec (n + 1) a
+snoc s Nil       = s :> Nil
+snoc s (x :> xs) = x :> (snoc s xs)
+
+infixl 5 <:
+{-# INLINEABLE (<:) #-}
+(<:) :: Vec n a -> a -> Vec (n + 1) a
+xs <: s = snoc s xs
+
+{-# NOINLINE shiftIntoR #-}
+shiftIntoR :: a -> Vec n a -> Vec n a
+shiftIntoR _ Nil     = Nil
+shiftIntoR s (x:>xs) = snoc s (vtail (x:>xs))
+
+infixl 4 <<+
+{-# INLINE (<<+) #-}
+(<<+) :: Vec n a -> a -> Vec n a
+xs <<+ s = shiftIntoR s xs
+
+{-# NOINLINE vappend #-}
+vappend :: Vec n a -> Vec m a -> Vec (n + m) a
+vappend Nil       ys = ys
+vappend (x :> xs) ys = unsafeCoerce (x :> (vappend xs ys))
+
+infixr 5 <++>
+{-# INLINE (<++>) #-}
+(<++>) :: Vec n a -> Vec m a -> Vec (n + m) a
+xs <++> ys = vappend xs ys
+
+{-# NOINLINE vsplit #-}
+vsplit :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
+vsplit n xs = vsplitU (toUNat n) xs
+
+vsplitU :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
+vsplitU UZero     ys        = (Nil,ys)
+vsplitU (USucc s) (y :> ys) = let (as,bs) = vsplitU s (unsafeCoerce ys)
+                              in  (y :> as, bs)
+
+{-# INLINEABLE vsplitI #-}
+vsplitI :: KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a)
+vsplitI = withSNat vsplit
+
+{-# NOINLINE vconcat #-}
+vconcat :: Vec n (Vec m a) -> Vec (n * m) a
+vconcat Nil       = Nil
+vconcat (x :> xs) = unsafeCoerce (vappend x (vconcat xs))
+
+{-# NOINLINE vunconcat #-}
+vunconcat :: SNat n -> SNat m -> Vec (n * m) a -> Vec n (Vec m a)
+vunconcat n m xs = vunconcatU (toUNat n) (toUNat m) xs
+
+vunconcatU :: UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
+vunconcatU UZero      _  _  = Nil
+vunconcatU (USucc n') m' ys = let (as,bs) = vsplitU m' (unsafeCoerce ys)
+                              in  as :> vunconcatU n' m' bs
+
+{-# INLINEABLE vunconcatI #-}
+vunconcatI :: (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a)
+vunconcatI = (withSNat . withSNat) vunconcat
+
+{-# NOINLINE vmerge #-}
+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 #-}
+vreverse :: Vec n a -> Vec n a
+vreverse Nil        = Nil
+vreverse (x :> xs)  = vreverse xs <: x
+
+{-# NOINLINE vmap #-}
+vmap :: (a -> b) -> Vec n a -> Vec n b
+vmap _ Nil       = Nil
+vmap f (x :> xs) = f x :> vmap f xs
+
+{-# NOINLINE vzipWith #-}
+vzipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
+vzipWith _ Nil       Nil       = Nil
+vzipWith f (x :> xs) (y :> ys) = f x y :> (vzipWith f xs (unsafeCoerce ys))
+
+{-# NOINLINE vfoldr #-}
+vfoldr :: (a -> b -> b) -> b -> Vec n a -> b
+vfoldr _ z Nil       = z
+vfoldr f z (x :> xs) = f x (vfoldr f z xs)
+
+{-# NOINLINE vfoldl #-}
+vfoldl :: (b -> a -> b) -> b -> Vec n a -> b
+vfoldl _ z Nil       = z
+vfoldl f z (x :> xs) = vfoldl f (f z x) xs
+
+{-# NOINLINE vfoldr1 #-}
+vfoldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a
+vfoldr1 _ (x :> Nil)       = x
+vfoldr1 f (x :> (y :> ys)) = f x (vfoldr1 f (y :> ys))
+
+{-# INLINEABLE vfoldl1 #-}
+vfoldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a
+vfoldl1 f xs = vfoldl f (vhead xs) (vtail xs)
+
+{-# NOINLINE vzip #-}
+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))
+
+{-# NOINLINE vunzip #-}
+vunzip :: Vec n (a,b) -> (Vec n a, Vec n b)
+vunzip Nil = (Nil,Nil)
+vunzip ((a,b) :> xs) = let (as,bs) = vunzip xs
+                       in  (a :> as, b :> bs)
+
+{-# NOINLINE vindexM_integer #-}
+vindexM_integer :: Vec n a -> Integer -> Maybe a
+vindexM_integer Nil       _ = Nothing
+vindexM_integer (x :> _)  0 = Just x
+vindexM_integer (_ :> xs) n = vindexM_integer xs (n-1)
+
+{-# NOINLINE vindex_integer #-}
+vindex_integer :: KnownNat n => Vec n a -> Integer -> a
+vindex_integer xs i = case vindexM_integer xs (maxIndex xs - i) of
+    Just a  -> a
+    Nothing -> error "index out of bounds"
+
+{-# INLINEABLE (!) #-}
+(!) :: (KnownNat n, Integral i) => Vec n a -> i -> a
+xs ! i = vindex_integer xs (toInteger i)
+
+{-# NOINLINE maxIndex #-}
+maxIndex :: forall n a . KnownNat n => Vec n a -> Integer
+maxIndex _ = fromSNat (snat :: SNat n) - 1
+
+{-# NOINLINE vreplaceM_integer #-}
+vreplaceM_integer :: Vec n a -> Integer -> a -> Maybe (Vec n a)
+vreplaceM_integer Nil       _ _ = Nothing
+vreplaceM_integer (_ :> xs) 0 y = Just (y :> xs)
+vreplaceM_integer (x :> xs) n y = case vreplaceM_integer xs (n-1) y of
+                                    Just xs' -> Just (x :> xs')
+                                    Nothing  -> Nothing
+
+{-# NOINLINE vreplace_integer #-}
+vreplace_integer :: KnownNat n => Vec n a -> Integer -> a -> Vec n a
+vreplace_integer xs i a = case vreplaceM_integer xs (maxIndex xs - i) a of
+  Just ys -> ys
+  Nothing -> error "index out of bounds"
+
+{-# INLINEABLE vreplace #-}
+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 :: SNat m -> Vec (m + n) a -> Vec m a
+vtake n = fst . vsplit n
+
+{-# INLINEABLE vtakeI #-}
+vtakeI :: KnownNat m => Vec (m + n) a -> Vec m a
+vtakeI = withSNat vtake
+
+{-# NOINLINE vdrop #-}
+vdrop :: SNat m -> Vec (m + n) a -> Vec n a
+vdrop n = snd . vsplit n
+
+{-# INLINEABLE vdropI #-}
+vdropI :: KnownNat m => Vec (m + n) a -> Vec n a
+vdropI = withSNat vdrop
+
+{-# NOINLINE vexact #-}
+vexact :: SNat m -> Vec (m + (n + 1)) a -> a
+vexact n xs = vhead $ snd $ vsplit n xs
+
+{-# NOINLINE vselect #-}
+vselect ::
+  ((f + (s * n) + 1) <= i)
+  => SNat f
+  -> SNat s
+  -> SNat (n + 1)
+  -> Vec i a
+  -> Vec (n + 1) a
+vselect f s n xs = vselect' (toUNat n) $ vdrop f (unsafeCoerce xs)
+  where
+    vselect' :: UNat n -> Vec m a -> Vec n a
+    vselect' UZero      _           = Nil
+    vselect' (USucc n') vs@(x :> _) = x :> vselect' n' (vdrop s (unsafeCoerce vs))
+
+{-# NOINLINE vselectI #-}
+vselectI ::
+  ((f + (s * n) + 1) <= i, KnownNat (n + 1))
+  => SNat f
+  -> SNat s
+  -> Vec i a
+  -> Vec (n + 1) a
+vselectI f s xs = withSNat (\n -> vselect f s n xs)
+
+{-# NOINLINE vcopy #-}
+vcopy :: SNat n -> a -> Vec n a
+vcopy n a = vreplicateU (toUNat n) a
+
+vreplicateU :: UNat n -> a -> Vec n a
+vreplicateU UZero     _ = Nil
+vreplicateU (USucc s) x = x :> vreplicateU s x
+
+{-# INLINEABLE vcopyI #-}
+vcopyI :: KnownNat n => a -> Vec n a
+vcopyI = withSNat vcopy
+
+{-# NOINLINE viterate #-}
+viterate :: SNat n -> (a -> a) -> a -> Vec n a
+viterate n f a = viterateU (toUNat n) f a
+
+viterateU :: UNat n -> (a -> a) -> a -> Vec n a
+viterateU UZero     _ _ = Nil
+viterateU (USucc s) g x = x :> viterateU s g (g x)
+
+{-# INLINEABLE viterateI #-}
+viterateI :: KnownNat n => (a -> a) -> a -> Vec n a
+viterateI = withSNat viterate
+
+{-# INLINEABLE vgenerate #-}
+vgenerate :: SNat n -> (a -> a) -> a -> Vec n a
+vgenerate n f a = viterate n f (f a)
+
+{-# INLINEABLE vgenerateI #-}
+vgenerateI :: KnownNat n => (a -> a) -> a -> Vec n a
+vgenerateI = withSNat vgenerate
+
+{-# NOINLINE toList #-}
+toList :: Vec n a -> [a]
+toList = vfoldr (:) []
+
+v :: Lift a => [a] -> ExpQ
+v []     = [| Nil |]
+v (x:xs) = [| x :> $(v xs) |]