diff --git a/Data/HList.hs b/Data/HList.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE MagicHash #-}
+{-
+OOHaskell (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+This module gathers the API that we need for OOP in Haskell.  We
+basically select a certain configuration of the HList library, and we
+also import modules that are needed for mutable data and monads. Note
+on overlapping: Needed for the chosen model of labels. Other models
+can be used instead, but the chosen look better in types.
+-}
+
+
+module Data.HList (
+
+ module Data.HList.CommonMain,
+ module Data.HList.GhcSyntax,
+ module Data.HList.GhcRecord,
+ module Data.HList.GhcExperiments,
+ module Data.STRef,
+ module Data.IORef,
+ module Data.Typeable,
+ module Control.Monad,
+ module Control.Monad.ST,
+ module Control.Monad.Fix,
+ module GHC.IOBase,
+-- module DeepNarrow,
+-- module Nominal,
+-- module New,
+-- module Data.HList.HList
+ concrete,
+ (#)
+) where
+
+
+import Data.HList.CommonMain hiding ( HDeleteMany
+                         , hDeleteMany
+                         , TypeCast
+                         , typeCast
+                         )
+
+import Data.HList.GhcSyntax
+import Data.HList.GhcRecord
+import Data.HList.GhcExperiments
+
+import Data.STRef
+import Data.IORef
+import Data.Typeable
+import Control.Monad
+import Control.Monad.ST
+import Control.Monad.Fix
+import GHC.IOBase hiding (stToIO, writeIORef, readIORef, newIORef, IORef,unsafeIOToST,unsafeSTToIO)
+
+infixr 9 #
+(#) :: (HasField l r v) => r -> l -> v
+m # field = (m .!. field)
+
+concrete :: (MonadFix m) => (a -> m a) -> a -> m a
+concrete generator self = generator self
+ where
+  _ = mfix generator
diff --git a/Data/HList/CommonMain.hs b/Data/HList/CommonMain.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/CommonMain.hs
@@ -0,0 +1,36 @@
+{-
+
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   This is a next-to-main module that loads all modules that at least
+   *compile* fine for all the models of interest. See the Makefile
+   for ways to run different models.
+
+-}
+
+module Data.HList.CommonMain (
+
+   module Data.HList.FakePrelude
+ , module Data.HList.HListPrelude
+ , module Data.HList.HArray
+ , module Data.HList.HOccurs
+ , module Data.HList.HTypeIndexed
+ , module Data.HList.TIP
+ , module Data.HList.TIC
+ , module Data.HList.HZip
+ , module Data.HList.Record
+ , module Data.HList.Variant
+) where
+
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+import Data.HList.HArray
+import Data.HList.HOccurs
+import Data.HList.HTypeIndexed
+import Data.HList.TIP
+import Data.HList.TIC
+import Data.HList.HZip
+import Data.HList.Record
+import Data.HList.Variant
diff --git a/Data/HList/FakePrelude.hs b/Data/HList/FakePrelude.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/FakePrelude.hs
@@ -0,0 +1,256 @@
+{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
+
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Some very basic technology for faking dependent types in Haskell.
+-}
+
+module Data.HList.FakePrelude where
+
+
+{-----------------------------------------------------------------------------}
+
+-- Type-level Booleans
+
+data HTrue; hTrue :: HTrue; hTrue = undefined
+data HFalse; hFalse :: HFalse; hFalse = undefined
+class HBool x; instance HBool HTrue; instance HBool HFalse
+instance Show HTrue where show _ = "HTrue"
+instance Show HFalse where show _ = "HFalse"
+
+
+-- Conjunction of type-level Booleans
+
+class (HBool t, HBool t', HBool t'') => HAnd t t' t'' | t t' -> t''
+ where
+  hAnd :: t -> t' -> t''
+
+instance HAnd HFalse HFalse HFalse
+ where
+  hAnd _ _ = hFalse
+
+instance HAnd HTrue HFalse HFalse
+ where
+  hAnd _ _ = hFalse
+
+instance HAnd HFalse HTrue HFalse
+ where
+  hAnd _ _ = hFalse
+
+instance HAnd HTrue HTrue HTrue
+ where
+  hAnd _ _ = hTrue
+
+
+-- Disjunction of type-level Booleans
+
+class (HBool t, HBool t', HBool t'') => HOr t t' t'' | t t' -> t''
+ where
+  hOr :: t -> t' -> t''
+
+instance HOr HFalse HFalse HFalse
+ where
+  hOr _ _ = hFalse
+
+instance HOr HTrue HFalse HTrue
+ where
+  hOr _ _ = hTrue
+
+instance HOr HFalse HTrue HTrue
+ where
+  hOr _ _ = hTrue
+
+instance HOr HTrue HTrue HTrue
+ where
+  hOr _ _ = hTrue
+
+
+-- Type-level conditional
+
+class HBool t => HCond t x y z | t x y -> z
+ where
+  hCond :: t -> x -> y -> z
+
+instance HCond HFalse x y y
+ where
+  hCond _ _ y = y
+
+instance HCond HTrue x y x
+ where
+  hCond _ x _ = x
+
+
+-- We could define all kinds of further Boolean operations.
+-- We omit everything what's not needed for the code in the paper.
+
+
+{-----------------------------------------------------------------------------}
+
+-- Type-level naturals
+
+data HZero
+data HSucc n
+
+hZero :: HZero; hZero = undefined
+hSucc :: HNat n => n -> HSucc n; hSucc _ = undefined
+hPred :: HNat n => HSucc n -> n; hPred _ = undefined
+
+class HNat n
+instance HNat HZero
+instance HNat n => HNat (HSucc n)
+
+instance Show HZero where show _ = "HZero"
+instance Show (HSucc HZero)
+ where show _ = "HSucc HZero"
+instance (HNat n, Show (HSucc n)) => Show (HSucc (HSucc n))
+ where show n = "HSucc (" ++ show (hPred n) ++ ")"
+
+class HNat n => HNat2Integral n
+ where
+  hNat2Integral :: Integral i => n -> i
+
+instance HNat2Integral HZero
+ where
+  hNat2Integral _ = 0
+
+instance HNat2Integral n => HNat2Integral (HSucc n)
+ where
+  hNat2Integral n = hNat2Integral (hPred n) + 1
+
+
+{-----------------------------------------------------------------------------}
+
+-- Type-level maybies
+
+data HNothing  = HNothing  deriving Show
+data HJust x   = HJust x   deriving Show
+
+
+{-----------------------------------------------------------------------------}
+
+-- Equality for types
+
+class HBool b => HEq x y b | x y -> b
+
+
+-- Equality instances for naturals
+
+instance HEq HZero HZero HTrue
+instance HNat n => HEq HZero (HSucc n) HFalse
+instance HNat n => HEq (HSucc n) HZero HFalse
+instance (HNat n, HNat n', HEq  n n' b )
+      =>  HEq (HSucc n) (HSucc n') b
+
+hEq :: HEq x y b => x -> y -> b
+hEq =  undefined
+
+
+{-----------------------------------------------------------------------------}
+
+-- Staged equality
+--  - Establish type equality statically
+--  - Establish remaining value-level equality dynamically
+
+class HStagedEq x y
+ where
+  hStagedEq :: x -> y -> Bool
+
+
+{-----------------------------------------------------------------------------}
+
+-- Less than
+
+class HBool b => HLt x y b | x y -> b
+
+
+-- Equality instances for naturals
+
+instance HLt HZero HZero HFalse
+instance HNat n => HLt HZero (HSucc n) HTrue
+instance HNat n => HLt (HSucc n) HZero HFalse
+instance (HNat n, HNat n', HLt  n n' b)
+      =>  HLt (HSucc n) (HSucc n') b
+
+hLt   :: HLt x y b => x -> y -> b
+hLt _ =  undefined
+
+
+{-----------------------------------------------------------------------------}
+
+-- A predicate for type equality
+-- There are different implementations.
+-- See imports in Main*.hs
+
+class HBool b => TypeEq x y b | x y -> b
+
+
+-- Rely on lazy show for type-level Booleans
+typeEq :: TypeEq t t' b => t -> t' -> b
+typeEq = undefined
+
+
+-- A more disciplined version: based on proxies
+proxyEq :: TypeEq t t' b => Proxy t -> Proxy t' -> b
+proxyEq _ _ = undefined
+
+
+{-----------------------------------------------------------------------------}
+
+-- Type-safe cast
+
+class TypeCast x y | x -> y, y -> x
+ where
+  typeCast :: x -> y
+
+
+{-----------------------------------------------------------------------------}
+
+-- A phantom type for type proxies
+
+data Proxy e
+instance Show (Proxy e) where show _ = "Proxy"
+
+proxy :: Proxy e
+proxy =  undefined
+
+toProxy :: e -> Proxy e
+toProxy _ = undefined
+
+unProxy :: Proxy e -> e
+unProxy =  undefined
+
+
+{-----------------------------------------------------------------------------}
+
+-- Type equality and disequality
+
+class TypeEqTrue x y
+class TypeEqFalse x y
+
+typeEqTrue :: TypeEqTrue x y => x -> y -> ()
+typeEqTrue _ _ = ()
+
+typeEqFalse :: TypeEqFalse x y => x -> y -> ()
+typeEqFalse _ _ = ()
+
+
+{-----------------------------------------------------------------------------}
+
+-- Subtyping
+
+class SubType l l'
+
+subType :: SubType l l' => l -> l' -> ()
+subType _ _ = ()
+
+
+{-----------------------------------------------------------------------------}
+
+-- A class without instances for explicit failure
+class Fail x
+
+
+{-----------------------------------------------------------------------------}
diff --git a/Data/HList/GhcExperiments.hs b/Data/HList/GhcExperiments.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/GhcExperiments.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE KindSignatures,MultiParamTypeClasses,FunctionalDependencies,FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
+
+{-
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   This module gathers experiments that do not work with Hugs.
+-}
+
+module Data.HList.GhcExperiments where
+
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+
+class HDeleteMany e l l' | e l -> l'
+ where
+  hDeleteMany :: Proxy e -> l -> l'
+
+instance HDeleteMany e HNil HNil
+ where
+  hDeleteMany _ HNil = HNil
+
+instance (HList l, HDeleteMany e l l')
+      => HDeleteMany e (HCons e l) l'
+ where
+  hDeleteMany p (HCons _ l) = hDeleteMany p l
+
+{-
+
+-- Hopelessly overlapping
+
+instance (HList l, HDeleteMany e l l')
+      => HDeleteMany e (HCons e' l) (HCons e' l')
+ where
+  hDeleteMany p (HCons e' l)
+   =
+     HCons e' (hDeleteMany p l)
+
+-}
+
+instance ( HList l
+         , HDeleteMany e l l'
+         , TypeCast (HCons e' l') l''
+         )
+      =>   HDeleteMany e (HCons e' l) l''
+ where
+  hDeleteMany p (HCons e' l)
+   =
+     typeCast (HCons e' (hDeleteMany p l))
+
+
+-----------------------------------------------------------------------------
+
+-- Test for type constructors
+
+-- signature: * -> *
+class IsTC1 x (f :: * -> *) b | x f -> b
+instance TypeCast HTrue b => IsTC1 (f a) f b
+instance TypeCast HFalse b => IsTC1 f x b
+
+-- signature: * -> * -> *
+class IsTC2 x (f :: * -> * -> *) b | x f -> b
+instance TypeCast HTrue b => IsTC2 (f a b) f b
+instance TypeCast HFalse b => IsTC2 f x b
+
+-- Sample
+funType :: IsTC2 t (->) b => t -> b
+funType = undefined
diff --git a/Data/HList/GhcRecord.hs b/Data/HList/GhcRecord.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/GhcRecord.hs
@@ -0,0 +1,288 @@
+{-# LANGUAGE PatternSignatures, ScopedTypeVariables, EmptyDataDecls,
+  FunctionalDependencies, FlexibleInstances, FlexibleContexts,
+  MultiParamTypeClasses, UndecidableInstances #-}
+
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Extensible records -- operations that (may) require GHC
+
+   See Record.hs for the base module.
+-}
+
+module Data.HList.GhcRecord where
+
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+import Data.HList.HArray
+import Data.HList.Record
+import Data.Typeable
+
+
+{-----------------------------------------------------------------------------}
+
+-- A variation on update.
+-- Replace a proxy by a value of the proxied type.
+hUnproxyLabel :: (HUpdateAtHNat n (LVPair l a) t l', HFind l ls n,
+                               RecordLabels t ls,
+                               HasField l t (Proxy a)) =>
+                                             l -> a -> Record t -> Record l'
+hUnproxyLabel l v r = hUpdateAtLabel l v r
+ where
+  tpe :: a -> Proxy a -> ()
+  tpe _ _ = ()
+  _ = tpe v (hLookupByLabel l r)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Test for values; refuse proxies
+
+hasNoProxies :: HasNoProxies r
+             => Record r -> ()
+hasNoProxies = const ()
+
+
+data ProxyFound x
+class HasNoProxies l
+instance HasNoProxies HNil
+instance Fail (ProxyFound x) => HasNoProxies (HCons (Proxy x) l)
+instance Fail (ProxyFound x) => HasNoProxies (HCons (LVPair lab (Proxy x)) l)
+instance HasNoProxies l => HasNoProxies (HCons e l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Narrow a record to a different record type
+
+-- First is the `monadic' version, which returns the `failure indictator'
+-- (HNothing) if the narrowing fails because the source does not have
+-- all the fields for the target.
+class  NarrowM a b res | a b -> res where
+    narrowM :: Record a -> Record b -> res
+
+instance NarrowM a HNil (HJust (Record HNil)) where
+    narrowM _ _ = HJust emptyRecord
+
+instance (H2ProjectByLabels (HCons l HNil) a rin rout,
+          NarrowM' rin rout b res)
+    => NarrowM a (HCons (LVPair l v) b) res where
+    narrowM (Record a) _ = narrowM' rin rout (undefined::b)
+     where
+        (rin,rout) = h2projectByLabels (undefined::(HCons l HNil)) a
+
+class  NarrowM' rin rout b res | rin rout b -> res where
+    narrowM' :: rin -> rout -> b -> res
+
+instance NarrowM' HNil rout b HNothing where
+    narrowM' _ _ _ = HNothing
+
+instance (NarrowM rout b res',
+          NarrowM'' f res' res)
+    => NarrowM' (HCons f HNil) rout b res where
+    narrowM' (HCons f HNil) rout b =
+        narrowM'' f (narrowM (Record rout) (Record b))
+
+class  NarrowM'' f r r' | f r -> r' where
+    narrowM'' :: f -> r -> r'
+
+instance NarrowM'' f HNothing HNothing where
+    narrowM'' _ _ = HNothing
+
+instance NarrowM'' f (HJust (Record r)) (HJust (Record (HCons f r))) where
+    narrowM'' f (HJust (Record r)) = HJust (Record (HCons f r))
+
+
+class  Narrow a b
+ where narrow :: Record a -> Record b
+
+instance Narrow a HNil
+ where   narrow _ = emptyRecord
+
+instance ( Narrow rout r'
+         , H2ProjectByLabels (HCons l HNil) r (HCons (LVPair l v) HNil) rout
+         ) => Narrow r (HCons (LVPair l v) r')
+  where
+    narrow (Record r) = Record (HCons f r')
+      where
+        (HCons f HNil,rout) = h2projectByLabels (undefined::(HCons l HNil)) r
+        (Record r')    = narrow (Record rout)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Narrow two records to their least-upper bound
+
+class LubNarrow a b c | a b -> c
+ where
+  lubNarrow :: a -> b -> (c,c)
+
+instance ( RecordLabels a la
+         , RecordLabels b lb
+         , HTIntersect la lb lc
+         , H2ProjectByLabels lc a c aout
+         , H2ProjectByLabels lc b c bout
+         , HRLabelSet c
+         )
+      => LubNarrow (Record a) (Record b) (Record c)
+ where
+  lubNarrow ra@(Record _) rb@(Record _) =
+     ( hProjectByLabels (undefined::lc) ra
+     , hProjectByLabels (undefined::lc) rb
+     )
+
+
+{-----------------------------------------------------------------------------}
+
+-- List constructors that also LUB together
+
+data NilLub
+nilLub :: NilLub
+nilLub = undefined :: NilLub
+
+class ConsLub h t l | h t -> l
+ where
+  consLub :: h -> t -> l
+
+instance ConsLub e  NilLub [e]
+ where
+  consLub h _ = [h]
+
+instance LubNarrow e0 e1 e2 => ConsLub e0 [e1] [e2]
+ where
+  consLub h t = fst (head z) : map snd (tail z)
+   where
+    z = map (lubNarrow h) (undefined:t)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Extension of lubNarrow to a heterogeneous list
+
+class HLub l e | l -> e
+ where
+  hLub :: l -> [e]
+
+instance ( LubNarrow h h' e
+         )
+      => HLub (HCons h (HCons h' HNil)) e
+ where
+  hLub (HCons h (HCons h' _)) = [fst ee, snd ee]
+   where
+    ee = lubNarrow h h'
+
+instance ( HLub (HCons h (HCons h'' t)) e'
+         , HLub (HCons h' (HCons h'' t)) e''
+         , LubNarrow e' e'' e
+         , HLub (HCons e (HCons h'' t)) e
+         )
+      => HLub (HCons h (HCons h' (HCons h'' t))) e
+ where
+  hLub (HCons h (HCons h' t)) = fst e : ( snd e : tail r )
+   where
+    e' = hLub (HCons h t)
+    e'' = hLub (HCons h' t)
+    e = lubNarrow (head e') (head e'')
+    r = hLub (HCons (fst e) t)
+
+
+
+{-----------------------------------------------------------------------------}
+-- Record equivalence modulo field order
+-- Decide if two records r1 and r2 are identical or differ only in the order
+-- of their fields.
+-- If the two record types are indeed equivalent, return the witness of
+-- their equivalence, (HJust (r1->r2,r2->r1)). If they are not equivalent,
+-- return HNothing
+-- The function equivR does not examine the values of its arguments:
+-- it needs only their types.
+
+-- The algorithm is simple: two records are equivalent if one can be narrowed
+-- to the other, and vice versa. The narrowing coercions are the desired
+-- witnesses.
+-- The obvious optimization is to check first if two records are of the same
+-- type. That requires TypeEq however. Perhaps we shouldn't use it here.
+-- Use of the record narrowing tacitly assumes that the label of a record
+-- field uniquely determines the type of the field value. Therefore, we
+-- should not use equivR on two records with inconsistent labeling...
+
+class RecordEquiv r1 r2 res | r1 r2 -> res where
+    equivR :: Record r1 -> Record r2 -> res
+
+
+{-
+instance (TypeEq r1 r2 b, RecordEquiv' b r1 r2 res)
+    => RecordEquiv r1 r2 res where
+    equivR _ _ = equivR' (undefined::b) (undefined::r1) (undefined::r2)
+-- Two records have the same type: the fast path
+instance RecordEquiv' HTrue r r
+                      (HJust (Record r->Record r,Record r->Record r)) where
+    equivR' _ _ _ = HJust (id,id)
+-}
+
+instance (NarrowM r1 r2 r12, NarrowM r2 r1 r21,
+          RecordEquiv' (Record r1->r12) (Record r2->r21) res)
+    => RecordEquiv r1 r2 res where
+    equivR r1 r2 = equivR' r1p r2p
+     where r1p (r1 :: Record r1) = narrowM r1 r2
+           r2p (r2 :: Record r2) = narrowM r2 r1
+
+class RecordEquiv' pj1 pj2 res | pj1 pj2 -> res where
+    equivR' :: pj1 -> pj2 -> res
+
+instance RecordEquiv' (r1->HJust r2) (r2->HJust r1) (HJust (r1->r2,r2->r1))
+    where
+    equivR' r12 r21 = HJust (unj.r12,unj.r21)
+     where unj (HJust x) = x
+
+-- r2 has something that r1 doesn't
+instance RecordEquiv' (r1->HNothing) pj2 HNothing where
+    equivR' _ _ = HNothing
+
+-- r1 is a strict superset of r2
+instance RecordEquiv' (r1->HJust r2) (r2->HNothing) HNothing where
+    equivR' _ _ = HNothing
+
+
+{-----------------------------------------------------------------------------}
+-- Typeable instances
+
+hNilTcName :: TyCon
+hNilTcName = mkTyCon "HList.HNil"
+instance Typeable HNil
+ where
+  typeOf _ = mkTyConApp hNilTcName []
+
+hConsTcName :: TyCon
+hConsTcName = mkTyCon "HList.HCons"
+instance (Typeable x, Typeable y) => Typeable (HCons x y)
+ where
+  typeOf (HCons x y)
+   = mkTyConApp hConsTcName [ typeOf x, typeOf y ]
+
+recordTcName :: TyCon
+recordTcName = mkTyCon "HList.Record"
+instance Typeable x => Typeable (Record x)
+ where
+  typeOf (Record x)
+   = mkTyConApp recordTcName [ typeOf x ]
+
+hFieldTcName :: TyCon
+hFieldTcName = mkTyCon "HList.F"
+instance (Typeable x, Typeable y) => Typeable (LVPair x y)
+ where
+  typeOf _
+   = mkTyConApp hFieldTcName [ typeOf (undefined::x), typeOf (undefined::y)  ]
+
+proxyTcName :: TyCon
+proxyTcName = mkTyCon "HList.Proxy"
+instance Typeable x => Typeable (Proxy x)
+ where
+  typeOf (_::Proxy x)
+   = mkTyConApp proxyTcName [ typeOf (undefined::x) ]
+
+
+{-----------------------------------------------------------------------------}
+
diff --git a/Data/HList/GhcSyntax.hs b/Data/HList/GhcSyntax.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/GhcSyntax.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Some dedicated infix operators at the type and the value level.
+-}
+
+module Data.HList.GhcSyntax where
+
+import Data.HList.HArray (HUpdateAtHNat())
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+import Data.HList.HOccurs
+import Data.HList.Record
+import Data.HList.GhcRecord
+import Data.HList.TIP
+import Data.HList.TIC
+
+
+{-----------------------------------------------------------------------------}
+
+-- Convenience notation for type sequences
+
+infixr 2 :*:
+infixr 2 .*.
+
+type e :*: l = HCons e l
+
+(.*.) :: HExtend e l l' => e -> l -> l'
+(.*.) =  hExtend
+
+
+{-----------------------------------------------------------------------------}
+
+-- Convenience notation for records
+
+infixr 4 :=:
+type l :=: v = LVPair l v
+
+infixr 4 .=.
+(.=.) :: l -> v -> LVPair l v
+l .=. v = newLVPair l v
+
+infixr 3 .!.
+(.!.) :: (HasField l r v) => r -> l -> v
+r .!. l =  hLookupByLabel l r
+
+infixl 1 .-.
+(.-.) :: (H2ProjectByLabels (HCons e HNil) t t1 t2) => Record t -> e -> Record t2
+r .-. l =  hDeleteAtLabel l r
+
+infixl 1 .@.
+(.@.) :: (HUpdateAtHNat n (LVPair t t1) t2 l',
+         HFind t ls n,
+         RecordLabels t2 ls) =>
+        Record t2 -> LVPair t t1 -> Record l'
+r .@. f@(LVPair v) =  hUpdateAtLabel (labelLVPair f) v r
+
+infixr 1 .^.
+(.^.) :: (HasField t t2 (Proxy t1),
+         RecordLabels t2 ls,
+         HFind t ls n,
+         Data.HList.HArray.HUpdateAtHNat n (LVPair t t1) t2 l') =>
+         LVPair t t1 -> Record t2 -> Record l'
+f@(LVPair v) .^. r = hUnproxyLabel (labelLVPair f) v r
+
+infixr 1 .<.
+(.<.) :: (HasField t t2 t1,
+         RecordLabels t2 ls,
+         HFind t ls n,
+         HUpdateAtHNat n (LVPair t t1) t2 l') =>
+        LVPair t t1 -> Record t2 -> Record l'
+f@(LVPair v) .<. r = hTPupdateAtLabel (labelLVPair f) v r
+
+infixl 1 .<++.
+(.<++.) :: (HLeftUnion r r' r'') => r -> r' -> r''
+r .<++. r' = hLeftUnion r r'
+
+
+{-----------------------------------------------------------------------------}
+
+-- Convenience notation for TIRs
+
+infixr 2 :+:
+infixr 2 .+.
+
+type e :+: l = HCons (Proxy e) l
+
+(.+.) :: ( HTypeIndexed l
+         , HTypeProxied l
+         , HOccursNot (Proxy e) l
+         )
+      => e -> TIP l -> TIP (HCons (Proxy e) l)
+e .+. r = hExtend (toProxy e) r
+
+
+{-----------------------------------------------------------------------------}
diff --git a/Data/HList/HArray.hs b/Data/HList/HArray.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/HArray.hs
@@ -0,0 +1,249 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
+  FlexibleContexts, UndecidableInstances #-}
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Array-like access to HLists.
+ -}
+
+module Data.HList.HArray where
+
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+
+
+{-----------------------------------------------------------------------------}
+
+-- A lookup operation
+
+class HNat n => HLookupByHNat n l e | n l -> e
+ where
+  hLookupByHNat :: n -> l -> e
+
+instance HLookupByHNat HZero (HCons e l) e
+ where
+  hLookupByHNat _ (HCons e _) = e
+
+instance (HLookupByHNat n l e', HNat n)
+      => HLookupByHNat (HSucc n) (HCons e l) e'
+ where
+  hLookupByHNat n (HCons _ l) = hLookupByHNat (hPred n) l
+
+
+{-----------------------------------------------------------------------------}
+
+-- A delete operation
+
+class HNat n => HDeleteAtHNat n l l' | n l -> l'
+ where
+  hDeleteAtHNat :: n -> l -> l'
+
+instance HDeleteAtHNat HZero (HCons e l) l
+ where
+  hDeleteAtHNat _ (HCons _ l) = l
+
+instance (HDeleteAtHNat n l l', HNat n)
+      => HDeleteAtHNat (HSucc n) (HCons e l) (HCons e l')
+ where
+  hDeleteAtHNat n (HCons e l) = HCons e (hDeleteAtHNat (hPred n) l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- An update operation
+
+class HNat n => HUpdateAtHNat n e l l' | n e l -> l', l' n -> e
+ where
+  hUpdateAtHNat :: n -> e -> l -> l'
+
+instance HUpdateAtHNat HZero e' (HCons e l) (HCons e' l)
+ where
+  hUpdateAtHNat _ e' (HCons _ l) = HCons e' l
+
+instance (HUpdateAtHNat n e' l l', HNat n)
+      => HUpdateAtHNat (HSucc n) e' (HCons e l) (HCons e l')
+ where
+  hUpdateAtHNat n e' (HCons e l)
+   = HCons e (hUpdateAtHNat (hPred n) e' l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Splitting an array according to indices
+hSplitByHNats :: (HSplitByHNats' ns l' l'1 l'', HMap (HAddTag HTrue) l l') =>
+                ns -> l -> (l'1, l'')
+hSplitByHNats ns l = hSplitByHNats' ns (hFlag l)
+
+class HNats ns => HSplitByHNats' ns l l' l'' | ns l -> l' l''
+ where
+  hSplitByHNats' :: ns -> l -> (l',l'')
+
+instance HSplit l l' l''
+      => HSplitByHNats' HNil l HNil l'
+ where
+  hSplitByHNats' HNil l = (HNil,l')
+   where
+    (l',_) = hSplit l
+
+instance ( HLookupByHNat n l (e,b)
+         , HUpdateAtHNat n (e,HFalse) l l'''
+         , HSplitByHNats' ns l''' l' l''
+         )
+      =>   HSplitByHNats' (HCons n ns) l (HCons e l') l''
+ where
+  hSplitByHNats' (HCons n ns) l = (HCons e l',l'')
+   where
+    (e,_)    = hLookupByHNat  n l
+    l'''     = hUpdateAtHNat  n (e,hFalse) l
+    (l',l'') = hSplitByHNats' ns l'''
+
+
+{-----------------------------------------------------------------------------}
+
+-- Another projection operation
+
+class HNats ns => HProjectByHNats ns l l' | ns l -> l'
+ where
+  hProjectByHNats :: ns -> l -> l'
+
+instance HProjectByHNats HNil HNil HNil
+ where
+  hProjectByHNats _ _ = HNil
+
+instance HProjectByHNats HNil (HCons e l) HNil
+ where
+  hProjectByHNats _ _ = HNil
+
+instance ( HLookupByHNat n (HCons e l) e'
+         , HProjectByHNats ns (HCons e l) l'
+         )
+         => HProjectByHNats (HCons n ns) (HCons e l) (HCons e' l')
+ where
+  hProjectByHNats (HCons n ns) l = HCons e' l'
+   where e' = hLookupByHNat n l
+         l' = hProjectByHNats ns l
+
+
+{-----------------------------------------------------------------------------}
+
+-- The complement of projection
+
+class HProjectAwayByHNats ns l l' | ns l -> l'
+ where
+  hProjectAwayByHNats :: ns -> l -> l'
+
+instance ( HLength l len
+         , HBetween len nats
+         , HDiff nats ns ns'
+         , HProjectByHNats ns' l l'
+         )
+           => HProjectAwayByHNats ns l l'
+ where
+  hProjectAwayByHNats ns l = l'
+   where
+    len  = hLength l
+    nats = hBetween len
+    ns'  = hDiff nats ns
+    l'   = hProjectByHNats ns' l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Generate naturals from 1 to x - 1
+
+class HBetween x y | x -> y
+ where
+  hBetween :: x -> y
+
+instance HBetween (HSucc HZero) (HCons HZero HNil)
+ where
+  hBetween _ = HCons hZero HNil
+
+instance ( HNat x
+         , HBetween (HSucc x) y
+         , HAppend y (HCons (HSucc x) HNil) z
+         , HList y
+         )
+           => HBetween (HSucc (HSucc x)) z
+ where
+  hBetween x = hBetween (hPred x) `hAppend` HCons (hPred x) HNil
+
+
+-- Set-difference on naturals
+
+class HDiff x y z | x y -> z
+ where
+  hDiff :: x -> y -> z
+
+instance HDiff HNil x HNil
+ where
+  hDiff _ _ = HNil
+
+instance ( HOrdMember e y b
+         , HDiff x y z
+         , HCond b z (HCons e z) z'
+         )
+           => HDiff (HCons e x) y z'
+ where
+  hDiff (HCons e x) y = z'
+   where z' = hCond b z (HCons e z)
+         b  = hOrdMember e y
+         z  = hDiff x y
+
+
+-- Membership test for types with HOrd instances
+-- This special type equality/comparison is entirely pure!
+
+class HOrdMember e l b | e l -> b
+ where
+  hOrdMember :: e -> l -> b
+
+instance HOrdMember e HNil HFalse
+ where
+  hOrdMember _ _ = hFalse
+
+instance ( HEq e e' b1
+         , HOrdMember e l b2
+         , HOr b1 b2 b
+         )
+           => HOrdMember e (HCons e' l) b
+ where
+  hOrdMember e (HCons e' l) = hOr b1 b2
+   where
+    b1 = hEq e e'
+    b2 = hOrdMember e l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Length operation
+
+class (HList l, HNat n) => HLength l n | l -> n
+instance HLength HNil HZero
+instance (HLength l n, HNat n, HList l)
+      => HLength (HCons a l) (HSucc n)
+
+hLength   :: HLength l n => l -> n
+hLength _ =  undefined
+
+
+{-----------------------------------------------------------------------------}
+
+-- Bounded lists
+
+class HMaxLength l s
+instance (HLength l s', HLt s' (HSucc s) HTrue) => HMaxLength l s
+
+class HMinLength l s
+instance (HLength l s', HLt s (HSucc s') HTrue) => HMinLength l s
+
+class HSingleton l
+instance HLength l (HSucc HZero) => HSingleton l
+
+hSingle :: (HSingleton l, HHead l e) => l -> e
+hSingle = hHead
+
+
+{-----------------------------------------------------------------------------}
diff --git a/Data/HList/HListPrelude.hs b/Data/HList/HListPrelude.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/HListPrelude.hs
@@ -0,0 +1,668 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
+  UndecidableInstances, FlexibleContexts #-}
+
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Basic declarations for typeful heterogeneous lists.
+ -}
+
+module Data.HList.HListPrelude where
+
+import Data.HList.FakePrelude
+
+{-----------------------------------------------------------------------------}
+
+-- Heterogeneous type sequences
+
+data HNil      = HNil      deriving (Eq,Show,Read)
+data HCons e l = HCons e l deriving (Eq,Show,Read)
+
+
+{-----------------------------------------------------------------------------}
+
+-- The set of all types of heterogeneous lists
+
+class HList l
+instance HList HNil
+instance HList l => HList (HCons e l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Public constructors
+
+hNil  :: HNil
+hNil  =  HNil
+
+hCons :: HList l => e -> l -> HCons e l
+hCons e l = HCons e l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Basic list functions
+
+class HHead l h | l -> h
+ where
+  hHead :: l -> h
+
+instance HHead (HCons e l) e
+ where
+  hHead (HCons e _) = e
+
+class HTail l l' | l -> l'
+ where
+  hTail :: l -> l'
+
+instance HTail (HCons e l) l
+ where
+  hTail (HCons _ l) = l
+
+
+
+{-----------------------------------------------------------------------------}
+
+-- A class for extension
+
+class HExtend e l l' | e l -> l', l' -> e l
+ where
+  hExtend :: e -> l -> l'
+
+instance HExtend e HNil (HCons e HNil)
+ where
+  hExtend e l = HCons e l
+
+instance HList l => HExtend e (HCons e' l) (HCons e (HCons e' l))
+ where
+  hExtend e l = HCons e l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Appending HLists
+
+-- The normal append for comparison
+
+append :: [a] -> [a] -> [a]
+append [] l = l
+append (x:l) l' = x : append l l'
+
+
+-- The class HAppend
+
+class HAppend l l' l'' | l l' -> l''
+ where
+  hAppend :: l -> l' -> l''
+
+
+-- The instance following the normal append
+
+instance HList l => HAppend HNil l l
+ where
+  hAppend HNil l = l
+
+instance (HList l, HAppend l l' l'')
+      => HAppend (HCons x l) l' (HCons x l'')
+ where
+  hAppend (HCons x l) l' = HCons x (hAppend l l')
+
+
+{-----------------------------------------------------------------------------}
+
+-- Reversing HLists
+
+class HReverse l1 l2 | l1 -> l2, l2 -> l1
+ where
+  hReverse:: l1 -> l2
+
+instance (HReverse' HNil l2 l3, HReverse' HNil l3 l2)
+      =>  HReverse l2 l3
+ where
+  hReverse l1 = hReverse' HNil l1
+
+
+-- l3 = (reverse l2) ++ l1
+
+class HReverse' l1 l2 l3 | l1 l2 -> l3
+ where
+  hReverse':: l1 -> l2 -> l3
+
+instance HReverse' l1 HNil l1
+ where
+  hReverse' l1 HNil = l1
+
+instance HReverse' (HCons a l1) l2' l3
+      => HReverse' l1 (HCons a l2') l3
+ where
+  hReverse' l1 (HCons a l2') = hReverse' (HCons a l1) l2'
+
+
+-- Naive HReverse
+
+class NaiveHReverse l l' | l -> l'
+ where
+  naiveHReverse :: l -> l'
+
+instance NaiveHReverse HNil HNil
+ where
+  naiveHReverse HNil = HNil
+
+instance ( NaiveHReverse l l'
+         , HAppend l' (HCons e HNil) l''
+         )
+      =>   NaiveHReverse (HCons e l) l''
+ where
+  naiveHReverse (HCons e l)
+   = hAppend (naiveHReverse l) (HCons e HNil)
+
+
+{-----------------------------------------------------------------------------}
+
+--
+-- A nicer notation for lists
+--
+
+-- List termination
+hEnd :: HCons t t1 -> HCons t t1
+hEnd t@(HCons _ _) = t
+
+{-
+   Note:
+        - x :: HCons a b
+            means: forall a b. x :: HCons a b
+        - hEnd x
+            means: exists a b. x :: HCons a b
+-}
+
+
+-- Building non-empty lists
+
+hBuild   :: (HBuild' HNil a r) => a -> r
+hBuild x =  hBuild' HNil x
+
+class HBuild' l a r | r-> a l
+ where
+  hBuild' :: l -> a -> r
+
+instance HReverse (HCons a l) (HCons a' l')
+      => HBuild' l a (HCons a' l')
+ where
+  hBuild' l x = hReverse (HCons x l)
+
+instance HBuild' (HCons a l) b r
+      => HBuild' l a (b->r)
+ where
+  hBuild' l x y = hBuild' (HCons x l) y
+
+{-
+
+HList> let x = hBuild True in hEnd x
+HCons True HNil
+
+HList> let x = hBuild True 'a' in hEnd x
+HCons True (HCons 'a' HNil)
+
+HList> let x = hBuild True 'a' "ok" in hEnd x
+HCons True (HCons 'a' (HCons "ok" HNil))
+
+HList> hEnd (hBuild (Key 42) (Name "Angus") Cow (Price 75.5))
+HCons (Key 42) (HCons (Name "Angus") (HCons Cow (HCons (Price 75.5) HNil)))
+
+HList> hEnd (hBuild (Key 42) (Name "Angus") Cow (Price 75.5)) == angus
+True
+
+-}
+
+{-----------------------------------------------------------------------------}
+
+-- A heterogeneous apply operator
+
+class Apply f a r | f a -> r where
+  apply :: f -> a -> r
+  apply = undefined                     -- In case we use Apply for
+                                        -- type-level computations only
+
+
+-- Normal function application
+
+instance Apply (x -> y) x y where
+  apply f x = f x
+
+
+-- Identity
+
+data Id = Id
+
+instance Apply Id x x where
+  apply _ x = x
+
+
+{-----------------------------------------------------------------------------}
+
+-- A heterogeneous fold for all types
+
+class HList l => HFoldr f v l r | f v l -> r
+ where
+  hFoldr :: f -> v -> l -> r
+
+instance HFoldr f v HNil v
+ where
+  hFoldr _ v _ = v
+
+instance ( HFoldr f v l r
+         , Apply f (e,r) r'
+         )
+      => HFoldr f v (HCons e l) r'
+ where
+  hFoldr f v (HCons e l) = apply f (e,hFoldr f v l)
+
+
+{-----------------------------------------------------------------------------}
+
+class HMap f l l' | f l -> l'
+ where
+  hMap :: f -> l -> l'
+
+instance HMap f HNil HNil
+ where
+  hMap _ HNil = HNil
+
+instance (
+           Apply f x y,
+           HMap f xs ys
+         )
+      => HMap f (HCons x xs) (HCons y ys)
+ where
+  hMap f (HCons x xs) = HCons (apply f x) (hMap f xs)
+
+{-----------------------------------------------------------------------------}
+
+-- Map a heterogeneous list to a homogeneous one
+
+class HMapOut f r e
+ where
+  hMapOut :: f -> r -> [e]
+
+instance HMapOut f HNil e
+ where
+  hMapOut _ _ = []
+
+instance ( HMapOut f l e'
+         , Apply f e e'
+         )
+      =>   HMapOut f (HCons e l) e'
+ where
+  hMapOut f (HCons e l) = apply f e : hMapOut f l
+
+
+{-----------------------------------------------------------------------------}
+
+-- A heterogenous version of mapM.
+-- mapM :: forall b m a. (Monad m) => (a -> m b) -> [a] -> m [b]
+-- Likewise for mapM_.
+
+hMapM   :: (Monad m, HMapOut f l (m e)) => f -> l -> [m e]
+hMapM f =  hMapOut f
+
+-- GHC doesn't like its own type.
+-- hMapM_  :: forall m a f e. (Monad m, HMapOut f a (m e)) => f -> a -> m ()
+-- Without explicit type signature, it's Ok. Sigh.
+-- Anyway, Hugs does insist on a better type. So we restrict as follows:
+--
+hMapM_   :: (Monad m, HMapOut f l (m ())) => f -> l -> m ()
+hMapM_ f =  sequence_ .  disambiguate . hMapM f
+ where
+  disambiguate :: [q ()] -> [q ()]
+  disambiguate =  id
+
+
+{-----------------------------------------------------------------------------}
+
+-- A reconstruction of append
+
+append' :: [a] -> [a] -> [a]
+append' l l' = foldr (:) l' l
+
+hAppend' :: (HFoldr ApplyHCons v l r) => l -> v -> r
+hAppend' l l' = hFoldr ApplyHCons l' l
+
+data ApplyHCons = ApplyHCons
+
+instance HList l => Apply ApplyHCons (e,l) (HCons e l)
+ where
+  apply ApplyHCons (e,l) = hCons e l
+
+
+{-----------------------------------------------------------------------------}
+
+-- A heterogeneous map for all types
+
+data HMap' f = HMap' f
+
+hMap' :: (HFoldr (HMap' f) HNil l r) => f -> l -> r
+hMap' f = hFoldr (HMap' f) hNil
+
+instance Apply f e e'
+      => Apply (HMap' f) (e,l) (HCons e' l)
+ where
+  apply (HMap' f) (e,l) = HCons e' l
+   where
+    e' = apply f e
+
+
+{-----------------------------------------------------------------------------}
+
+-- A function for showing
+
+data HShow  = HShow
+data HSeq x = HSeq x
+
+instance Show x => Apply HShow x (IO ())
+ where
+  apply _ x = do putStrLn $ show x
+
+instance ( Monad m
+         , Apply f x (m ())
+         )
+      => Apply (HSeq f) (x,m ()) (m ())
+ where
+  apply (HSeq f) (x,c) = do apply f x; c
+
+
+{-----------------------------------------------------------------------------}
+
+-- Type-level equality for lists
+
+instance HEq HNil HNil HTrue
+instance HList l => HEq HNil (HCons e l) HFalse
+instance HList l => HEq (HCons e l) HNil HFalse
+instance (HList l, HList l', HEq e e' b, HEq l l' b', HAnd b b' b'')
+      => HEq (HCons e l) (HCons e' l') b''
+
+
+{-----------------------------------------------------------------------------}
+
+-- Staged equality for lists
+
+instance HStagedEq HNil HNil
+ where
+  hStagedEq _ _ = True
+
+instance HStagedEq HNil (HCons e l)
+ where
+  hStagedEq _ _ = False
+
+instance HStagedEq (HCons e l) HNil
+ where
+  hStagedEq _ _ = False
+
+instance ( TypeEq e e' b
+         , HStagedEq l l'
+         , HStagedEq' b e e'
+         )
+      =>   HStagedEq (HCons e l) (HCons e' l')
+ where
+  hStagedEq (HCons e l) (HCons e' l') = (hStagedEq' b e e') && b'
+   where
+    b  = typeEq e e'
+    b' = hStagedEq l l'
+
+class HStagedEq' b e e'
+ where
+  hStagedEq' :: b -> e -> e' -> Bool
+
+instance HStagedEq' HFalse e e'
+ where
+  hStagedEq' _ _ _ = False
+
+instance Eq e => HStagedEq' HTrue e e
+ where
+  hStagedEq' _ = (==)
+
+
+{-----------------------------------------------------------------------------}
+
+
+-- Ensure a list to contain HNats only
+
+class HList l => HNats l
+instance HNats HNil
+instance (HNat n, HNats ns) => HNats (HCons n ns)
+
+
+-- Static set property based on HEq
+
+class HSet l
+instance HSet HNil
+instance (HMember e l HFalse, HSet l) => HSet (HCons e l)
+
+
+-- Find an element in a set based on HEq
+class HNat n => HFind e l n | e l -> n
+ where
+  hFind :: e -> l -> n
+
+instance ( HEq e e' b
+         , HFind' b e l n
+         )
+      =>   HFind e (HCons e' l) n
+ where
+  hFind e (HCons e' l) = n
+   where
+    b  = hEq e e'
+    n  = hFind' b e l
+
+class HNat n => HFind' b e l n | b e l -> n
+ where
+  hFind' :: b -> e -> l -> n
+
+instance HFind' HTrue e l HZero
+ where
+  hFind' _ _ _ = hZero
+
+instance HFind e l n
+      => HFind' HFalse e l (HSucc n)
+ where
+  hFind' _ e l = hSucc (hFind e l)
+
+
+-- Membership test
+
+class HBool b => HMember e l b | e l -> b
+instance HMember e HNil HFalse
+instance (HEq e e' b, HMember e l b', HOr b b' b'')
+      =>  HMember e (HCons e' l) b''
+
+hMember :: HMember e l b => e -> l -> b
+hMember _ _ = undefined
+
+
+-- Another type-level membership test
+-- Check to see if an element e occurs in a list l
+-- If not, return HNothing
+-- If the element does occur, return HJust l'
+-- where l' is a type-level list without e
+
+class HMemberM e l r | e l -> r
+instance HMemberM e HNil HNothing
+instance (HEq e e' b, HMemberM' b e (HCons e' l) res)
+      =>  HMemberM e (HCons e' l) res
+class HMemberM' b e l r | b e l -> r
+instance HMemberM' HTrue e (HCons e l) (HJust l)
+instance (HMemberM e l r, HMemberM' r e (HCons e' l) res)
+    => HMemberM' HFalse e (HCons e' l) res
+instance HMemberM' HNothing e l HNothing
+instance HMemberM' (HJust l') e (HCons e' l) (HJust (HCons e' l'))
+
+
+
+-- Membership test based on type equality
+
+class HBool b => HTMember e l b | e l -> b
+instance HTMember e HNil HFalse
+instance (TypeEq e e' b, HTMember e l b', HOr b b' b'')
+      =>  HTMember e (HCons e' l) b''
+
+hTMember :: HTMember e l b => e -> l -> b
+hTMember _ _ = undefined
+
+
+-- Intersection based on HTMember
+
+class HTIntersect l1 l2 l3 | l1 l2 -> l3
+ where
+  hTIntersect :: l1 -> l2 -> l3
+
+instance HTIntersect HNil l HNil
+ where
+  hTIntersect _ _ = HNil
+
+instance ( HTMember h l1 b
+         , HTIntersectBool b h t l1 l2
+         )
+         => HTIntersect (HCons h t) l1 l2
+ where
+  hTIntersect (HCons h t) l1 = hTIntersectBool b h t l1
+   where
+    b = hTMember h l1
+
+class HBool b => HTIntersectBool b h t l1 l2 | b h t l1 -> l2
+ where
+ hTIntersectBool :: b -> h -> t -> l1 -> l2
+
+instance HTIntersect t l1 l2
+      => HTIntersectBool HTrue h t l1 (HCons h l2)
+ where
+  hTIntersectBool _ h t l1 = HCons h (hTIntersect t l1)
+
+instance HTIntersect t l1 l2
+      => HTIntersectBool HFalse h t l1 l2
+ where
+  hTIntersectBool _ _ t l1 = hTIntersect t l1
+
+
+-- Turn a heterogeneous list into a homogeneous one
+
+class HList2List l e
+ where
+  hList2List :: l -> [e]
+
+instance HList2List HNil e
+ where
+  hList2List HNil = []
+
+instance HList2List l e
+      => HList2List (HCons e l) e
+ where
+  hList2List (HCons e l) = e:hList2List l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Turn list in a list of justs
+
+class ToHJust l l' | l -> l'
+ where
+  toHJust :: l -> l'
+
+instance ToHJust HNil HNil
+ where
+  toHJust HNil = HNil
+
+instance ToHJust l l' => ToHJust (HCons e l) (HCons (HJust e) l')
+ where
+  toHJust (HCons e l) = HCons (HJust e) (toHJust l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Extract justs from list of maybes
+
+class FromHJust l l' | l -> l'
+ where
+  fromHJust :: l -> l'
+
+instance FromHJust HNil HNil
+ where
+  fromHJust HNil = HNil
+
+instance FromHJust l l' => FromHJust (HCons HNothing l) l'
+ where
+  fromHJust (HCons _ l) = fromHJust l
+
+instance FromHJust l l' => FromHJust (HCons (HJust e) l) (HCons e l')
+ where
+  fromHJust (HCons (HJust e) l) = HCons e (fromHJust l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Annotated lists
+
+data HAddTag t = HAddTag t
+data HRmTag    = HRmTag
+
+hAddTag :: (HMap (HAddTag t) l l') => t -> l -> l'
+hAddTag t l = hMap (HAddTag t) l
+hRmTag :: (HMap HRmTag l l') => l -> l'
+hRmTag l    = hMap HRmTag l
+
+instance Apply (HAddTag t) e (e,t)
+ where
+  apply (HAddTag t) e = (e,t)
+
+instance Apply HRmTag (e,t) e
+ where
+  apply HRmTag (e,_) = e
+
+
+-- Annotate list with a type-level Boolean
+hFlag :: (HMap (HAddTag HTrue) l l') => l -> l'
+hFlag l = hAddTag hTrue l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Splitting by HTrue and HFalse
+
+class HSplit l l' l'' | l -> l' l''
+ where
+  hSplit :: l -> (l',l'')
+
+instance HSplit HNil HNil HNil
+ where
+  hSplit HNil = (HNil,HNil)
+
+instance HSplit l l' l''
+      => HSplit (HCons (e,HTrue) l) (HCons e l') l''
+ where
+  hSplit (HCons (e,_) l) = (HCons e l',l'')
+   where
+    (l',l'') = hSplit l
+
+instance HSplit l l' l''
+      => HSplit (HCons (e,HFalse) l) l' (HCons e l'')
+ where
+  hSplit (HCons (e,_) l) = (l',HCons e l'')
+   where
+    (l',l'') = hSplit l
+
+{-
+
+Let expansion makes a difference to Hugs:
+
+HListPrelude> let x = (hFlag (HCons "1" HNil)) in hSplit x
+(HCons "1" HNil,HNil)
+HListPrelude> hSplit (hFlag (HCons "1" HNil))
+ERROR - Unresolved overloading
+*** Type       : HSplit (HCons ([Char],HTrue) HNil) a b => (a,b)
+*** Expression : hSplit (hFlag (HCons "1" HNil))
+
+
+-}
+
+
+{-----------------------------------------------------------------------------}
diff --git a/Data/HList/HOccurs.hs b/Data/HList/HOccurs.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/HOccurs.hs
@@ -0,0 +1,231 @@
+{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses, FlexibleInstances,
+  FlexibleContexts, UndecidableInstances #-}
+
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Result-type-driven operations on typeful heterogeneous lists.
+-}
+
+module Data.HList.HOccurs where
+
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+
+{-----------------------------------------------------------------------------}
+
+-- Zero or more occurrences
+
+class HOccursMany e l
+ where
+  hOccursMany :: l -> [e]
+
+instance HOccursMany e HNil
+ where
+  hOccursMany HNil = []
+
+instance ( HOccursMany e l, HList l )
+      =>   HOccursMany e (HCons e l)
+ where
+  hOccursMany (HCons e l) = e:hOccursMany l
+
+instance ( HOccursMany e l, HList l )
+      =>   HOccursMany e (HCons e' l)
+ where
+  hOccursMany (HCons _ l) = hOccursMany l
+
+
+{-----------------------------------------------------------------------------}
+
+-- One or more occurrences
+
+class HOccursMany1 e l
+ where
+  hOccursMany1 :: l -> (e,[e])
+
+instance ( HOccursMany e l, HList l )
+      =>   HOccursMany1 e (HCons e l)
+ where
+  hOccursMany1 (HCons e l) = (e,hOccursMany l)
+
+instance ( HOccursMany1 e l, HList l )
+      => HOccursMany1 e (HCons e' l)
+ where
+  hOccursMany1 (HCons _ l) = hOccursMany1 l
+
+
+{-----------------------------------------------------------------------------}
+
+-- The first occurrence
+
+class HOccursFst e l
+ where
+  hOccursFst :: l -> e
+
+instance HList l
+      => HOccursFst e (HCons e l)
+ where
+  hOccursFst (HCons e _) = e
+
+instance ( HOccursFst e l, HList l )
+      =>   HOccursFst e (HCons e' l)
+ where
+  hOccursFst (HCons _ l) = hOccursFst l
+
+
+{-----------------------------------------------------------------------------}
+
+-- One occurrence and nothing is left
+
+class HOccurs e l
+ where
+  hOccurs :: l -> e
+
+data TypeNotFound e
+
+instance Fail (TypeNotFound e)
+      => HOccurs e HNil
+ where
+  hOccurs = undefined
+
+instance ( HList l
+         , HOccursNot e l
+         )
+           => HOccurs e (HCons e l)
+ where
+  hOccurs (HCons e _) = e
+
+instance ( HOccurs e l
+         , HList l
+         )
+           => HOccurs e (HCons e' l)
+ where
+  hOccurs (HCons _ l) = hOccurs l
+
+
+{-----------------------------------------------------------------------------}
+
+-- One occurrence and nothing is left
+-- A variation that avoids overlapping instances
+
+class HOccurs' e l
+ where
+  hOccurs' :: l -> e
+
+instance ( TypeEq e e' b
+         , HOccursBool b e (HCons e' l) )
+      =>   HOccurs' e (HCons e' l)
+ where
+  hOccurs' (HCons e' l) = e
+   where
+    e = hOccursBool b (HCons e' l)
+    b = proxyEq (toProxy e) (toProxy e')
+
+class HOccursBool b e l
+ where
+  hOccursBool :: b -> l -> e
+
+instance ( HList l
+         , HOccursNot e l
+         )
+           => HOccursBool HTrue e (HCons e l)
+ where
+  hOccursBool _ (HCons e _) = e
+
+instance ( HOccurs' e l
+         , HList l
+         )
+           => HOccursBool HFalse e (HCons e' l)
+ where
+  hOccursBool _ (HCons _ l) = hOccurs' l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Zero or at least one occurrence
+
+class HOccursOpt e l
+ where
+  hOccursOpt :: l -> Maybe e
+
+instance HOccursOpt e HNil
+ where
+  hOccursOpt HNil = Nothing
+
+instance HOccursOpt e (HCons e l)
+ where
+  hOccursOpt (HCons e _) = Just e
+
+instance HOccursOpt e l
+      => HOccursOpt e (HCons e' l)
+ where
+  hOccursOpt (HCons _ l) = hOccursOpt l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Class to test that a type is "free" in a type sequence
+
+data TypeFound e
+class HOccursNot e l
+instance HOccursNot e HNil
+instance Fail (TypeFound e) => HOccursNot e (HCons e l)
+instance HOccursNot e l => HOccursNot e (HCons e' l)
+
+
+{-----------------------------------------------------------------------------}
+
+class HProject l l'
+ where
+  hProject :: l -> l'
+
+instance HProject l HNil
+ where
+  hProject _ = HNil
+
+instance ( HList l'
+         , HOccurs e l
+         , HProject l l'
+         )
+      =>   HProject l (HCons e l')
+ where
+  hProject l = HCons (hOccurs l) (hProject l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Illustration of typical test scenarios
+
+{-
+
+Retrieve the Breed of an animal.
+
+ghci-or-hugs> hOccurs myAnimal :: Breed
+Cow
+
+-}
+
+{-
+
+Normal hOccurs requires specification of the result type even if the result
+type is determined by the fact that we are faced with a singleton list.
+
+ghci-or-hugs> hOccurs (HCons 1 HNil)
+
+<interactive>:1:
+    No instance for (HOccurs e1 (HCons e HNil))
+
+-}
+
+{-
+
+However, hOccurs can be elaborated as improved as follows:
+
+ghci-or-hugs> hLookup (HCons 1 HNil)
+1
+
+-}
+
+{-----------------------------------------------------------------------------}
diff --git a/Data/HList/HTypeIndexed.hs b/Data/HList/HTypeIndexed.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/HTypeIndexed.hs
@@ -0,0 +1,124 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
+  UndecidableInstances, FlexibleContexts #-}
+
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Type-indexed operations on typeful heterogeneous lists.
+-}
+
+module Data.HList.HTypeIndexed where
+
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+import Data.HList.HArray
+import Data.HList.HOccurs
+
+
+{-----------------------------------------------------------------------------}
+
+class HDeleteMany e l l' | e l -> l'
+ where
+  hDeleteMany :: Proxy e -> l -> l'
+
+instance HDeleteMany e HNil HNil
+ where
+  hDeleteMany _ HNil = HNil
+
+instance ( HList l
+         , TypeEq e e' b
+         , HDeleteManyCase b e e' l l'
+         )
+      =>   HDeleteMany e (HCons e' l) l'
+ where
+  hDeleteMany p (HCons e' l) = l'
+   where
+    b  = proxyEq p (toProxy e')
+    l' = hDeleteManyCase b p e' l
+
+class HDeleteManyCase b e e' l l' | b e e' l -> l'
+ where
+  hDeleteManyCase :: b -> Proxy e -> e' -> l -> l'
+
+instance HDeleteMany e l l'
+      => HDeleteManyCase HTrue e e l l'
+ where
+  hDeleteManyCase _ p _ l = hDeleteMany p l
+
+
+instance HDeleteMany e l l'
+      => HDeleteManyCase HFalse e e' l (HCons e' l')
+ where
+  hDeleteManyCase _ p e' l = HCons e' (hDeleteMany p l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Map a type to a natural
+
+class HNat n => HType2HNat e l n | e l -> n
+instance (TypeEq e' e b, HType2HNatCase b e l n)
+      =>  HType2HNat e (HCons e' l) n
+
+-- Helper class
+
+class (HBool b, HNat n) => HType2HNatCase b e l n | b e l -> n
+instance HOccursNot e l => HType2HNatCase HTrue e l HZero
+instance HType2HNat e l n => HType2HNatCase HFalse e l (HSucc n)
+
+hType2HNat :: HType2HNat e l n => Proxy e -> l -> n
+hType2HNat _ _ = undefined
+
+
+
+-- Map types to naturals
+
+class HTypes2HNats ps l ns | ps l -> ns
+ where
+  hTypes2HNats :: ps -> l -> ns
+
+instance HTypes2HNats HNil l HNil
+ where
+  hTypes2HNats _ _ = HNil
+
+instance ( HType2HNat   e l n
+         , HTypes2HNats ps l ns
+         )
+      =>   HTypes2HNats (HCons (Proxy e) ps) l (HCons n ns)
+ where
+  hTypes2HNats (HCons p ps) l = HCons (hType2HNat p l) (hTypes2HNats ps l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Define type-indexed delete in terms of the natural-based primitive
+hDeleteAtProxy :: (HDeleteAtHNat n l l', HType2HNat e l n) => Proxy e -> l -> l'
+hDeleteAtProxy p l = hDeleteAtHNat (hType2HNat p l) l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Define type-indexed update in terms of the natural-based update
+hUpdateAtType :: (HUpdateAtHNat n e l l', HType2HNat e l n) => e -> l -> l'
+hUpdateAtType e l = hUpdateAtHNat (hType2HNat (toProxy e) l) e l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Projection based on proxies
+hProjectByProxies :: (HProjectByHNats ns l l', HTypes2HNats ps l ns) => ps -> l -> l'
+hProjectByProxies ps l = hProjectByHNats (hTypes2HNats ps l) l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Splitting based on proxies
+hSplitByProxies :: (HMap (HAddTag HTrue) l l', HSplitByHNats' ns l' l'1 l'',
+                   HTypes2HNats ps l ns) =>
+                  ps -> l -> (l'1, l'')
+hSplitByProxies ps l = hSplitByHNats (hTypes2HNats ps l) l
+
+
+{-----------------------------------------------------------------------------}
diff --git a/Data/HList/HZip.hs b/Data/HList/HZip.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/HZip.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
+
+module Data.HList.HZip where
+
+import Data.HList.HListPrelude
+
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Zipping and unzipping for (conceptually) lists of pairs.
+ -}
+
+{-----------------------------------------------------------------------------}
+
+-- Test for zippability
+
+class HZippable x y
+instance HZippable HNil HNil
+instance HZippable l l' => HZippable (HCons e l) (HCons e' l')
+
+
+{-----------------------------------------------------------------------------}
+
+-- Zip and unzip
+
+class HZip x y l | x y -> l, l -> x y
+ where
+  hZip   :: x -> y -> l
+  hUnzip :: l -> (x,y)
+
+{-
+
+-- Zipping version I
+-- Somehow too polymorphic.
+-- Version II specialises for HNil and HCons.
+
+instance HZippable x y => HZip x y (x,y)
+ where
+  hZip x y = (x,y)
+  hUnzip = id
+
+-}
+
+{-
+
+-- Zipping version II
+-- Built-in show and alias-based type construction inconvenient.
+-- Version III goes for a true list of pairs.
+
+instance HZip HNil HNil (HNil,HNil)
+ where
+  hZip x y = (x,y)
+  hUnzip = id
+
+instance HZip xt yt zt
+      => HZip (HCons xh xt) (HCons yh yt) (HCons xh xt,HCons yh yt)
+ where
+  hZip x y = (x,y)
+  hUnzip = id
+
+-}
+
+
+-- {-
+
+--- Zipping version III
+--- Works best for us.
+
+instance HZip HNil HNil HNil
+ where
+  hZip HNil HNil = HNil
+  hUnzip HNil = (HNil,HNil)
+
+instance HZip tx ty l
+      => HZip (HCons hx tx) (HCons hy ty) (HCons (hx,hy) l)
+ where
+  hZip (HCons hx tx) (HCons hy ty) = HCons (hx,hy) (hZip tx ty)
+  hUnzip (HCons (hx,hy) l) = (HCons hx tx, HCons hy ty)
+   where
+    (tx,ty) = hUnzip l
+
+-- -}
diff --git a/Data/HList/Label4.hs b/Data/HList/Label4.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/Label4.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, EmptyDataDecls #-}
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Yet another model of labels.
+   Labels are type proxies.
+-}
+
+module Data.HList.Label4 where
+
+import Data.Typeable
+import Data.Char
+
+import Data.HList.FakePrelude
+import Data.HList.Record
+
+
+-- Equality on labels
+
+instance TypeEq x y b => HEq (Proxy x) (Proxy y) b
+
+
+-- Show label
+
+instance Typeable x => ShowLabel (Proxy x)
+ where
+  showLabel = (\(x:xs) -> toLower x:xs)
+            . reverse
+            . takeWhile (not . (==) '.')
+            . reverse
+            . show
+{-
+            . tyConString
+            . typeRepTyCon
+-}
+            . typeOf
+            . unProxy
diff --git a/Data/HList/Record.hs b/Data/HList/Record.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/Record.hs
@@ -0,0 +1,394 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
+  FlexibleContexts, UndecidableInstances #-}
+{-# OPTIONS -fglasgow-exts #-}
+
+{-
+   The HList library
+
+   (C) 2004-2006, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Extensible records
+
+   The are different models of labels that go with this module;
+   see the files Label?.hs.
+-}
+
+module Data.HList.Record where
+
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+import Data.HList.HArray
+
+
+{-----------------------------------------------------------------------------}
+
+-- Record types as label-value pairs, where label is purely phantom.
+-- Thus the run-time representation of a field is the same as that of
+-- its value, and the record, at run-time, is indistinguishable from
+-- the HList of field values. At run-time, all information about the
+-- labels is erased.
+
+-- Field of label l with value type v
+newtype LVPair l v = LVPair { valueLVPair :: v }
+
+-- Label accessor
+labelLVPair :: LVPair l v -> l
+labelLVPair = undefined
+
+newLVPair :: l -> v -> LVPair l v
+newLVPair _ = LVPair
+
+newtype Record r = Record r
+
+
+-- Build a record
+mkRecord :: HRLabelSet r => r -> Record r
+mkRecord = Record
+
+
+-- Build an empty record
+emptyRecord :: Record HNil
+emptyRecord = mkRecord HNil
+
+
+-- Propery of a proper label set for a record: no duplication of labels
+
+class HRLabelSet ps
+instance HRLabelSet HNil
+instance HRLabelSet (HCons x HNil)
+instance ( HEq l1 l2 HFalse
+         , HRLabelSet (HCons (LVPair l2 v2) r)
+         , HRLabelSet (HCons (LVPair l1 v1) r)
+         ) => HRLabelSet (HCons (LVPair l1 v1) (HCons (LVPair l2 v2) r))
+
+{-
+instance (HZip ls vs ps, HLabelSet ls) => HRLabelSet ps
+-}
+
+class HLabelSet ls
+instance HLabelSet HNil
+instance (HMember x ls HFalse, HLabelSet ls)
+      =>  HLabelSet (HCons x ls)
+
+
+-- Construct the (phantom) list of labels of the record.
+-- This is a type-level only function
+class RecordLabels r ls | r -> ls
+instance RecordLabels HNil HNil
+instance RecordLabels r' ls
+      => RecordLabels (HCons (LVPair l v) r') (HCons l ls)
+
+recordLabels :: RecordLabels r ls => r -> ls
+recordLabels = undefined
+
+
+{-----------------------------------------------------------------------------}
+
+-- A Show instance to appeal to normal records
+
+instance ShowComponents r => Show (Record r)
+ where
+  show (Record r) =  "Record{"
+                  ++ showComponents "" r
+                  ++ "}"
+
+class ShowComponents l
+ where
+  showComponents :: String -> l -> String
+
+instance ShowComponents HNil
+ where
+  showComponents _ HNil = ""
+
+instance ( ShowLabel l
+         , Show v
+         , ShowComponents r
+         )
+      =>   ShowComponents (HCons (LVPair l v) r)
+ where
+  showComponents comma (HCons f@(LVPair v) r)
+     =  comma
+     ++ showLabel (labelLVPair f)
+     ++ "="
+     ++ show v
+     ++ showComponents "," r
+
+class ShowLabel l
+ where
+  showLabel :: l -> String
+
+
+{-----------------------------------------------------------------------------}
+
+-- Extension for records
+
+instance HRLabelSet (HCons (LVPair l v) r)
+    => HExtend (LVPair l v) (Record r) (Record (HCons (LVPair l v) r))
+ where
+  hExtend f (Record r) = mkRecord (HCons f r)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Record concatenation
+
+instance ( HRLabelSet r''
+         , HAppend r r' r''
+         )
+    => HAppend (Record r) (Record r') (Record r'')
+ where
+  hAppend (Record r) (Record r') = mkRecord (hAppend r r')
+
+
+{-----------------------------------------------------------------------------}
+
+-- Lookup operation
+
+-- This is a baseline implementation.
+-- We use a helper class, HasField, to abstract from the implementation.
+
+class HasField l r v | l r -> v
+  where
+    hLookupByLabel:: l -> r -> v
+
+{-
+instance ( RecordLabels r ls
+         , HFind l ls n
+         , HLookupByHNat n r (LVPair l v)
+         ) => HasField l (Record r) v
+  where
+    hLookupByLabel l (Record r) = v
+      where
+        ls = recordLabels r
+        n = hFind l ls
+        (LVPair v) = hLookupByHNat n r
+
+-}
+
+
+-- Because hLookupByLabel is so frequent and important, we implement
+-- it separately, more efficiently. The algorithm is familiar assq, only
+-- the comparison operation is done at compile-time
+
+instance HasField l r v => HasField l (Record r) v where
+    hLookupByLabel l (Record r) = hLookupByLabel l r
+
+class HasField' b l r v | b l r -> v where
+    hLookupByLabel':: b -> l -> r -> v
+
+instance (HEq l l' b, HasField' b l (HCons (LVPair l' v') r) v)
+    => HasField l (HCons (LVPair l' v') r) v where
+    hLookupByLabel l r@(HCons f' _) =
+             hLookupByLabel' (hEq l (labelLVPair f')) l r
+
+instance HasField' HTrue l (HCons (LVPair l v) r) v where
+    hLookupByLabel' _ _ (HCons (LVPair v) _) = v
+instance HasField l r v => HasField' HFalse l (HCons fld r) v where
+    hLookupByLabel' _ l (HCons _ r) = hLookupByLabel l r
+
+
+
+{-----------------------------------------------------------------------------}
+
+-- Delete operation
+hDeleteAtLabel :: (H2ProjectByLabels (HCons e HNil) t t1 t2) => e -> Record t -> Record t2
+hDeleteAtLabel l (Record r) = Record r'
+ where
+  (_,r')  = h2projectByLabels (HCons l HNil) r
+
+
+{-----------------------------------------------------------------------------}
+
+-- Update operation
+hUpdateAtLabel ::( RecordLabels t ls, HFind e ls n, HUpdateAtHNat n (LVPair e v) t l') =>
+                e -> v -> Record t -> Record l'
+hUpdateAtLabel l v (Record r) = Record r'
+ where
+  n    = hFind l (recordLabels r)
+  r'   = hUpdateAtHNat n (newLVPair l v) r
+
+
+{-----------------------------------------------------------------------------}
+-- Projection for records
+-- It is also an important operation: the basis of many
+-- deconstructors -- so we try to implement it efficiently.
+hProjectByLabels :: (HRLabelSet a, H2ProjectByLabels ls t a b) => ls -> Record t -> Record a
+hProjectByLabels ls (Record r) = mkRecord (fst $ h2projectByLabels ls r)
+
+hProjectByLabels2 :: (HRLabelSet t2, HRLabelSet t1, H2ProjectByLabels ls t t1 t2) =>
+                                                 ls -> Record t -> (Record t1, Record t2)
+hProjectByLabels2 ls (Record r) = (mkRecord rin, mkRecord rout)
+   where (rin,rout) = h2projectByLabels ls r
+
+-- Invariant: r = rin `disjoint-union` rout
+--            labels(rin) = ls
+class H2ProjectByLabels ls r rin rout | ls r -> rin rout where
+    h2projectByLabels :: ls -> r -> (rin,rout)
+
+instance H2ProjectByLabels HNil r HNil r where
+    h2projectByLabels _ r = (HNil,r)
+
+instance H2ProjectByLabels (HCons l ls) HNil HNil HNil where
+    h2projectByLabels _ _ = (HNil,HNil)
+
+instance (HMemberM l' (HCons l ls) b,
+          H2ProjectByLabels' b (HCons l ls) (HCons (LVPair l' v') r') rin rout)
+    => H2ProjectByLabels (HCons l ls) (HCons (LVPair l' v') r') rin rout where
+    -- h2projectByLabels = h2projectByLabels' (undefined::b)
+    -- The latter is solely for the Hugs benefit
+    h2projectByLabels ls r@(HCons _ _) =h2projectByLabels' (undefined::b) ls r
+      -- where b = hMember (labelLVPair f') ls
+
+class H2ProjectByLabels' b ls r rin rout | b ls r -> rin rout where
+    h2projectByLabels' :: b -> ls -> r -> (rin,rout)
+
+instance H2ProjectByLabels ls' r' rin rout =>
+    H2ProjectByLabels' (HJust ls') ls (HCons f' r') (HCons f' rin) rout where
+    h2projectByLabels' _ _ (HCons x r) = (HCons x rin, rout)
+        where (rin,rout) = h2projectByLabels (undefined::ls') r
+
+instance H2ProjectByLabels ls r' rin rout =>
+    H2ProjectByLabels' HNothing ls (HCons f' r') rin (HCons f' rout) where
+    h2projectByLabels' _ ls (HCons x r) = (rin, HCons x rout)
+        where (rin,rout) = h2projectByLabels ls r
+
+
+{-----------------------------------------------------------------------------}
+
+-- Rename the label of record
+hRenameLabel :: (H2ProjectByLabels (HCons e HNil) t t1 t2, HasField e t v,
+                HRLabelSet (HCons (LVPair l v) t2)) =>
+               e -> l -> Record t -> Record (HCons (LVPair l v) t2)
+hRenameLabel l l' r = r''
+ where
+  v   = hLookupByLabel l r
+  r'  = hDeleteAtLabel l r
+  r'' = hExtend (newLVPair l' v) r'
+
+
+{-----------------------------------------------------------------------------}
+
+-- A variation on update: type-preserving update.
+hTPupdateAtLabel :: (HUpdateAtHNat n (LVPair l a) t l', HFind l ls n, RecordLabels t ls,
+                    HasField l t a) =>
+                   l -> a -> Record t -> Record l'
+hTPupdateAtLabel l v r = hUpdateAtLabel l v r
+ where
+   te :: a -> a -> ()
+   te _ _ = ()
+   _ = te v (hLookupByLabel l r)
+
+{-
+
+-- We could also say:
+
+hTPupdateAtLabel l v r = hUpdateAtLabel l v r `asTypeOf` r
+
+-- Then we were taking a dependency on Haskell's type equivalence.
+-- This would also constrain the actual implementation of hUpdateAtLabel.
+
+-}
+
+{-----------------------------------------------------------------------------}
+
+-- Subtyping for records
+
+instance ( RecordLabels r' ls
+         , H2ProjectByLabels ls r r' rout
+         )
+    => SubType (Record r) (Record r')
+
+
+{-----------------------------------------------------------------------------}
+
+class  HLeftUnion r r' r'' | r r' -> r''
+ where hLeftUnion :: r -> r' -> r''
+
+instance HLeftUnion r (Record HNil) r
+ where   hLeftUnion r _ = r
+
+instance ( RecordLabels r ls
+         , HMember l ls b
+         , HLeftUnionBool b r (LVPair l v) r'''
+         , HLeftUnion (Record r''') (Record r') r''
+         )
+           => HLeftUnion (Record r) (Record (HCons (LVPair l v) r')) r''
+  where
+   hLeftUnion (Record r) (Record (HCons f r')) = r''
+    where
+     b       = hMember (labelLVPair f) (recordLabels r)
+     r'''    = hLeftUnionBool b r f
+     r''     = hLeftUnion (Record r''') (Record r')
+
+class  HLeftUnionBool b r f r' | b r f -> r'
+ where hLeftUnionBool :: b -> r -> f -> r'
+
+instance HLeftUnionBool HTrue r f r
+   where hLeftUnionBool _ r _  = r
+
+instance HLeftUnionBool HFalse r f (HCons f r)
+   where hLeftUnionBool _ r f = HCons f r
+
+
+{-----------------------------------------------------------------------------}
+-- Compute the symmetric union of two records r1 and r2 and
+-- return the pair of records injected into the union (ru1, ru2).
+-- To be more precise, we compute the symmetric union _type_ ru
+-- of two record _types_ r1 and r2. The emphasis on types is important.
+-- The two records (ru1,ru2) in the result of unionSR have the same
+-- type ru, but they are generally different values.
+-- Here the simple example: suppose
+--   r1 = (Label .=. True)  .*. emptyRecord
+--   r2 = (Label .=. False) .*. emptyRecord
+-- Then unionSR r1 r2 will return (r1,r2). Both components of the result
+-- are different records of the same type.
+
+-- To project from the union ru, use hProjectByLabels.
+-- It is possible to project from the union obtaining a record
+-- that was not used at all when creating the union.
+-- We do assure however that if (unionSR r1 r2) gave (r1u,r2u),
+-- then projecting r1u onto the type of r1 gives the _value_ identical
+-- to r1. Ditto for r2.
+
+class UnionSymRec r1 r2 ru | r1 r2 -> ru where
+    unionSR :: r1 -> r2 -> (ru, ru)
+
+instance UnionSymRec r1 (Record HNil) r1 where
+    unionSR r1 _ = (r1, r1)
+
+instance ( RecordLabels r1 ls
+         , HMember l ls b
+         , UnionSymRec' b (Record r1) (LVPair l v) (Record r2') ru
+         )
+    => UnionSymRec (Record r1) (Record (HCons (LVPair l v) r2')) ru
+    where
+    unionSR r1 (Record (HCons f r2')) =
+        unionSR' (undefined::b) r1 f (Record r2')
+
+class UnionSymRec' b r1 f2 r2' ru | b r1 f2 r2' -> ru where
+    unionSR' :: b -> r1 -> f2 -> r2'  -> (ru, ru)
+
+-- Field f2 is already in r1, so it will be in the union of r1
+-- with the rest of r2.
+-- To inject (HCons f2 r2) in that union, we should replace the
+-- field f2
+instance (UnionSymRec r1 r2' (Record ru),
+          HasField l2 ru v2,
+          HUpdateAtHNat n (LVPair l2 v2) ru ru,
+          RecordLabels ru ls,
+          HFind l2 ls n)
+    => UnionSymRec' HTrue r1 (LVPair l2 v2) r2' (Record ru) where
+    unionSR' _ r1 (LVPair v2) r2' = (ul, ur')
+       where (ul,ur) = unionSR r1 r2'
+             ur' = hTPupdateAtLabel (undefined::l2) v2 ur
+
+
+instance (UnionSymRec r1 r2' (Record ru),
+          HExtend f2 (Record ru) (Record (HCons f2 ru)))
+    => UnionSymRec' HFalse r1 f2 r2' (Record (HCons f2 ru)) where
+    unionSR' _ r1 f2 r2' = (ul', ur')
+       where (ul,ur) = unionSR r1 r2'
+             ul' = hExtend f2 ul
+             ur' = hExtend f2 ur
+
+
diff --git a/Data/HList/TIC.hs b/Data/HList/TIC.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/TIC.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
+
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Type-indexed co-products.
+-}
+
+module Data.HList.TIC where
+
+import Data.Dynamic
+
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+import Data.HList.HOccurs
+import Data.HList.TIP
+
+
+{-----------------------------------------------------------------------------}
+
+-- A datatype for type-indexed co-products
+
+data TIC l = TIC Dynamic
+
+
+{-----------------------------------------------------------------------------}
+
+-- Public constructor
+
+mkTIC :: ( HTypeIndexed l
+         , HTypeProxied l
+         , HOccurs (Proxy i) l
+         , Typeable i
+         )
+      => i -> TIC l
+
+mkTIC i = TIC (toDyn i)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Public destructor
+
+unTIC :: ( HTypeIndexed l
+         , HTypeProxied l
+         , HOccurs (Proxy o) l
+         , Typeable o
+         )
+      => TIC l -> Maybe o
+
+unTIC (TIC i) = fromDynamic i
+
+
+{-----------------------------------------------------------------------------}
+
+-- A type-indexed type sequence that is a sequence of proxy types
+
+class HTypeProxied l
+instance HTypeProxied HNil
+instance HTypeProxied l => HTypeProxied (HCons (Proxy e) l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- TICs are opaque
+
+instance Show (TIC l)
+ where
+  show _ = "<Cannot show TIC content!>"
+
+
+{-----------------------------------------------------------------------------}
diff --git a/Data/HList/TIP.hs b/Data/HList/TIP.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/TIP.hs
@@ -0,0 +1,254 @@
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances #-}
+module Data.HList.TIP where
+
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Type-indexed products.
+-}
+
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+import Data.HList.HArray
+import Data.HList.HOccurs
+import Data.HList.HTypeIndexed
+
+
+{-----------------------------------------------------------------------------}
+
+-- The newtype for type-indexed products
+
+newtype TIP l = TIP l
+        deriving (Read,Show)
+
+mkTIP :: HTypeIndexed l => l -> TIP l
+mkTIP = TIP
+
+unTIP :: TIP l -> l
+unTIP (TIP l) = l
+
+emptyTIP :: TIP HNil
+emptyTIP = mkTIP HNil
+
+
+
+{-----------------------------------------------------------------------------}
+
+-- Type-indexed type sequences
+
+class HList l => HTypeIndexed l
+instance HTypeIndexed HNil
+instance (HOccursNot e l,HTypeIndexed l) => HTypeIndexed (HCons e l)
+
+
+{-----------------------------------------------------------------------------}
+
+--
+-- One occurrence and nothing is left
+--
+-- This variation provides an extra feature for singleton lists.
+-- That is, the result type is unified with the element in the list.
+-- Hence the explicit provision of a result type can be omitted.
+--
+
+instance TypeCast e' e => HOccurs e (TIP (HCons e' HNil))
+ where
+  hOccurs (TIP (HCons e' _)) = typeCast e'
+
+instance HOccurs e (HCons x (HCons y l))
+      => HOccurs e (TIP (HCons x (HCons y l)))
+ where
+  hOccurs (TIP l) = hOccurs l
+
+
+{-----------------------------------------------------------------------------}
+
+-- HOccursNot lifted to TIPs
+
+instance HOccursNot e l => HOccursNot e (TIP l)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Type-indexed extension
+hExtend' :: (HTypeIndexed t, HOccursNot e t) => e -> TIP t -> TIP (HCons e t)
+hExtend' e (TIP l) = mkTIP (HCons e l)
+
+{-
+
+Valid type I
+
+hExtend' :: (HTypeIndexed l, HOccursNot e l)
+         => e -> TIP l -> TIP (HCons e l)
+
+Valid type II
+
+*TIP> :t hExtend'
+hExtend' :: forall l e.
+            (HTypeIndexed (HCons e l)) =>
+            e -> TIP l -> TIP (HCons e l)
+
+-}
+
+
+{-----------------------------------------------------------------------------}
+
+-- Lift extension through HExtend
+
+instance ( HOccursNot e l
+         , HTypeIndexed l
+         )
+      => HExtend e (TIP l) (TIP (HCons e l))
+ where
+  hExtend = hExtend'
+
+
+{-----------------------------------------------------------------------------}
+
+-- Lifting previous operations
+
+
+instance ( HAppend l l' l''
+         , HTypeIndexed l''
+         )
+           => HAppend (TIP l) (TIP l') (TIP l'')
+ where
+  hAppend (TIP l) (TIP l') = mkTIP (hAppend l l')
+
+
+instance HOccursMany e l
+      => HOccursMany e (TIP l)
+ where
+  hOccursMany = hOccursMany . unTIP
+
+
+instance HOccursMany1 e l
+      => HOccursMany1 e (TIP l)
+ where
+  hOccursMany1 = hOccursMany1 . unTIP
+
+
+instance HOccursFst e l
+      => HOccursFst e (TIP l)
+ where
+  hOccursFst = hOccursFst . unTIP
+
+
+instance HOccursOpt e l
+      => HOccursOpt e (TIP l)
+ where
+  hOccursOpt = hOccursOpt . unTIP
+
+
+{-----------------------------------------------------------------------------}
+
+-- Shielding type-indexed operations
+
+onTIP :: HTypeIndexed a => (b -> a) -> TIP b -> TIP a
+onTIP f (TIP l) = mkTIP (f l)
+
+tipyDelete :: (HTypeIndexed l',HType2HNat e b n,HDeleteAtHNat n b l') => Proxy e -> TIP b -> TIP l'
+tipyDelete  p t  = onTIP (hDeleteAtProxy p) t
+tipyUpdate :: (HTypeIndexed l',HType2HNat e b n,HUpdateAtHNat n e b l') => e -> TIP b -> TIP l'
+tipyUpdate  e t  = onTIP (hUpdateAtType e) t
+tipyProject :: (HTypeIndexed l',HTypes2HNats ps b ns,HProjectByHNats ns b l') => ps -> TIP b -> TIP l'
+tipyProject ps t = onTIP (hProjectByProxies ps) t
+
+
+-- Split produces two TIPs
+tipySplit :: (HTypeIndexed t2,HTypeIndexed t1,HTypes2HNats ps t ns,HSplitByHNats' ns l' t1 t2,
+             HMap (HAddTag HTrue) t l') =>
+            ps -> TIP t -> (TIP t1, TIP t2)
+tipySplit ps (TIP l) = (mkTIP l',mkTIP l'')
+ where
+  (l',l'') = hSplitByProxies ps l
+
+
+{-----------------------------------------------------------------------------}
+
+-- Subtyping for TIPs
+
+instance SubType (TIP l) (TIP HNil)
+instance (HOccurs e l, SubType (TIP l) (TIP l'))
+      =>  SubType (TIP l) (TIP (HCons e l'))
+
+
+{-----------------------------------------------------------------------------}
+
+-- Sample code
+
+{-
+
+Assume
+
+myTipyCow = TIP myAnimal
+
+animalKey :: (HOccurs Key l, SubType l (TIP Animal)) => l -> Key
+animalKey = hOccurs
+
+Session log
+
+*TIP> :t myTipyCow
+myTipyCow :: TIP Animal
+
+*TIP> hOccurs myTipyCow :: Breed
+Cow
+
+*TIP> hExtend BSE myTipyCow
+TIP (HCons BSE
+    (HCons (Key 42)
+    (HCons (Name "Angus")
+    (HCons Cow
+    (HCons (Price 75.5)
+     HNil)))))
+
+*TIP> BSE .*. myTipyCow
+--- same as before ---
+
+*TIP> Sheep .*. myTipyCow
+Type error ...
+
+*TIP> Sheep .*. tipyDelete myTipyCow (HProxy::HProxy Breed)
+TIP (HCons Sheep (HCons (Key 42) (HCons (Name "Angus") (HCons (Price 75.5) HNil))))
+
+*TIP> tipyUpdate myTipyCow Sheep
+TIP (HCons (Key 42) (HCons (Name "Angus") (HCons Sheep (HCons (Price 75.5) HNil))))
+
+-}
+
+{-----------------------------------------------------------------------------}
+
+-- This example from the TIR paper challenges singleton lists.
+-- Thanks to the HW 2004 reviewer who pointed out the value of this example.
+-- We note that the explicit type below is richer than the inferred type.
+-- This richer type is needed for making this operation more polymorphic.
+-- That is, a) would not work without the explicit type, while it would:
+--  a)  ((+) (1::Int)) $ snd $ tuple oneTrue
+--  b)  ((+) (1::Int)) $ fst $ tuple oneTrue
+
+tuple :: ( HOccurs e1 (TIP l)
+         , HType2HNat e1 l n
+         , HDeleteAtHNat n l l'
+         , HOccurs e2 (TIP l')
+         , HOccurs e2 (TIP l)
+         , HType2HNat e2 l n'
+         , HDeleteAtHNat n' l l''
+         , HOccurs e1 (TIP l'')
+         ) =>
+              TIP l -> (e1, e2)
+
+tuple (TIP l) = let
+                 x  = hOccurs (TIP l)
+                 l' = hDeleteAtProxy (toProxy x) l
+                 y  = hOccurs (TIP l')
+                in (x,y)
+
+
+-- A specific tuple
+oneTrue :: TIP (HCons Int (HCons Bool HNil))
+oneTrue = hExtend (1::Int) (hExtend True emptyTIP)
+
+
+{-----------------------------------------------------------------------------}
diff --git a/Data/HList/TypeCastGeneric1.hs b/Data/HList/TypeCastGeneric1.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/TypeCastGeneric1.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}
+
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   A generic implementation of type cast. For this implementation to
+   work, we need to import it at a higher level in the module hierarchy
+   than all clients of the class. Otherwise, type simplification will
+   inline TypeCast x y, which implies compile-time unification of x and y.
+
+   This technique works fine for ghc, and within limits for hugs.
+-}
+
+module Data.HList.TypeCastGeneric1 where
+
+import Data.HList.FakePrelude
+
+instance TypeCast x x
+ where
+  typeCast = id
diff --git a/Data/HList/TypeEqBoolGeneric.hs b/Data/HList/TypeEqBoolGeneric.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/TypeEqBoolGeneric.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Generic implementations of type equality and disequality
+-}
+
+module Data.HList.TypeEqBoolGeneric where
+
+import Data.HList.FakePrelude
+
+instance            TypeEqTrue  x x
+instance Fail () => TypeEqFalse x x
+instance            TypeEqFalse x y
diff --git a/Data/HList/TypeEqGeneric1.hs b/Data/HList/TypeEqGeneric1.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/TypeEqGeneric1.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
+  FlexibleContexts, UndecidableInstances #-}
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   A generic implementation of a type equality predicate. The given
+   implementation only works for GHC. It relies on two properties
+   of GHC instance selection: (i) selection is lazy, and the negation
+   of the constraints of the more specific instance is assumed for
+   the more general instance.
+
+   The specific encoding given here makes use of TypeCast,
+   and by transitive closure therefore relies on separate compilation
+   of TypeCast clients and the TypeCast instance.
+
+   There is another encoding in TypeEqGeneric2.hs.
+-}
+
+module Data.HList.TypeEqGeneric1 where
+
+import Data.HList.FakePrelude
+
+instance TypeEq x x HTrue
+instance (HBool b, TypeCast HFalse b) => TypeEq x y b
+-- instance TypeEq x y HFalse -- would violate functional dependency
+
+
+class HBool b => TupleType t b | t -> b
+instance TupleType () HTrue
+instance TupleType (x,y) HTrue
+instance TupleType (x,y,z) HTrue
+-- Continue for a while
+instance (HBool b, TypeCast HFalse b) => TupleType x b
+-- instance TupleType x HFalse -- would violate functional dependency
diff --git a/Data/HList/Variant.hs b/Data/HList/Variant.hs
new file mode 100644
--- /dev/null
+++ b/Data/HList/Variant.hs
@@ -0,0 +1,98 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
+  UndecidableInstances, FlexibleContexts #-}
+
+{-
+   The HList library
+
+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke
+
+   Variants, i.e., labelled sums.
+
+   One approach to their implementation would be to consider both
+   the favoured label and the corresponding value as dynamics upon
+   variant construction. Since we are too lazy to programme some
+   Typeable instances for non-ghc systems (NB: in GHC, Typeable
+   is derivable), we rather model variants as (opaque) records
+   with maybies for the values. Only one value will actually hold
+   non-Nothing, as guaranteed by the constructor.
+
+   See VariantP.hs for a different approach to open sums.
+-}
+
+module Data.HList.Variant where
+
+import Data.HList.FakePrelude
+import Data.HList.HListPrelude
+import Data.HList.HArray
+import Data.HList.Record
+
+
+{-----------------------------------------------------------------------------}
+
+-- Variant types on the basis of label-maybe pairs.
+
+newtype Variant mr = Variant mr
+
+
+{-----------------------------------------------------------------------------}
+
+-- Turn proxy sequence into sequence of Nothings
+
+class HMaybied r r' | r -> r'
+ where
+  hMaybied :: r -> r'
+
+instance HMaybied HNil HNil
+ where
+  hMaybied _ = HNil
+
+instance HMaybied r r'
+      => HMaybied (HCons (LVPair l (Proxy v)) r) (HCons (LVPair l (Maybe v)) r')
+ where
+  hMaybied (HCons _ r) = HCons (LVPair Nothing) (hMaybied r)
+
+
+{-----------------------------------------------------------------------------}
+
+-- Public constructor
+
+mkVariant :: ( RecordLabels v ls
+             , HFind x ls n
+             , HMaybied v v'
+             , HUpdateAtHNat n (LVPair x (Maybe y)) v' v'
+             )
+          => x -> y -> (Record v) -> Variant v'
+
+mkVariant x y (Record v) = Variant v'
+ where
+  n       = hFind x (recordLabels v)
+  ms      = hMaybied v
+  v'      = hUpdateAtHNat n (newLVPair x (Just y)) ms
+
+
+{-----------------------------------------------------------------------------}
+
+-- Public destructor
+
+unVariant :: ( RecordLabels v ls
+             , HFind x ls n
+             , HLookupByHNat n v (LVPair x (Maybe y))
+             )
+          => x -> Variant v -> Maybe y
+
+unVariant x (Variant v) = y
+ where
+  n       = hFind x (recordLabels v)
+  LVPair y     = hLookupByHNat n v
+
+
+{-----------------------------------------------------------------------------}
+
+-- Variants are opaque
+
+instance Show (Variant v)
+ where
+  show _ = "<Cannot show Variant content!>"
+
+
+{-----------------------------------------------------------------------------}
diff --git a/HList.cabal b/HList.cabal
new file mode 100644
--- /dev/null
+++ b/HList.cabal
@@ -0,0 +1,26 @@
+Name:                HList
+Version:             0.1
+Category:            Data
+Synopsis:            Heterogeneous lists
+Description:         HList is a record system providing strongly typed heterogenous lists, records,
+                     type-indexed products (TIP) and co-products; licensed under the MIT X License.
+License:             OtherLicense
+License-File:        LICENSE
+Author:              2004 Oleg Kiselyov (FNMOC, Monterey), Ralf Laemmel (CWI/VU, Amsterdam),
+                     Keean Schupke (Imperial College, London)
+Maintainer:          oleg@pobox.com
+
+Tested-With:         GHC==6.8.2
+Build-Depends:       base
+Build-Type:          Simple
+Exposed-modules:     Data.HList
+Other-modules:       Data.HList.Label4, Data.HList.CommonMain, Data.HList.Variant, Data.HList.GhcSyntax,
+                     Data.HList.GhcRecord, Data.HList.Record, Data.HList.HZip, Data.HList.TIC, Data.HList.TIP,
+                     Data.HList.HTypeIndexed, Data.HList.HOccurs, Data.HList.HArray, Data.HList.GhcExperiments,
+                     Data.HList.HListPrelude, Data.HList.TypeEqBoolGeneric, Data.HList.TypeEqGeneric1,
+                     Data.HList.TypeCastGeneric1, Data.HList.FakePrelude
+
+extensions:          EmptyDataDecls, FlexibleContexts, FlexibleInstances, FunctionalDependencies,
+                     MultiParamTypeClasses, OverlappingInstances, PatternSignatures, RankNTypes,
+                     ScopedTypeVariables, TypeSynonymInstances, UndecidableInstances
+ghc-options:         -O2 -Wall
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2004 Oleg Kiselyov (FNMOC, Monterey), Ralf Laemmel (CWI/VU, Amsterdam), Keean Schupke (Imperial College, London)
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be
+included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+import Distribution.Simple
+main = defaultMainWithHooks defaultUserHooks