diff --git a/CHANGELOG b/CHANGELOG
new file mode 100644
--- /dev/null
+++ b/CHANGELOG
@@ -0,0 +1,8 @@
+
+1.2 -> 1.2.1
+- Renamed Data.Type.HList to Data.Type.RList
+- Now using DataKinds to represent right-lists of types
+
+1.1.1 -> 1.2
+- Added Closed type
+- Updated to work with stack and also ghc-7.10
diff --git a/Data/Binding/Hobbits.hs b/Data/Binding/Hobbits.hs
--- a/Data/Binding/Hobbits.hs
+++ b/Data/Binding/Hobbits.hs
@@ -37,7 +37,7 @@
 
   -- * Ancilliary modules
   module Data.Proxy, module Data.Type.Equality,
-  module Data.Type.HList,
+  module Data.Type.RList,
   -- | Type lists track the types of bound variables.
   module Data.Binding.Hobbits.NuMatching
   -- | The "Data.Binding.Hobbits.NuMatching" module exposes the
@@ -47,7 +47,7 @@
 
 import Data.Proxy
 import Data.Type.Equality
-import Data.Type.HList
+import Data.Type.RList
 import Data.Binding.Hobbits.Mb
 import Data.Binding.Hobbits.Closed
 import Data.Binding.Hobbits.QQ
diff --git a/Data/Binding/Hobbits/Examples/LambdaLifting.hs b/Data/Binding/Hobbits/Examples/LambdaLifting.hs
--- a/Data/Binding/Hobbits/Examples/LambdaLifting.hs
+++ b/Data/Binding/Hobbits/Examples/LambdaLifting.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE QuasiQuotes, ViewPatterns #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeOperators, DataKinds #-}
 {-# LANGUAGE GADTs #-}
 
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
@@ -32,7 +32,7 @@
   ) where
 
 import Data.Binding.Hobbits
-import qualified Data.Type.HList as C
+import qualified Data.Type.RList as C
 
 import Data.Binding.Hobbits.Examples.LambdaLifting.Terms
 
@@ -46,10 +46,10 @@
 ------------------------------------------------------------
 
 data LType a where LType :: LType (L a)
-type LC c = HList LType c
+type LC c = MapRList LType c
 
-type family AddArrows c b
-type instance AddArrows Nil b = b
+type family AddArrows (c :: RList *) b
+type instance AddArrows RNil b = b
 type instance AddArrows (c :> L a) b = AddArrows c (a -> b)
 
 data PeelRet c a where
@@ -57,36 +57,36 @@
              PeelRet c (AddArrows lc a)
 
 peelLambdas :: Mb c (Binding (L b) (Term a)) -> PeelRet c (b -> a)
-peelLambdas b = peelLambdasH Nil LType (mbCombine b)
+peelLambdas b = peelLambdasH MNil LType (mbCombine b)
 
 peelLambdasH ::
   lc ~ (lc0 :> b) => LC lc0 -> LType b -> Mb (c :++: lc) (Term a) ->
                      PeelRet c (AddArrows lc a)
 peelLambdasH lc0 isl [nuP| Lam b |] =
-  peelLambdasH (lc0 :> isl) LType (mbCombine b)
-peelLambdasH lc0 ilt t = PeelRet (lc0 :> ilt) t
+  peelLambdasH (lc0 :>: isl) LType (mbCombine b)
+peelLambdasH lc0 ilt t = PeelRet (lc0 :>: ilt) t
 
 
 
 
 boundParams ::
-  lc ~ (lc0 :> b) => LC lc -> (HList Name lc -> DTerm a) ->
+  lc ~ (lc0 :> b) => LC lc -> (MapRList Name lc -> DTerm a) ->
                      Decl (AddArrows lc a)
-boundParams (lc0 :> LType) k = -- flagged as non-exhaustive, in spite of type
-  freeParams lc0 (\ns -> Decl_One $ nu $ \n -> k (ns :> n))
+boundParams (lc0 :>: LType) k = -- flagged as non-exhaustive, in spite of type
+  freeParams lc0 (\ns -> Decl_One $ nu $ \n -> k (ns :>: n))
 
 freeParams ::
-  LC lc -> (HList Name lc -> Decl a) -> Decl (AddArrows lc a)
-freeParams Nil k = k C.empty
-freeParams (lc :> LType) k =
-    freeParams lc (\names -> Decl_Cons $ nu $ \x -> k (names :> x))
+  LC lc -> (MapRList Name lc -> Decl a) -> Decl (AddArrows lc a)
+freeParams MNil k = k C.empty
+freeParams (lc :>: LType) k =
+    freeParams lc (\names -> Decl_Cons $ nu $ \x -> k (names :>: x))
 
 ------------------------------------------------------------
 -- sub-contexts
 ------------------------------------------------------------
 
 -- FIXME: use this type in place of functions
-type SubC c' c = HList Name c -> HList Name c'
+type SubC c' c = MapRList Name c -> MapRList Name c'
 
 ------------------------------------------------------------
 -- operations on contexts of free variables
@@ -95,7 +95,7 @@
 data MbLName c a where
     MbLName :: Mb c (Name (L a)) -> MbLName c (L a)
 
-type FVList c fvs = HList (MbLName c) fvs
+type FVList c fvs = MapRList (MbLName c) fvs
 
 -- unioning free variable contexts: the data structure
 data FVUnionRet c fvs1 fvs2 where
@@ -103,21 +103,21 @@
                   FVUnionRet c fvs1 fvs2
 
 fvUnion :: FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2
-fvUnion Nil Nil = FVUnionRet Nil (\_ -> Nil) (\_ -> Nil)
-fvUnion Nil (fvs2 :> fv2) = case fvUnion Nil fvs2 of
+fvUnion MNil MNil = FVUnionRet MNil (\_ -> MNil) (\_ -> MNil)
+fvUnion MNil (fvs2 :>: fv2) = case fvUnion MNil fvs2 of
   FVUnionRet fvs f1 f2 -> case elemMC fv2 fvs of
-    Nothing -> FVUnionRet (fvs :> fv2)
-               (\(xs :> _) -> f1 xs) (\(xs :> x) -> f2 xs :> x)
-    Just idx -> FVUnionRet fvs f1 (\xs -> f2 xs :> C.hlistLookup idx xs)
-fvUnion (fvs1 :> fv1) fvs2 = case fvUnion fvs1 fvs2 of
+    Nothing -> FVUnionRet (fvs :>: fv2)
+               (\(xs :>: _) -> f1 xs) (\(xs :>: x) -> f2 xs :>: x)
+    Just idx -> FVUnionRet fvs f1 (\xs -> f2 xs :>: C.hlistLookup idx xs)
+fvUnion (fvs1 :>: fv1) fvs2 = case fvUnion fvs1 fvs2 of
   FVUnionRet fvs f1 f2 -> case elemMC fv1 fvs of
-    Nothing -> FVUnionRet (fvs :> fv1)
-               (\(xs :> x) -> f1 xs :> x) (\(xs :> _) -> f2 xs)
-    Just idx -> FVUnionRet fvs (\xs -> f1 xs :> C.hlistLookup idx xs) f2
+    Nothing -> FVUnionRet (fvs :>: fv1)
+               (\(xs :>: x) -> f1 xs :>: x) (\(xs :>: _) -> f2 xs)
+    Just idx -> FVUnionRet fvs (\xs -> f1 xs :>: C.hlistLookup idx xs) f2
 
 elemMC :: MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
-elemMC _ Nil = Nothing
-elemMC mbLN@(MbLName n) (mc :> MbLName n') = case mbCmpName n n' of
+elemMC _ MNil = Nothing
+elemMC mbLN@(MbLName n) (mc :>: MbLName n') = case mbCmpName n n' of
   Just Refl -> Just Member_Base
   Nothing -> fmap Member_Step (elemMC mbLN mc)
 
@@ -131,7 +131,7 @@
     SDVar :: Name (D a) -> STerm c a
     SApp :: STerm c (a -> b) -> STerm c a -> STerm c b
 
-skelSubst :: STerm c a -> HList Name c -> DTerm a
+skelSubst :: STerm c a -> MapRList Name c -> DTerm a
 skelSubst (SWeaken f db) names = skelSubst db $ f names
 skelSubst (SVar inC) names = TVar $ C.hlistLookup inC names
 skelSubst (SDVar dTVar) _ = TDVar dTVar
@@ -142,11 +142,11 @@
   STerm fvs (AddArrows fvs a) -> FVList c fvs -> STerm fvs a
 skelAppMultiNames db args = skelAppMultiNamesH db args (C.members args) where
   skelAppMultiNamesH ::
-    STerm fvs (AddArrows args a) -> FVList c args -> HList (Member fvs) args ->
+    STerm fvs (AddArrows args a) -> FVList c args -> MapRList (Member fvs) args ->
     STerm fvs a
-  skelAppMultiNamesH fvs Nil _ = fvs
+  skelAppMultiNamesH fvs MNil _ = fvs
   -- flagged as non-exhaustive, in spite of type
-  skelAppMultiNamesH fvs (args :> MbLName _) (inCs :> inC) =
+  skelAppMultiNamesH fvs (args :>: MbLName _) (inCs :>: inC) =
     SApp (skelAppMultiNamesH fvs args inCs) (SVar inC)
 
 ------------------------------------------------------------
@@ -157,28 +157,31 @@
     FVSTerm :: FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a
 
 fvSSepLTVars ::
-  HList f lc -> FVSTerm (c :++: lc) Nil a -> FVSTerm c lc a
+  MapRList f lc -> FVSTerm (c :++: lc) RNil a -> FVSTerm c lc a
 fvSSepLTVars lc (FVSTerm fvs db) = case fvSSepLTVarsH lc Proxy fvs of
   SepRet fvs' f -> FVSTerm fvs' (SWeaken f db)
 
 data SepRet lc c fvs where
   SepRet :: FVList c fvs' -> SubC fvs (fvs' :++: lc) -> SepRet lc c fvs
 
--- | Create a 'Proxy' object for the type list of a 'HList' vector.
-proxyOfHList :: HList f c -> Proxy c
-proxyOfHList _ = Proxy
+-- | Create a 'Proxy' object for the type list of a 'MapRList' vector.
+proxyOfMapRList :: MapRList f c -> Proxy c
+proxyOfMapRList _ = Proxy
 
 fvSSepLTVarsH ::
-  HList f lc -> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs
-fvSSepLTVarsH _ _ Nil = SepRet Nil (\_ -> Nil)
-fvSSepLTVarsH lc c (fvs :> fv@(MbLName n)) = case fvSSepLTVarsH lc c fvs of
+  MapRList f lc -> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs
+fvSSepLTVarsH _ _ MNil = SepRet MNil (\_ -> MNil)
+fvSSepLTVarsH lc c (fvs :>: fv@(MbLName n)) = case fvSSepLTVarsH lc c fvs of
   SepRet m f -> case raiseAppName (C.mkMonoAppend c lc) n of
-    Left idx -> SepRet m (\xs -> f xs :> C.hlistLookup (C.weakenMemberL (proxyOfHList m) idx) xs)
-    Right n -> SepRet (m :> MbLName n)
-               (\xs -> case C.splitHList c' lc xs of
-                         (fvs' :> fv', lcs) ->
-                           f (appendHList fvs' lcs) :> fv')
-    where c' = proxyCons (proxyOfHList m) fv
+    Left idx ->
+      SepRet m (\xs ->
+                 f xs :>: C.hlistLookup (C.weakenMemberL (proxyOfMapRList m) idx) xs)
+    Right n ->
+      SepRet (m :>: MbLName n)
+      (\xs -> case C.splitMapRList c' lc xs of
+          (fvs' :>: fv', lcs) ->
+            f (appendMapRList fvs' lcs) :>: fv')
+    where c' = proxyCons (proxyOfMapRList m) fv
 
 raiseAppName ::
   Append c1 c2 (c1 :++: c2) -> Mb (c1 :++: c2) (Name a) -> Either (Member c2 a) (Mb c1 (Name a))
@@ -191,11 +194,11 @@
 -- lambda-lifting, woo hoo!
 ------------------------------------------------------------
 
-type LLBodyRet b c a = Cont (Decls b) (FVSTerm c Nil a)
+type LLBodyRet b c a = Cont (Decls b) (FVSTerm c RNil a)
 
 llBody :: LC c -> Mb c (Term a) -> LLBodyRet b c a
 llBody _ [nuP| Var v |] =
-  return $ FVSTerm (Nil :> MbLName v) $ SVar Member_Base
+  return $ FVSTerm (MNil :>: MbLName v) $ SVar Member_Base
 llBody c [nuP| App t1 t2 |] = do
   FVSTerm fvs1 db1 <- llBody c t1
   FVSTerm fvs2 db2 <- llBody c t2
@@ -203,23 +206,23 @@
   return $ FVSTerm names $ SApp (SWeaken sub1 db1) (SWeaken sub2 db2)
 llBody c [nuP| Lam b |] = do
   PeelRet lc body <- return $ peelLambdas b
-  llret <- llBody (C.appendHList c lc) body
+  llret <- llBody (C.appendMapRList c lc) body
   FVSTerm fvs db <- return $ fvSSepLTVars lc llret
   cont $ \k ->
     Decls_Cons (freeParams (fvsToLC fvs) $ \names1 ->
                 boundParams lc $ \names2 ->
-                skelSubst db (C.appendHList names1 names2))
+                skelSubst db (C.appendMapRList names1 names2))
       $ nu $ \d -> k $ FVSTerm fvs (skelAppMultiNames (SDVar d) fvs)
   where
     fvsToLC :: FVList c lc -> LC lc
-    fvsToLC = C.mapHList mbLNameToProof where
+    fvsToLC = C.mapMapRList mbLNameToProof where
       mbLNameToProof :: MbLName c a -> LType a
       mbLNameToProof (MbLName _) = LType
 
 -- the top-level lambda-lifting function
 lambdaLift :: Term a -> Decls a
-lambdaLift t = runCont (llBody Nil (emptyMb t)) $ \(FVSTerm fvs db) ->
-  Decls_Base (skelSubst db (C.mapHList (\(MbLName mbn) -> elimEmptyMb mbn) fvs))
+lambdaLift t = runCont (llBody MNil (emptyMb t)) $ \(FVSTerm fvs db) ->
+  Decls_Base (skelSubst db (C.mapMapRList (\(MbLName mbn) -> elimEmptyMb mbn) fvs))
 
 mbLambdaLift :: Mb c (Term a) -> Mb c (Decls a)
 mbLambdaLift = fmap lambdaLift
diff --git a/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs b/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs
--- a/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs
+++ b/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE TemplateHaskell, Rank2Types, QuasiQuotes, ViewPatterns #-}
-{-# LANGUAGE GADTs, KindSignatures #-}
+{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
 
 -- |
 -- Module      : Data.Binding.Hobbits.SuperComb
@@ -20,13 +20,13 @@
   ) where
 
 import Data.Binding.Hobbits
-import qualified Data.Type.HList as C
+import qualified Data.Type.RList as C
 
 -- dummy datatypes for distinguishing Decl names from Lam names
 data L a
 data D a
 
--- to make a function for HList (for pretty)
+-- to make a function for MapRList (for pretty)
 newtype StringF x = StringF String
 unStringF (StringF str) = str
 
@@ -52,14 +52,14 @@
 -- pretty print terms
 tpretty :: Term a -> String
 tpretty t = pretty' (emptyMb t) C.empty 0
-  where pretty' :: Mb c (Term a) -> HList StringF c -> Int -> String
+  where pretty' :: Mb c (Term a) -> MapRList StringF c -> Int -> String
         pretty' [nuP| Var b |] varnames n =
             case mbNameBoundP b of
               Left pf  -> unStringF (C.hlistLookup pf varnames)
               Right n -> "(free-var " ++ show n ++ ")"
         pretty' [nuP| Lam b |] varnames n =
             let x = "x" ++ show n in
-            "(\\" ++ x ++ "." ++ pretty' (mbCombine b) (varnames :> (StringF x)) (n+1) ++ ")"
+            "(\\" ++ x ++ "." ++ pretty' (mbCombine b) (varnames :>: (StringF x)) (n+1) ++ ")"
         pretty' [nuP| App b1 b2 |] varnames n =
             "(" ++ pretty' b1 varnames n ++ " " ++ pretty' b2 varnames n ++ ")"
 
@@ -98,7 +98,7 @@
 pretty :: DTerm a -> String
 pretty t = mpretty (emptyMb t) C.empty
 
-mpretty :: Mb c (DTerm a) -> HList StringF c -> String
+mpretty :: Mb c (DTerm a) -> MapRList StringF c -> String
 mpretty [nuP| TVar b |] varnames =
     mprettyName (mbNameBoundP b) varnames
 mpretty [nuP| TDVar b |] varnames =
@@ -116,18 +116,18 @@
 decls_pretty decls =
     "let\n" ++ (mdecls_pretty (emptyMb decls) C.empty 0)
 
-mdecls_pretty :: Mb c (Decls a) -> HList StringF c -> Int -> String
+mdecls_pretty :: Mb c (Decls a) -> MapRList StringF c -> Int -> String
 mdecls_pretty [nuP| Decls_Base t |] varnames n =
     "in " ++ (mpretty t varnames)
 mdecls_pretty [nuP| Decls_Cons decl rest |] varnames n =
     let fname = "F" ++ show n in
     fname ++ " " ++ (mdecl_pretty decl varnames 0) ++ "\n"
-    ++ mdecls_pretty (mbCombine rest) (varnames :> (StringF fname)) (n+1)
+    ++ mdecls_pretty (mbCombine rest) (varnames :>: (StringF fname)) (n+1)
 
-mdecl_pretty :: Mb c (Decl a) -> HList StringF c -> Int -> String
+mdecl_pretty :: Mb c (Decl a) -> MapRList StringF c -> Int -> String
 mdecl_pretty [nuP| Decl_One t|] varnames n =
   let vname = "x" ++ show n in
-  vname ++ " = " ++ mpretty (mbCombine t) (varnames :> StringF vname)
+  vname ++ " = " ++ mpretty (mbCombine t) (varnames :>: StringF vname)
 mdecl_pretty [nuP| Decl_Cons d|] varnames n =
   let vname = "x" ++ show n in
-  vname ++ " " ++ mdecl_pretty (mbCombine d) (varnames :> StringF vname) (n+1)
+  vname ++ " " ++ mdecl_pretty (mbCombine d) (varnames :>: StringF vname) (n+1)
diff --git a/Data/Binding/Hobbits/Internal/Mb.hs b/Data/Binding/Hobbits/Internal/Mb.hs
--- a/Data/Binding/Hobbits/Internal/Mb.hs
+++ b/Data/Binding/Hobbits/Internal/Mb.hs
@@ -21,14 +21,14 @@
 import Data.Typeable
 import Data.Proxy
 import Data.Type.Equality
-import Data.Type.HList
+import Data.Type.RList
 
 import Data.Binding.Hobbits.Internal.Name
 
 
 {-|
   An @Mb ctx b@ is a multi-binding that binds one name for each type
-  in @ctx@, where @ctx@ has the form @'Nil' ':>' t1 ':>' ... ':>' tn@.
+  in @ctx@, where @ctx@ has the form @'RNil' ':>' t1 ':>' ... ':>' tn@.
   Internally, multi-bindings are represented either as "fresh
   functions", which are functions that quantify over all fresh names
   that have not been used before and map them to the body of the
@@ -38,8 +38,8 @@
   that the names given in the pair can be relaced by fresher names.
 -}
 data Mb ctx b
-    = MkMbFun (HList Proxy ctx) (HList Name ctx -> b)
-    | MkMbPair (MbTypeRepr b) (HList Name ctx) b
+    = MkMbFun (MapRList Proxy ctx) (MapRList Name ctx -> b)
+    | MkMbPair (MbTypeRepr b) (MapRList Name ctx) b
     deriving Typeable
 
 
@@ -60,7 +60,7 @@
     MbTypeReprData :: MbTypeReprData a -> MbTypeRepr a
 
 data MbTypeReprData a =
-    MkMbTypeReprData (forall ctx. HList Name ctx -> HList Name ctx -> a -> a)
+    MkMbTypeReprData (forall ctx. MapRList Name ctx -> MapRList Name ctx -> a -> a)
 
 
 {-|
@@ -69,9 +69,9 @@
   listed in @ns'@. This is similar to the name-swapping of Nominal
   Logic, except that the swapping does not go both ways.
 -}
-mapNamesPf :: MbTypeRepr a -> HList Name ctx -> HList Name ctx -> a -> a
-mapNamesPf MbTypeReprName Nil Nil n = n
-mapNamesPf MbTypeReprName (names :> m) (names' :> m') n =
+mapNamesPf :: MbTypeRepr a -> MapRList Name ctx -> MapRList Name ctx -> a -> a
+mapNamesPf MbTypeReprName MNil MNil n = n
+mapNamesPf MbTypeReprName (names :>: m) (names' :>: m') n =
     case cmpName m n of
       Just Refl -> m'
       Nothing -> mapNamesPf MbTypeReprName names names' n
@@ -88,14 +88,14 @@
 
 
 -- | Ensures a multi-binding is in "fresh function" form
-ensureFreshFun :: Mb ctx a -> (HList Proxy ctx, HList Name ctx -> a)
+ensureFreshFun :: Mb ctx a -> (MapRList Proxy ctx, MapRList Name ctx -> a)
 ensureFreshFun (MkMbFun proxies f) = (proxies, f)
 ensureFreshFun (MkMbPair tRepr ns body) =
-    (mapHList (\_ -> Proxy) ns, \ns' -> mapNamesPf tRepr ns ns' body)
+    (mapMapRList (\_ -> Proxy) ns, \ns' -> mapNamesPf tRepr ns ns' body)
 
 -- | Ensures a multi-binding is in "fresh pair" form
-ensureFreshPair :: Mb ctx a -> (HList Name ctx, a)
+ensureFreshPair :: Mb ctx a -> (MapRList Name ctx, a)
 ensureFreshPair (MkMbPair _ ns body) = (ns, body)
 ensureFreshPair (MkMbFun proxies f) =
-    let ns = mapHList (MkName . fresh_name) proxies in
+    let ns = mapMapRList (MkName . fresh_name) proxies in
     (ns, f ns)
diff --git a/Data/Binding/Hobbits/Internal/Name.hs b/Data/Binding/Hobbits/Internal/Name.hs
--- a/Data/Binding/Hobbits/Internal/Name.hs
+++ b/Data/Binding/Hobbits/Internal/Name.hs
@@ -26,7 +26,7 @@
 import Data.IORef (IORef, newIORef, readIORef, writeIORef)
 import System.IO.Unsafe (unsafePerformIO)
 
-import Data.Type.HList
+import Data.Type.RList
 
 
 -- | A @Name a@ is a bound name that is associated with type @a@.
@@ -35,9 +35,9 @@
 instance Show (Name a) where
   showsPrec _ (MkName n) = showChar '#' . shows n . showChar '#'
 
-instance Show (HList Name c) where
-    show names = "[" ++ (concat $ intersperse "," $ hlistToList $
-                        mapHList (Constant . show) names) ++ "]"
+instance Show (MapRList Name c) where
+    show names = "[" ++ (concat $ intersperse "," $ mapRListToList $
+                        mapMapRList (Constant . show) names) ++ "]"
 
 
 -------------------------------------------------------------------------------
@@ -85,11 +85,11 @@
 
 
 -- building a proxy for each type in some unknown context
-data ExProxy where ExProxy :: HList Proxy ctx -> ExProxy
+data ExProxy where ExProxy :: MapRList Proxy ctx -> ExProxy
 proxyFromLen :: Int -> ExProxy
-proxyFromLen 0 = ExProxy Nil
+proxyFromLen 0 = ExProxy MNil
 proxyFromLen n = case proxyFromLen (n - 1) of
-                   ExProxy proxy -> ExProxy (proxy :> Proxy)
+                   ExProxy proxy -> ExProxy (proxy :>: Proxy)
 
 -- -- unsafely building a proxy for each type in ctx from the length n
 -- -- of ctx; this is only safe when we know the length of ctx = n
diff --git a/Data/Binding/Hobbits/Liftable.hs b/Data/Binding/Hobbits/Liftable.hs
--- a/Data/Binding/Hobbits/Liftable.hs
+++ b/Data/Binding/Hobbits/Liftable.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, TemplateHaskell, ViewPatterns, QuasiQuotes #-}
+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns, QuasiQuotes, DataKinds #-}
 
 -- |
 -- Module      : Data.Binding.Hobbits.Mb
@@ -18,7 +19,7 @@
 
 module Data.Binding.Hobbits.Liftable where
 
-import Data.Type.HList
+import Data.Type.RList
 import Data.Binding.Hobbits.Internal.Mb
 import Data.Binding.Hobbits.QQ
 import Data.Binding.Hobbits.Closed
diff --git a/Data/Binding/Hobbits/Mb.hs b/Data/Binding/Hobbits/Mb.hs
--- a/Data/Binding/Hobbits/Mb.hs
+++ b/Data/Binding/Hobbits/Mb.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, ViewPatterns #-}
+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, ViewPatterns, DataKinds #-}
 
 -- |
 -- Module      : Data.Binding.Hobbits.Mb
@@ -38,7 +38,7 @@
 
 import Unsafe.Coerce (unsafeCoerce)
 
-import Data.Type.HList
+import Data.Type.RList
 
 import Data.Binding.Hobbits.Internal.Name
 import Data.Binding.Hobbits.Internal.Mb
@@ -49,7 +49,7 @@
 -------------------------------------------------------------------------------
 
 -- | A @Binding@ is simply a multi-binding that binds one name
-type Binding a = Mb (Nil :> a)
+type Binding a = Mb (RNil :> a)
 
 -- note: we reverse l to show the inner-most bindings last
 instance Show a => Show (Mb c a) where
@@ -61,18 +61,18 @@
   body is the result of @f n@.
 -}
 nu :: (Name a -> b) -> Binding a b
-nu f = MkMbFun (Nil :> Proxy) (\(Nil :> n) -> f n)
+nu f = MkMbFun (MNil :>: Proxy) (\(MNil :>: n) -> f n)
 
 {-|
   The expression @nuMulti p f@ creates a multi-binding of zero or more
   names, one for each element of the vector @p@. The bound names are
   passed the names to @f@, which returns the body of the
-  multi-binding.  The argument @p@, of type @'HList' f ctx@, acts as a
+  multi-binding.  The argument @p@, of type @'MapRList' f ctx@, acts as a
   \"phantom\" argument, used to reify the list of types @ctx@ at the
   term level; thus it is unimportant what the type function @f@ is.
 -}
-nuMulti :: HList f ctx -> (HList Name ctx -> b) -> Mb ctx b
-nuMulti proxies f = MkMbFun (mapHList (const Proxy) proxies) f
+nuMulti :: MapRList f ctx -> (MapRList Name ctx -> b) -> Mb ctx b
+nuMulti proxies f = MkMbFun (mapMapRList (const Proxy) proxies) f
 
 -- | @nus = nuMulti@
 nus x = nuMulti x
@@ -95,12 +95,15 @@
 -}
 mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a)
 mbNameBoundP (ensureFreshPair -> (names, n)) = helper names n where
-    helper :: HList Name c -> Name a -> Either (Member c a) (Name a)
-    helper Nil n = Right n
-    helper (names :> (MkName i)) (MkName j) | i == j = unsafeCoerce $ Left Member_Base
-    helper (names :> _) n = case helper names n of
-                              Left memb -> Left (Member_Step memb)
-                              Right n -> Right n
+    helper :: MapRList Name c -> Name a -> Either (Member c a) (Name a)
+    helper MNil n = Right n
+    helper (names :>: (MkName i)) (MkName j)
+      | i == j =
+        unsafeCoerce $ Left Member_Base
+    helper (names :>: _) n =
+      case helper names n of
+        Left memb -> Left (Member_Step memb)
+        Right n -> Right n
 -- old implementation with lists
 {-
 case elemIndex n names of
@@ -129,30 +132,31 @@
 -------------------------------------------------------------------------------
 
 -- | Creates an empty binding that binds 0 names.
-emptyMb :: a -> Mb Nil a
-emptyMb body = MkMbFun Nil (\_ -> body)
+emptyMb :: a -> Mb RNil a
+emptyMb body = MkMbFun MNil (\_ -> body)
 
 {-|
   Eliminates an empty binding, returning its body. Note that
   @elimEmptyMb@ is the inverse of @emptyMb@.
 -}
-elimEmptyMb :: Mb Nil a -> a
+elimEmptyMb :: Mb RNil a -> a
 elimEmptyMb (ensureFreshPair -> (_, body)) = body
 
 
 -- Extract the proxy objects from an Mb inside of a fresh function
-freshFunctionProxies :: HList Proxy ctx1 -> (HList Name ctx1 -> Mb ctx2 a) ->
-                        HList Proxy ctx2
+freshFunctionProxies :: MapRList Proxy ctx1 -> (MapRList Name ctx1 -> Mb ctx2 a) ->
+                        MapRList Proxy ctx2
 freshFunctionProxies proxies1 f =
-    case f (mapHList (const $ MkName 0) proxies1) of
+    case f (mapMapRList (const $ MkName 0) proxies1) of
       MkMbFun proxies2 _ -> proxies2
-      MkMbPair _ ns _ -> mapHList (const Proxy) ns
+      MkMbPair _ ns _ -> mapMapRList (const Proxy) ns
 
 
 -- README: inner-most bindings come FIRST
 -- | Combines a binding inside another binding into a single binding.
 mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
-mbCombine (MkMbPair tRepr1 l1 (MkMbPair tRepr2 l2 b)) = MkMbPair tRepr2 (appendHList l1 l2) b
+mbCombine (MkMbPair tRepr1 l1 (MkMbPair tRepr2 l2 b)) =
+  MkMbPair tRepr2 (appendMapRList l1 l2) b
 mbCombine (ensureFreshFun -> (proxies1, f1)) =
     -- README: we pass in Names with integer value 0 here in order to
     -- get out the proxies for the inner-most bindings; this is "safe"
@@ -160,33 +164,33 @@
     -- themselves
     let proxies2 = freshFunctionProxies proxies1 f1 in
     MkMbFun
-    (appendHList proxies1 proxies2)
+    (appendMapRList proxies1 proxies2)
     (\ns ->
-         let (ns1, ns2) = splitHList Proxy proxies2 ns in
+         let (ns1, ns2) = splitMapRList Proxy proxies2 ns in
          let (_, f2) = ensureFreshFun (f1 ns1) in
          f2 ns2)
 
 
 {-|
   Separates a binding into two nested bindings. The first argument, of
-  type @'HList' any c2@, is a \"phantom\" argument to indicate how
+  type @'MapRList' any c2@, is a \"phantom\" argument to indicate how
   the context @c@ should be split.
 -}
-mbSeparate :: HList any ctx2 -> Mb (ctx1 :++: ctx2) a ->
+mbSeparate :: MapRList any ctx2 -> Mb (ctx1 :++: ctx2) a ->
               Mb ctx1 (Mb ctx2 a)
 mbSeparate c2 (MkMbPair tRepr ns a) =
     MkMbPair (MbTypeReprMb tRepr) ns1 (MkMbPair tRepr ns2 a) where
-        (ns1, ns2) = splitHList Proxy c2 ns
+        (ns1, ns2) = splitMapRList Proxy c2 ns
 mbSeparate c2 (MkMbFun proxies f) =
-    MkMbFun proxies1 (\ns1 -> MkMbFun proxies2 (\ns2 -> f (appendHList ns1 ns2)))
+    MkMbFun proxies1 (\ns1 -> MkMbFun proxies2 (\ns2 -> f (appendMapRList ns1 ns2)))
         where
-          (proxies1, proxies2) = splitHList Proxy c2 proxies
+          (proxies1, proxies2) = splitMapRList Proxy c2 proxies
 
 
 -- | Returns a proxy object that enumerates all the types in ctx.
-mbToProxy :: Mb ctx a -> HList Proxy ctx
+mbToProxy :: Mb ctx a -> MapRList Proxy ctx
 mbToProxy (MkMbFun proxies _) = proxies
-mbToProxy (MkMbPair _ ns _) = mapHList (\_ -> Proxy) ns
+mbToProxy (MkMbPair _ ns _) = mapMapRList (\_ -> Proxy) ns
 
 
 {-|
@@ -253,34 +257,36 @@
 
 > (<*>) :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
 > (<*>) f a =
->     nuWithElimMulti ('Nil' :> f :> a)
->                     (\_ ('Nil' :> 'Identity' f' :> 'Identity' a') -> f' a')
+>     nuWithElimMulti ('MNil' :>: f :>: a)
+>                     (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')
 -}
 nuMultiWithElim :: TypeCtx ctx =>
-                   (HList Name ctx -> HList Identity args -> b) ->
-                   HList (Mb ctx) args -> Mb ctx b
+                   (MapRList Name ctx -> MapRList Identity args -> b) ->
+                   MapRList (Mb ctx) args -> Mb ctx b
 nuMultiWithElim f args =
   MkMbFun typeCtxProxies
-          (\ns -> f ns $ mapHList (\arg -> Identity $ snd (ensureFreshFun arg) ns) args)
+          (\ns ->
+            f ns $ mapMapRList (\arg ->
+                                 Identity $ snd (ensureFreshFun arg) ns) args)
 
 
 {-|
   Similar to 'nuMultiWithElim' but binds only one name.
 -}
-nuWithElim :: (Name a -> HList Identity args -> b) ->
-              HList (Mb (Nil :> a)) args ->
+nuWithElim :: (Name a -> MapRList Identity args -> b) ->
+              MapRList (Mb (RNil :> a)) args ->
               Binding a b
 nuWithElim f args =
-    nuMultiWithElim (\(Nil :> n) -> f n) args
+    nuMultiWithElim (\(MNil :>: n) -> f n) args
 
 
 {-|
   Similar to 'nuMultiWithElim' but takes only one argument
 -}
-nuMultiWithElim1 :: TypeCtx ctx => (HList Name ctx -> arg -> b) -> Mb ctx arg ->
+nuMultiWithElim1 :: TypeCtx ctx => (MapRList Name ctx -> arg -> b) -> Mb ctx arg ->
                     Mb ctx b
 nuMultiWithElim1 f arg =
-    nuMultiWithElim (\names (Nil :> Identity arg) -> f names arg) (Nil :> arg)
+    nuMultiWithElim (\names (MNil :>: Identity arg) -> f names arg) (MNil :>: arg)
 
 
 {-|
@@ -289,4 +295,4 @@
 -}
 nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b
 nuWithElim1 f arg =
-  nuWithElim (\n (Nil :> Identity arg) -> f n arg) (Nil :> arg)
+  nuWithElim (\n (MNil :>: Identity arg) -> f n arg) (MNil :>: arg)
diff --git a/Data/Binding/Hobbits/NuMatching.hs b/Data/Binding/Hobbits/NuMatching.hs
--- a/Data/Binding/Hobbits/NuMatching.hs
+++ b/Data/Binding/Hobbits/NuMatching.hs
@@ -1,4 +1,6 @@
-{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies, FlexibleInstances, FlexibleContexts, TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}
+{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, DataKinds #-}
 
 -- |
 -- Module      : Data.Binding.Hobbits.NuMatching
@@ -30,14 +32,14 @@
 import Control.Monad.State
 --import Control.Monad.Identity
 
-import Data.Type.HList
+import Data.Type.RList
 import Data.Binding.Hobbits.Internal.Name
 import Data.Binding.Hobbits.Internal.Mb
 import Data.Binding.Hobbits.Internal.Closed
 
 
 {-| Just like 'mapNamesPf', except uses the NuMatching class. -}
-mapNames :: NuMatching a => HList Name ctx -> HList Name ctx -> a -> a
+mapNames :: NuMatching a => MapRList Name ctx -> MapRList Name ctx -> a -> a
 mapNames = mapNamesPf nuMatchingProof
 
 
@@ -116,13 +118,13 @@
 
 -- the NuMatchingList class, for saying that NuMatching holds for a context of types
 class NuMatchingList args where
-    nuMatchingListProof :: HList NuMatchingObj args
+    nuMatchingListProof :: MapRList NuMatchingObj args
 
-instance NuMatchingList Nil where
-    nuMatchingListProof = Nil
+instance NuMatchingList RNil where
+    nuMatchingListProof = MNil
 
 instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where
-    nuMatchingListProof = nuMatchingListProof :> NuMatchingObj ()
+    nuMatchingListProof = nuMatchingListProof :>: NuMatchingObj ()
 
 
 class NuMatching1 f where
@@ -135,16 +137,16 @@
     nuMatchingProof = nuMatchingProof1 nuMatchingProof
 -}
 
-instance (NuMatching1 f, NuMatchingList ctx) => NuMatching (HList f ctx) where
+instance (NuMatching1 f, NuMatchingList ctx) => NuMatching (MapRList f ctx) where
     nuMatchingProof = MbTypeReprData $ MkMbTypeReprData $ helper nuMatchingListProof where
         helper :: NuMatching1 f =>
-                  HList NuMatchingObj args -> HList Name ctx1 -> HList Name ctx1 ->
-                  HList f args -> HList f args
-        helper Nil c1 c2 Nil = Nil
-        helper (proofs :> NuMatchingObj ()) c1 c2 (elems :> (elem :: f a)) =
+                  MapRList NuMatchingObj args -> MapRList Name ctx1 ->
+                  MapRList Name ctx1 -> MapRList f args -> MapRList f args
+        helper MNil c1 c2 MNil = MNil
+        helper (proofs :>: NuMatchingObj ()) c1 c2 (elems :>: (elem :: f a)) =
             case nuMatchingProof1 :: NuMatchingObj (f a) of
               NuMatchingObj () ->
-                  (helper proofs c1 c2 elems) :>
+                  (helper proofs c1 c2 elems) :>:
                   mapNames c1 c2 elem
 
 
@@ -164,7 +166,7 @@
 
 type Names = (TH.Name, TH.Name, TH.Name, TH.Name)
 
-mapNamesType a = [t| forall ctx. HList Name ctx -> HList Name ctx -> $a -> $a |]
+mapNamesType a = [t| forall ctx. MapRList Name ctx -> MapRList Name ctx -> $a -> $a |]
 
 {-|
   Template Haskell function for creating NuMatching instances for (G)ADTs.
diff --git a/Data/Type/HList.hs b/Data/Type/HList.hs
deleted file mode 100644
--- a/Data/Type/HList.hs
+++ /dev/null
@@ -1,203 +0,0 @@
-{-# LANGUAGE TypeOperators, EmptyDataDecls, RankNTypes #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE GADTs #-}
-
--- |
--- Module      : Data.Type.HList
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : westbrook@galois.com
--- Stability   : experimental
--- Portability : GHC
---
--- A /type list/ contains types as elements. We use GADT proofs terms to
--- establish membership and append relations. A @Data.Type.HList.HList@ @f@
--- is a vector indexed by a type list, where @f :: * -> *@ is applied to each
--- type element.
-
-module Data.Type.HList where
-
-import Data.Type.Equality ((:~:)(..))
-import Data.Proxy (Proxy(..))
-import Data.Functor.Constant
-import Data.Typeable
-
--------------------------------------------------------------------------------
--- type-level lists
--------------------------------------------------------------------------------
-
-data Nil deriving Typeable
-data r :> a deriving Typeable; infixl 5 :>
-
-type family (r1 :++: r2); infixr 5 :++:
-type instance r :++: Nil = r
-type instance r1 :++: r2 :> a = (r1 :++: r2) :> a
-
-proxyCons :: Proxy r -> f a -> Proxy (r :> a)
-proxyCons _ _ = Proxy
-
-
--------------------------------------------------------------------------------
--- proofs of membership in a type-level list
--------------------------------------------------------------------------------
-
-{-|
-  A @Member ctx a@ is a \"proof\" that the type @a@ is in the type
-  list @ctx@, meaning that @ctx@ equals
-
->  t0 ':>' a ':>' t1 ':>' ... ':>' tn
-
-  for some types @t0,t1,...,tn@.
--}
-data Member ctx a where
-  Member_Base :: Member (ctx :> a) a
-  Member_Step :: Member ctx a -> Member (ctx :> b) a
-  deriving Typeable
-
-instance Show (Member r a) where showsPrec p = showsPrecMember (p > 10)
-
-showsPrecMember :: Bool -> Member ctx a -> ShowS
-showsPrecMember _ Member_Base = showString "Member_Base"
-showsPrecMember p (Member_Step prf) = showParen p $
-  showString "Member_Step" . showsPrec 10 prf
-
---toEq :: Member (Nil :> a) b -> b :~: a
---toEq Member_Base = Refl
---toEq _ = error "Should not happen! (toEq)"
-
-weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
-weakenMemberL _ Member_Base = Member_Base
-weakenMemberL tag (Member_Step mem) = Member_Step (weakenMemberL tag mem)
-
-membersEq :: Member ctx a -> Member ctx b -> Maybe (a :~: b)
-membersEq Member_Base Member_Base = Just Refl
-membersEq (Member_Step mem1) (Member_Step mem2) = membersEq mem1 mem2
-membersEq _ _ = Nothing
-
-
-------------------------------------------------------------
--- proofs that one list equals the append of two others
-------------------------------------------------------------
-
-{-|
-  An @Append ctx1 ctx2 ctx@ is a \"proof\" that @ctx = ctx1 ':++:' ctx2@.
--}
-data Append ctx1 ctx2 ctx where
-  Append_Base :: Append ctx Nil ctx
-  Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)
-
--- -- | Appends two 'Append' proofs.
--- trans ::
---   Append ctx1 ctx2 ex_ctx -> Append ex_ctx ctx3 ctx -> Append ctx1 (ctx2 :++: ctx3) ctx
--- trans app Append_Base = app
--- trans app (Append_Step app') = Append_Step (trans app app')
-
--- -- | Returns a proof that ctx :~: ctx1 :++: ctx2
--- appendPf :: Append ctx1 ctx2 ctx -> (ctx :~: ctx1 :++: ctx2)
--- appendPf Append_Base = Refl
--- appendPf (Append_Step app) = case appendPf app of Refl -> Refl
-
--- -- | Returns the length of an 'Append' proof.
--- length :: Append ctx1 ctx2 ctx3 -> Int
--- length Append_Base = 0
--- length (Append_Step app) = 1 + Data.Type.List.Proof.Append.length app
-
--------------------------------------------------------------------------------
--- Heterogeneous lists
--------------------------------------------------------------------------------
-
-{-|
-  A @HList f c@ is a vector with exactly one element of type @f a@ for
-  each type @a@ in the type list @c@.
--}
-data HList f c where
-  Nil :: HList f Nil -- Creates an empty vector
-  (:>) :: HList f c -> f a -> HList f (c :> a) -- Appends an element to the end of a vector
-
--- | Create an empty 'HList' vector.
-empty :: HList f Nil
-empty = Nil
-
--- | Create a singleton 'HList' vector.
-singleton :: f a -> HList f (Nil :> a)
-singleton x = Nil :> x
-
--- | Look up an element of a 'HList' vector using a 'Member' proof.
-hlistLookup :: Member c a -> HList f c -> f a
-hlistLookup Member_Base (_ :> x) = x
-hlistLookup (Member_Step mem') (mc :> _) = hlistLookup mem' mc
---hlistLookup _ _ = error "Should not happen! (hlistLookup)"
-
--- | Map a function on all elements of a 'HList' vector.
-mapHList :: (forall x. f x -> g x) -> HList f c -> HList g c
-mapHList _ Nil = Nil
-mapHList f (mc :> x) = mapHList f mc :> f x
-
--- | Map a binary function on all pairs of elements of two 'HList' vectors.
-mapHList2 :: (forall x. f x -> g x -> h x) -> HList f c -> HList g c -> HList h c
-mapHList2 _ Nil Nil = Nil
-mapHList2 f (xs :> x) (ys :> y) = mapHList2 f xs ys :> f x y
-mapHList2 _ _ _ = error "Something is terribly wrong in mapHList2: this case should not happen!"
-
--- | Append two 'HList' vectors.
-appendHList :: HList f c1 -> HList f c2 -> HList f (c1 :++: c2)
-appendHList mc Nil = mc
-appendHList mc1 (mc2 :> x) = appendHList mc1 mc2 :> x
-
--- -- | Append two 'HList' vectors.
--- appendWithPf :: Append c1 c2 c -> HList f c1 -> HList f c2 -> HList f c
--- appendWithPf Append_Base mc Nil = mc
--- appendWithPf (Append_Step app) mc1 (mc2 :> x) = appendWithPf app mc1 mc2 :> x
--- appendWithPf  _ _ _ = error "Something is terribly wrong in appendWithPf: this case should not happen!"
-
--- | Make an 'Append' proof from any 'HList' vector for the second
--- argument of the append.
-mkAppend :: HList f c2 -> Append c1 c2 (c1 :++: c2)
-mkAppend Nil = Append_Base
-mkAppend (c :> _) = Append_Step (mkAppend c)
-
--- | A version of 'mkAppend' that takes in a 'Proxy' argument.
-mkMonoAppend :: Proxy c1 -> HList f c2 -> Append c1 c2 (c1 :++: c2)
-mkMonoAppend _ = mkAppend
-
--- | The inverse of 'mkAppend', that builds an 'HList' from an 'Append'
-proxiesFromAppend :: Append c1 c2 c -> HList Proxy c2
-proxiesFromAppend Append_Base = Nil
-proxiesFromAppend (Append_Step a) = proxiesFromAppend a :> Proxy
-
--- | Split an 'HList' vector into two pieces. The first argument is a
--- phantom argument that gives the form of the first list piece.
-splitHList :: (c ~ (c1 :++: c2)) => Proxy c1 -> HList any c2 -> HList f c -> (HList f c1, HList f c2)
-splitHList _ Nil mc = (mc, Nil)
-splitHList _ (any :> _) (mc :> x) = (mc1, mc2 :> x)
-  where (mc1, mc2) = splitHList Proxy any mc
---split _ _ = error "Should not happen! (Map.split)"
-
--- | Create a vector of proofs that each type in @c@ is a 'Member' of @c@.
-members :: HList f c -> HList (Member c) c
-members Nil = Nil
-members (c :> _) = mapHList Member_Step (members c) :> Member_Base
-
--- -- | Replace a single element of a 'HList' vector.
--- replace :: HList f c -> Member c a -> f a -> HList f c
--- replace (xs :> _) Member_Base y = xs :> y
--- replace (xs :> x) (Member_Step memb) y = replace xs memb y :> x
--- replace _ _ _ = error "Should not happen! (Map.replace)"
-
--- | Convert an HList to a list
-hlistToList :: HList (Constant a) c -> [a]
-hlistToList Nil = []
-hlistToList (xs :> Constant x) = hlistToList xs ++ [x]
-
--- | A type-class which ensures that ctx is a valid context, i.e., has
--- | the form (Nil :> t1 :> ... :> tn) for some types t1 through tn
-class TypeCtx ctx where
-  typeCtxProxies :: HList Proxy ctx
-
-instance TypeCtx Nil where
-  typeCtxProxies = Nil
-
-instance TypeCtx ctx => TypeCtx (ctx :> a) where
-  typeCtxProxies = typeCtxProxies :> Proxy
diff --git a/Data/Type/RList.hs b/Data/Type/RList.hs
new file mode 100644
--- /dev/null
+++ b/Data/Type/RList.hs
@@ -0,0 +1,208 @@
+{-# LANGUAGE TypeOperators, EmptyDataDecls, RankNTypes #-}
+{-# LANGUAGE TypeFamilies, DataKinds, KindSignatures #-}
+{-# LANGUAGE GADTs #-}
+
+-- |
+-- Module      : Data.Type.RList
+-- Copyright   : (c) 2016 Edwin Westbrook
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@galois.com
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- A /right list/, or 'RList', is a list where cons adds to the end, or the
+-- right-hand side, of a list. This is useful conceptually for contexts of
+-- name-bindings, where the most recent name-binding is intuitively at the end
+-- of the context.
+
+module Data.Type.RList where
+
+import Data.Type.Equality ((:~:)(..))
+import Data.Proxy (Proxy(..))
+import Data.Functor.Constant
+import Data.Typeable
+
+-------------------------------------------------------------------------------
+-- Right-lists as a datatype
+-------------------------------------------------------------------------------
+
+data RList a
+  = RNil
+  | (RList a) :> a
+
+type family ((r1 :: RList *) :++: (r2 :: RList *)) :: RList *
+infixr 5 :++:
+type instance r :++: RNil = r
+type instance r1 :++: r2 :> a = (r1 :++: r2) :> a
+
+proxyCons :: Proxy r -> f a -> Proxy (r :> a)
+proxyCons _ _ = Proxy
+
+
+-------------------------------------------------------------------------------
+-- proofs of membership in a type-level list
+-------------------------------------------------------------------------------
+
+{-|
+  A @Member ctx a@ is a \"proof\" that the type @a@ is in the type
+  list @ctx@, meaning that @ctx@ equals
+
+>  t0 ':>' a ':>' t1 ':>' ... ':>' tn
+
+  for some types @t0,t1,...,tn@.
+-}
+data Member ctx a where
+  Member_Base :: Member (ctx :> a) a
+  Member_Step :: Member ctx a -> Member (ctx :> b) a
+  deriving Typeable
+
+instance Show (Member r a) where showsPrec p = showsPrecMember (p > 10)
+
+showsPrecMember :: Bool -> Member ctx a -> ShowS
+showsPrecMember _ Member_Base = showString "Member_Base"
+showsPrecMember p (Member_Step prf) = showParen p $
+  showString "Member_Step" . showsPrec 10 prf
+
+--toEq :: Member (Nil :> a) b -> b :~: a
+--toEq Member_Base = Refl
+--toEq _ = error "Should not happen! (toEq)"
+
+weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
+weakenMemberL _ Member_Base = Member_Base
+weakenMemberL tag (Member_Step mem) = Member_Step (weakenMemberL tag mem)
+
+membersEq :: Member ctx a -> Member ctx b -> Maybe (a :~: b)
+membersEq Member_Base Member_Base = Just Refl
+membersEq (Member_Step mem1) (Member_Step mem2) = membersEq mem1 mem2
+membersEq _ _ = Nothing
+
+
+------------------------------------------------------------
+-- proofs that one list equals the append of two others
+------------------------------------------------------------
+
+{-|
+  An @Append ctx1 ctx2 ctx@ is a \"proof\" that @ctx = ctx1 ':++:' ctx2@.
+-}
+data Append ctx1 ctx2 ctx where
+  Append_Base :: Append ctx RNil ctx
+  Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)
+
+-- -- | Appends two 'Append' proofs.
+-- trans ::
+--   Append ctx1 ctx2 ex_ctx -> Append ex_ctx ctx3 ctx -> Append ctx1 (ctx2 :++: ctx3) ctx
+-- trans app Append_Base = app
+-- trans app (Append_Step app') = Append_Step (trans app app')
+
+-- -- | Returns a proof that ctx :~: ctx1 :++: ctx2
+-- appendPf :: Append ctx1 ctx2 ctx -> (ctx :~: ctx1 :++: ctx2)
+-- appendPf Append_Base = Refl
+-- appendPf (Append_Step app) = case appendPf app of Refl -> Refl
+
+-- -- | Returns the length of an 'Append' proof.
+-- length :: Append ctx1 ctx2 ctx3 -> Int
+-- length Append_Base = 0
+-- length (Append_Step app) = 1 + Data.Type.List.Proof.Append.length app
+
+-------------------------------------------------------------------------------
+-- Heterogeneous lists
+-------------------------------------------------------------------------------
+
+{-|
+  A @MapRList f r@ is a vector with exactly one element of type @f a@ for
+  each type @a@ in the type 'RList' @r@.
+-}
+data MapRList f c where
+  MNil :: MapRList f RNil
+  (:>:) :: MapRList f c -> f a -> MapRList f (c :> a)
+
+-- | Create an empty 'MapRList' vector.
+empty :: MapRList f RNil
+empty = MNil
+
+-- | Create a singleton 'MapRList' vector.
+singleton :: f a -> MapRList f (RNil :> a)
+singleton x = MNil :>: x
+
+-- | Look up an element of a 'MapRList' vector using a 'Member' proof.
+hlistLookup :: Member c a -> MapRList f c -> f a
+hlistLookup Member_Base (_ :>: x) = x
+hlistLookup (Member_Step mem') (mc :>: _) = hlistLookup mem' mc
+--hlistLookup _ _ = error "Should not happen! (hlistLookup)"
+
+-- | Map a function on all elements of a 'MapRList' vector.
+mapMapRList :: (forall x. f x -> g x) -> MapRList f c -> MapRList g c
+mapMapRList _ MNil = MNil
+mapMapRList f (mc :>: x) = mapMapRList f mc :>: f x
+
+-- | Map a binary function on all pairs of elements of two 'MapRList' vectors.
+mapMapRList2 :: (forall x. f x -> g x -> h x) ->
+                MapRList f c -> MapRList g c -> MapRList h c
+mapMapRList2 _ MNil MNil = MNil
+mapMapRList2 f (xs :>: x) (ys :>: y) = mapMapRList2 f xs ys :>: f x y
+mapMapRList2 _ _ _ =
+  error "Something is terribly wrong in mapMapRList2: this case should not happen!"
+
+-- | Append two 'MapRList' vectors.
+appendMapRList :: MapRList f c1 -> MapRList f c2 -> MapRList f (c1 :++: c2)
+appendMapRList mc MNil = mc
+appendMapRList mc1 (mc2 :>: x) = appendMapRList mc1 mc2 :>: x
+
+-- -- | Append two 'MapRList' vectors.
+-- appendWithPf :: Append c1 c2 c -> MapRList f c1 -> MapRList f c2 -> MapRList f c
+-- appendWithPf Append_Base mc Nil = mc
+-- appendWithPf (Append_Step app) mc1 (mc2 :>: x) = appendWithPf app mc1 mc2 :>: x
+-- appendWithPf  _ _ _ = error "Something is terribly wrong in appendWithPf: this case should not happen!"
+
+-- | Make an 'Append' proof from any 'MapRList' vector for the second
+-- argument of the append.
+mkAppend :: MapRList f c2 -> Append c1 c2 (c1 :++: c2)
+mkAppend MNil = Append_Base
+mkAppend (c :>: _) = Append_Step (mkAppend c)
+
+-- | A version of 'mkAppend' that takes in a 'Proxy' argument.
+mkMonoAppend :: Proxy c1 -> MapRList f c2 -> Append c1 c2 (c1 :++: c2)
+mkMonoAppend _ = mkAppend
+
+-- | The inverse of 'mkAppend', that builds an 'MapRList' from an 'Append'
+proxiesFromAppend :: Append c1 c2 c -> MapRList Proxy c2
+proxiesFromAppend Append_Base = MNil
+proxiesFromAppend (Append_Step a) = proxiesFromAppend a :>: Proxy
+
+-- | Split an 'MapRList' vector into two pieces. The first argument is a
+-- phantom argument that gives the form of the first list piece.
+splitMapRList :: (c ~ (c1 :++: c2)) => Proxy c1 ->
+                 MapRList any c2 -> MapRList f c -> (MapRList f c1, MapRList f c2)
+splitMapRList _ MNil mc = (mc, MNil)
+splitMapRList _ (any :>: _) (mc :>: x) = (mc1, mc2 :>: x)
+  where (mc1, mc2) = splitMapRList Proxy any mc
+--split _ _ = error "Should not happen! (Map.split)"
+
+-- | Create a vector of proofs that each type in @c@ is a 'Member' of @c@.
+members :: MapRList f c -> MapRList (Member c) c
+members MNil = MNil
+members (c :>: _) = mapMapRList Member_Step (members c) :>: Member_Base
+
+-- -- | Replace a single element of a 'MapRList' vector.
+-- replace :: MapRList f c -> Member c a -> f a -> MapRList f c
+-- replace (xs :>: _) Member_Base y = xs :>: y
+-- replace (xs :>: x) (Member_Step memb) y = replace xs memb y :>: x
+-- replace _ _ _ = error "Should not happen! (Map.replace)"
+
+-- | Convert an MapRList to a list
+mapRListToList :: MapRList (Constant a) c -> [a]
+mapRListToList MNil = []
+mapRListToList (xs :>: Constant x) = mapRListToList xs ++ [x]
+
+-- | A type-class which ensures that ctx is a valid context, i.e., has
+-- | the form (RNil :> t1 :> ... :> tn) for some types t1 through tn
+class TypeCtx ctx where
+  typeCtxProxies :: MapRList Proxy ctx
+
+instance TypeCtx RNil where
+  typeCtxProxies = MNil
+
+instance TypeCtx ctx => TypeCtx (ctx :> a) where
+  typeCtxProxies = typeCtxProxies :>: Proxy
diff --git a/hobbits.cabal b/hobbits.cabal
--- a/hobbits.cabal
+++ b/hobbits.cabal
@@ -1,5 +1,5 @@
 Name:                hobbits
-Version:             1.2
+Version:             1.2.1
 Synopsis:            A library for canonically representing terms with binding
 
 Description: A library for canonically representing terms with binding via a
@@ -16,6 +16,8 @@
 Cabal-version: >= 1.6.0.1
 Build-Type:    Simple
 
+extra-source-files: CHANGELOG
+
 Library
   Build-Depends: base >= 4.7 && < 4.9
   Build-Depends: template-haskell >= 2.9 && < 2.11
@@ -33,7 +35,7 @@
 
   Extensions: CPP
 
-  Exposed-Modules: Data.Type.HList,
+  Exposed-Modules: Data.Type.RList,
 
                    Data.Binding.Hobbits,
                    Data.Binding.Hobbits.Mb,