diff --git a/Data/Binding/Hobbits.hs b/Data/Binding/Hobbits.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits.hs
+++ /dev/null
@@ -1,55 +0,0 @@
-{-# LANGUAGE TypeOperators #-}
-
--- |
--- Module      : Data.Binding.Hobbits
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- This library implements multi-bindings as described in the paper
--- E. Westbrook, N. Frisby, P. Brauner, \"Hobbits for Haskell: A Library for
--- Higher-Order Encodings in Functional Programming Languages\".
-
-module Data.Binding.Hobbits (
-  -- * Values under multi-bindings
-  module Data.Binding.Hobbits.Mb,
-  -- | The 'Data.Binding.Hobbits.Mb.Mb' type modeling multi-bindings is the
-  -- central abstract type of the library
-
-  -- * Closed terms
-  module Data.Binding.Hobbits.Closed,
-  -- | The 'Data.Binding.Hobbits.Closed.Cl' type models
-  -- super-combinators, which are safe functions to apply under
-  -- 'Data.Binding.Hobbits.Mb.Mb'.
-
-  -- * Pattern-matching multi-bindings and closed terms
-  module Data.Binding.Hobbits.QQ,
-  -- | The 'Data.Binding.Hobbits.QQ.nuP' quasiquoter allows safe pattern
-  -- matching on 'Data.Binding.Hobbits.Mb.Mb'
-  -- values. 'Data.Binding.Hobbits.QQ.superCombP' is similar.
-
-  -- * Lifting values out of multi-bindings
-  module Data.Binding.Hobbits.Liftable,
-
-  -- * Ancilliary modules
-  module Data.Proxy, module Data.Type.Equality,
-  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
-  -- | NuMatching class, which allows pattern-matching on (G)ADTs in
-  -- | the bodies of multi-bindings
-                            ) where
-
-import Data.Proxy
-import Data.Type.Equality
-import Data.Type.RList
-import Data.Binding.Hobbits.Mb
-import Data.Binding.Hobbits.Closed
-import Data.Binding.Hobbits.QQ
-import Data.Binding.Hobbits.Liftable
-import Data.Binding.Hobbits.NuMatching
diff --git a/Data/Binding/Hobbits/Closed.hs b/Data/Binding/Hobbits/Closed.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Closed.hs
+++ /dev/null
@@ -1,64 +0,0 @@
-{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
-
--- |
--- Module      : Data.Binding.Hobbits.Closed
--- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- This module uses Template Haskell to distinguish closed terms, so that the
--- library can trust such functions to not contain any @Name@ values in their
--- closure.
-
-module Data.Binding.Hobbits.Closed (
-  -- * Abstract types
-  Closed(),
-  -- * Operators involving 'Closed'
-  unClosed, mkClosed, noClosedNames, clApply, clMbApply, clApplyCl,
-  -- * Typeclass for inherently closed types
-  Closable(..)
-) where
-
-import Data.Binding.Hobbits.Internal.Name
-import Data.Binding.Hobbits.Internal.Mb
-import Data.Binding.Hobbits.Internal.Closed
-import Data.Binding.Hobbits.Mb
-
--- | @noClosedNames@ encodes the hobbits guarantee that no name can escape its
--- multi-binding.
-noClosedNames :: Closed (Name a) -> b
-noClosedNames (Closed n) =
-  -- We compare n to itself to force evaluation, in case the body of
-  -- the closed value is non-terminating...
-  case cmpName n n of
-    _ ->
-      error $
-      "... Clever girl!" ++
-      "The `noClosedNames' invariant has somehow been violated."
-
--- | Closed terms are closed (sorry) under application.
-clApply :: Closed (a -> b) -> Closed a -> Closed b
--- could be defined with cl were it not for the GHC stage restriction
-clApply (Closed f) (Closed a) = Closed (f a)
-
--- | Closed multi-bindings are also closed under application.
-clMbApply :: Closed (Mb ctx (a -> b)) -> Closed (Mb ctx a) ->
-             Closed (Mb ctx b)
-clMbApply (Closed f) (Closed a) = Closed (mbApply f a)
-
--- | When applying a closed function, the argument can be viewed as locally
--- closed
-clApplyCl :: Closed (Closed a -> b) -> Closed a -> Closed b
-clApplyCl (Closed f) a = Closed (f a)
-
--- | FIXME: this should not be possible!!
-closeBug :: a -> Closed a
-closeBug = $([| \x -> $(mkClosed [| x |]) |])
-
--- | Typeclass for inherently closed types
-class Closable a where
-  toClosed :: a -> Closed a
diff --git a/Data/Binding/Hobbits/Examples/LambdaLifting.hs b/Data/Binding/Hobbits/Examples/LambdaLifting.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Examples/LambdaLifting.hs
+++ /dev/null
@@ -1,228 +0,0 @@
-{-# LANGUAGE QuasiQuotes, ViewPatterns #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeOperators, DataKinds #-}
-{-# LANGUAGE GADTs #-}
-
-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
-
--- |
--- Module      : Data.Binding.Hobbits.Examples.LambdaLifting
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- The lambda lifting example from the paper E. Westbrook, N. Frisby,
--- P. Brauner, \"Hobbits for Haskell: A Library for Higher-Order Encodings in
--- Functional Programming Languages\".
-
--------------------------------------------------------------------------
--- lambda lifting for the lambda calculus with top-level declarations
--------------------------------------------------------------------------
-
-module Data.Binding.Hobbits.Examples.LambdaLifting (
-  -- * Term data types, using 'Data.Binding.Hobbits.Mb'
-  module Data.Binding.Hobbits.Examples.LambdaLifting.Terms,
-  -- * The lambda-lifting function
-  lambdaLift, mbLambdaLift
-  ) where
-
-import Data.Binding.Hobbits
-import qualified Data.Type.RList as C
-
-import Data.Binding.Hobbits.Examples.LambdaLifting.Terms
-
--- imported for ease of use at terminal
-import Data.Binding.Hobbits.Examples.LambdaLifting.Examples
-
-import Control.Monad.Cont (Cont, runCont, cont)
-
-------------------------------------------------------------
--- "peeling" lambdas off of a term
-------------------------------------------------------------
-
-data LType a where LType :: LType (L a)
-type LC c = MapRList LType c
-
-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
-  PeelRet :: lc ~ (lc0 :> b) => LC lc -> Mb (c :++: lc) (Term a) ->
-             PeelRet c (AddArrows lc a)
-
-peelLambdas :: Mb c (Binding (L b) (Term a)) -> PeelRet c (b -> a)
-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
-
-
-
-
-boundParams ::
-  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))
-
-freeParams ::
-  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 = MapRList Name c -> MapRList Name c'
-
-------------------------------------------------------------
--- operations on contexts of free variables
-------------------------------------------------------------
-
-data MbLName c a where
-    MbLName :: Mb c (Name (L a)) -> MbLName c (L a)
-
-type FVList c fvs = MapRList (MbLName c) fvs
-
--- unioning free variable contexts: the data structure
-data FVUnionRet c fvs1 fvs2 where
-    FVUnionRet :: FVList c fvs -> SubC fvs1 fvs -> SubC fvs2 fvs ->
-                  FVUnionRet c fvs1 fvs2
-
-fvUnion :: FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2
-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.mapRListLookup 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.mapRListLookup idx xs) f2
-
-elemMC :: MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
-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)
-
-------------------------------------------------------------
--- deBruijn terms, i.e., closed terms
-------------------------------------------------------------
-
-data STerm c a where
-    SWeaken :: SubC c1 c -> STerm c1 a -> STerm c a
-    SVar :: Member c (L a) -> STerm c a
-    SDVar :: Name (D a) -> STerm c a
-    SApp :: STerm c (a -> b) -> STerm c a -> STerm c b
-
-skelSubst :: STerm c a -> MapRList Name c -> DTerm a
-skelSubst (SWeaken f db) names = skelSubst db $ f names
-skelSubst (SVar inC) names = TVar $ C.mapRListLookup inC names
-skelSubst (SDVar dTVar) _ = TDVar dTVar
-skelSubst (SApp db1 db2) names = TApp (skelSubst db1 names) (skelSubst db2 names)
-
--- applying a STerm to a context of names
-skelAppMultiNames ::
-  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 -> MapRList (Member fvs) args ->
-    STerm fvs a
-  skelAppMultiNamesH fvs MNil _ = fvs
-  -- flagged as non-exhaustive, in spite of type
-  skelAppMultiNamesH fvs (args :>: MbLName _) (inCs :>: inC) =
-    SApp (skelAppMultiNamesH fvs args inCs) (SVar inC)
-
-------------------------------------------------------------
--- STerms combined with their free variables
-------------------------------------------------------------
-
-data FVSTerm c lc a where
-    FVSTerm :: FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a
-
-fvSSepLTVars ::
-  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 'MapRList' vector.
-proxyOfMapRList :: MapRList f c -> Proxy c
-proxyOfMapRList _ = Proxy
-
-fvSSepLTVarsH ::
-  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.mapRListLookup (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))
-raiseAppName app n =
-  case fmap mbNameBoundP (mbSeparate (proxiesFromAppend app) n) of
-    [nuP| Left mem |] -> Left $ mbLift mem
-    [nuP| Right n |] -> Right n
-
-------------------------------------------------------------
--- lambda-lifting, woo hoo!
-------------------------------------------------------------
-
-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 (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
-  FVUnionRet names sub1 sub2 <- return $ fvUnion fvs1 fvs2
-  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.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.appendMapRList names1 names2))
-      $ nu $ \d -> k $ FVSTerm fvs (skelAppMultiNames (SDVar d) fvs)
-  where
-    fvsToLC :: FVList c lc -> LC lc
-    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 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/Examples.hs b/Data/Binding/Hobbits/Examples/LambdaLifting/Examples.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Examples/LambdaLifting/Examples.hs
+++ /dev/null
@@ -1,52 +0,0 @@
--- |
--- Module      : Data.Binding.Hobbits.SuperComb
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
-
-module Data.Binding.Hobbits.Examples.LambdaLifting.Examples where
-
-import Data.Binding.Hobbits.Examples.LambdaLifting.Terms
-import Data.Binding.Hobbits
-
-------------------------------------------------------------
--- examples
-------------------------------------------------------------
-
-ex1 :: Term ((b1 -> b) -> b1 -> b)
-ex1 = lam (\f -> (lam $ \x -> App f x))
-
-ex2 :: Term ((((b2 -> b1) -> b2 -> b1) -> b) -> b)
-ex2 = lam (\f1 -> App f1 (lam (\f2 -> lam (\x -> App f2 x))))
-
-ex3 :: Term (b3 -> (((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b)
-ex3 = lam (\x -> lam (\f1 -> App f1 (lam (\f2 -> lam (\y -> f2 `App` x `App` y)))))
-
-ex4
-  :: Term
-       (((b1 -> b) -> b2 -> b)
-        -> (((b1 -> b) -> b2 -> b) -> b2 -> b1)
-        -> b2
-        -> b1)
-ex4 = lam $ \x -> lam $ \f1 ->
-      App f1 (lam $ \f2 -> lam $ \y -> f2 `App` (f1 `App` x `App` y))
-
-ex5 :: Term (((b2 -> b1) -> b) -> (b2 -> b1) -> b)
-ex5 = lam (\f1 -> lam $ \f2 -> App f1 (lam $ \x -> App f2 x))
-
--- lambda-lift with a free variable (use mbLambdaLift)
-ex6 :: Binding (L ((b -> b) -> a)) (Term a)
-ex6 = nu (\f -> App (Var f) (lam $ \x -> x))
-
--- lambda-lift with a free variable as part of a lambda's environment
-ex7 :: Binding (L ((b2 -> b2) -> b1)) (Term ((b1 -> b) -> b))
-ex7 = nu (\f -> lam $ \y -> App y $ App (Var f) (lam $ \x -> x))
-
--- example from paper's Section 4
-exP :: Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b)
-exP = lam $ \f -> lam $ \g -> App f $ lam $ \x -> App g $ App g x
diff --git a/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs b/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs
+++ /dev/null
@@ -1,133 +0,0 @@
-{-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE TemplateHaskell, Rank2Types, QuasiQuotes, ViewPatterns #-}
-{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
-
--- |
--- Module      : Data.Binding.Hobbits.SuperComb
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
-
-module Data.Binding.Hobbits.Examples.LambdaLifting.Terms
-  (L, D,
-   Term(..), lam,
-   DTerm(..), Decl(..), Decls(..)
-  ) where
-
-import Data.Binding.Hobbits
-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 MapRList (for pretty)
-newtype StringF x = StringF String
-unStringF (StringF str) = str
-
-
-------------------------------------------------------------
--- source terms
-------------------------------------------------------------
-
--- Term datatype; no Ds since there's no declarations yet
-data Term :: * -> * where
-  Var :: Name (L a) -> Term a
-  Lam :: Binding (L b) (Term a) -> Term (b -> a)
-  App :: Term (b -> a) -> Term b -> Term a
-
-$(mkNuMatching [t| forall a . Term a |])
-
-instance Show (Term a) where show = tpretty
-
--- helps to build terms without explicitly using nu or Var
-lam :: (Term a -> Term b) -> Term (a -> b)
-lam f = Lam $ nu (f . Var)
-
--- pretty print terms
-tpretty :: Term a -> String
-tpretty t = pretty' (emptyMb t) C.empty 0
-  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.mapRListLookup 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) ++ ")"
-        pretty' [nuP| App b1 b2 |] varnames n =
-            "(" ++ pretty' b1 varnames n ++ " " ++ pretty' b2 varnames n ++ ")"
-
-------------------------------------------------------------
--- target terms
-------------------------------------------------------------
-
--- terms under declarations
-data DTerm :: * -> * where
-  TVar :: Name (L a) -> DTerm a
-  TDVar :: Name (D a) -> DTerm a
-  TApp :: DTerm (a -> b) -> DTerm a -> DTerm b
-
--- we use this type for a definiens instead of putting lambdas on the front
-data Decl :: * -> * where
-  Decl_One :: Binding (L a) (DTerm b) -> Decl (a -> b)
-  Decl_Cons :: Binding (L a) (Decl b) -> Decl (a -> b)
-
--- top-level declarations with a return value
-data Decls :: * -> * where
-  Decls_Base :: DTerm a -> Decls a
-  Decls_Cons :: Decl b -> Binding (D b) (Decls a) -> Decls a
-
-$(mkNuMatching [t| forall a . DTerm a |])
-$(mkNuMatching [t| forall a . Decl a |])
-$(mkNuMatching [t| forall a . Decls a |])
-
-instance Show (DTerm a) where show = pretty
-instance Show (Decls a) where show = decls_pretty
-
-------------------------------------------------------------
--- pretty printing
-------------------------------------------------------------
-
--- pretty print terms
-pretty :: DTerm a -> String
-pretty t = mpretty (emptyMb t) C.empty
-
-mpretty :: Mb c (DTerm a) -> MapRList StringF c -> String
-mpretty [nuP| TVar b |] varnames =
-    mprettyName (mbNameBoundP b) varnames
-mpretty [nuP| TDVar b |] varnames =
-    mprettyName (mbNameBoundP b) varnames
-mpretty [nuP| TApp b1 b2 |] varnames =
-    "(" ++ mpretty b1 varnames
-        ++ " " ++ mpretty b2 varnames ++ ")"
-
-mprettyName (Left pf) varnames = unStringF (C.mapRListLookup pf varnames)
-mprettyName (Right n) varnames = "(free-var " ++ (show n) ++ ")"
-        
-
--- pretty print decls
-decls_pretty :: Decls a -> String
-decls_pretty decls =
-    "let\n" ++ (mdecls_pretty (emptyMb decls) C.empty 0)
-
-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)
-
-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)
-mdecl_pretty [nuP| Decl_Cons d|] varnames n =
-  let vname = "x" ++ show n in
-  vname ++ " " ++ mdecl_pretty (mbCombine d) (varnames :>: StringF vname) (n+1)
diff --git a/Data/Binding/Hobbits/Internal/Closed.hs b/Data/Binding/Hobbits/Internal/Closed.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Internal/Closed.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
-
--- |
--- Module      : Data.Binding.Hobbits.Closed
--- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- This module defines the type @'Cl' a@ of closed objects of type
--- @a@. Note that, in order to ensure adequacy of the Hobbits
--- name-binding approach, this representation is hidden from the user,
--- and so this file should never be imported directly by the user.
---
-
-module Data.Binding.Hobbits.Internal.Closed where
-
-import Language.Haskell.TH (Q, Exp(..), Type(..))
-import qualified Language.Haskell.TH as TH
-import qualified Language.Haskell.TH.ExpandSyns as TH
-
-import qualified Data.Generics as SYB
-import qualified Language.Haskell.TH.Syntax as TH
-
-{-| The type @Closed a@ represents a closed term of type @a@, i.e., an expression
-of type @a@ with no free (Haskell) variables.  Since this cannot be checked
-directly in the Haskell type system, the @Closed@ data type is hidden, and the
-user can only create closed terms using Template Haskell, through the 'mkClosed'
-operator. -}
-newtype Closed a = Closed { unClosed :: a }
-
--- | Extract the type of an 'Info' object
-#if MIN_VERSION_template_haskell(2,11,0)
-reifyNameType :: TH.Name -> Q Type
-reifyNameType n =
-  TH.reify n >>= \i ->
-  case i of
-    TH.VarI _ ty _ -> return ty
-    _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."
-#else
-reifyNameType :: TH.Name -> Q Type
-reifyNameType n =
-  TH.reify n >>= \i ->
-  case i of
-    TH.VarI _ ty _ _ -> return ty
-    _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."
-#endif
-
--- | @mkClosed@ is used with Template Haskell quotations to create closed terms
--- of type 'Closed'. A quoted expression is closed if all of the names occuring in
--- it are either:
---
---   1) bound globally or
---   2) bound within the quotation or
---   3) also of type 'Closed'.
-mkClosed :: Q Exp -> Q Exp
-mkClosed e = AppE (ConE 'Closed) `fmap` e >>= SYB.everywhereM (SYB.mkM w) where
-  w e@(VarE n@(TH.Name _ flav)) = case flav of
-    TH.NameG {} -> return e -- bound globally
-    TH.NameU {} -> return e -- bound locally within this quotation
-    TH.NameL {} -> closed n >> return e -- bound locally outside this quotation
-    _ -> fail $ "`mkClosed' does not allow dynamically bound names: `"
-      ++ show n ++ "'."
-  w e = return e
-
-  closed n = do
-    ty <- reifyNameType n
-    TH.expandSyns ty >>= w ty
-      where
-        w _ (AppT (ConT m) _) | m == ''Closed = return ()
-        w top_ty (ForallT _ _ ty') = w top_ty ty'
-        w top_ty _ =
-          fail $ "`mkClosed` requires non-global variables to have type `Closed'.\n\t`"
-          ++ show (TH.ppr n) ++ "' does not. It's type is:\n\t `"
-          ++ show (TH.ppr top_ty) ++ "'."
diff --git a/Data/Binding/Hobbits/Internal/Mb.hs b/Data/Binding/Hobbits/Internal/Mb.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Internal/Mb.hs
+++ /dev/null
@@ -1,101 +0,0 @@
-{-# LANGUAGE GADTs, DeriveDataTypeable, Rank2Types, ViewPatterns #-}
-
--- |
--- Module      : Data.Binding.Hobbits.Internal.Name
--- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : westbrook@kestrel.edu
--- Stability   : experimental
--- Portability : GHC
---
--- This module defines the type @'Mb' ctx a@. In order to ensure
--- adequacy of the Hobbits name-binding approach, this representation
--- is hidden, and so this file should never be imported directly by
--- the user.
---
-
-module Data.Binding.Hobbits.Internal.Mb where
-
-import Data.Typeable
-import Data.Proxy
-import Data.Type.Equality
-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 @'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
-  binding, or as "fresh pairs", which are pairs of a list of names
-  that are guaranteed to be fresh along with a body. Note that fresh
-  pairs must come with an 'MbTypeRepr' for the body type, to ensure
-  that the names given in the pair can be relaced by fresher names.
--}
-data Mb ctx b
-    = MkMbFun (MapRList Proxy ctx) (MapRList Name ctx -> b)
-    | MkMbPair (MbTypeRepr b) (MapRList Name ctx) b
-    deriving Typeable
-
-
-{-|
-   This type states that it is possible to replace free names with
-   fresh names in an object of type @a@. This type essentially just
-   captures a representation of the type a as either a Name type, a
-   multi-binding, a function type, or a (G)ADT. In order to be sure
-   that only the "right" proofs are used for (G)ADTs, however, this
-   type is hidden from the user, and can only be constructed with
-   'mkNuMatching'.
--}
-
-data MbTypeRepr a where
-    MbTypeReprName :: MbTypeRepr (Name a)
-    MbTypeReprMb :: MbTypeRepr a -> MbTypeRepr (Mb ctx a)
-    MbTypeReprFun :: MbTypeRepr a -> MbTypeRepr b -> MbTypeRepr (a -> b)
-    MbTypeReprData :: MbTypeReprData a -> MbTypeRepr a
-
-data MbTypeReprData a =
-    MkMbTypeReprData (forall ctx. MapRList Name ctx -> MapRList Name ctx -> a -> a)
-
-
-{-|
-  The call @mapNamesPf data ns ns' a@ replaces each occurrence of a
-  free name in @a@ which is listed in @ns@ by the corresponding name
-  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 -> 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
-mapNamesPf MbTypeReprName _ _ _ = error "Should not be possible! (in mapNamesPf)"
-mapNamesPf (MbTypeReprMb tRepr) names1 names2 (ensureFreshFun -> (proxies, f)) =
-    -- README: the fresh function created below is *guaranteed* to not
-    -- be passed elements of either names1 or names2, since it should
-    -- only ever be passed fresh names
-    MkMbFun proxies (\ns -> mapNamesPf tRepr names1 names2 (f ns))
-mapNamesPf (MbTypeReprFun tReprIn tReprOut) names names' f =
-    (mapNamesPf tReprOut names names') . f . (mapNamesPf tReprIn names' names)
-mapNamesPf (MbTypeReprData (MkMbTypeReprData mapFun)) names names' x =
-    mapFun names names' x
-
-
--- | Ensures a multi-binding is in "fresh function" form
-ensureFreshFun :: Mb ctx a -> (MapRList Proxy ctx, MapRList Name ctx -> a)
-ensureFreshFun (MkMbFun proxies f) = (proxies, f)
-ensureFreshFun (MkMbPair tRepr ns body) =
-    (mapMapRList (\_ -> Proxy) ns, \ns' -> mapNamesPf tRepr ns ns' body)
-
--- | Ensures a multi-binding is in "fresh pair" form
-ensureFreshPair :: Mb ctx a -> (MapRList Name ctx, a)
-ensureFreshPair (MkMbPair _ ns body) = (ns, body)
-ensureFreshPair (MkMbFun proxies f) =
-    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
deleted file mode 100644
--- a/Data/Binding/Hobbits/Internal/Name.hs
+++ /dev/null
@@ -1,134 +0,0 @@
-{-# LANGUAGE GADTs, DeriveDataTypeable, FlexibleInstances, TypeOperators #-}
-
--- |
--- Module      : Data.Binding.Hobbits.Internal.Name
--- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : westbrook@kestrel.edu
--- Stability   : experimental
--- Portability : GHC
---
--- This module defines the type @'Name' a@ as a wrapper around a fresh
--- integer. Note that, in order to ensure adequacy of the Hobbits
--- name-binding approach, this representation is hidden from the user,
--- and so this file should never be imported directly by the user.
---
-
-module Data.Binding.Hobbits.Internal.Name where
-
-import Data.List
-import Data.Functor.Constant
-import Data.Typeable
-import Data.Type.Equality ((:~:))
-import Unsafe.Coerce (unsafeCoerce)
-import Data.IORef (IORef, newIORef, readIORef, writeIORef)
-import System.IO.Unsafe (unsafePerformIO)
-
-import Data.Type.RList
-
-
--- | A @Name a@ is a bound name that is associated with type @a@.
-newtype Name a = MkName Int deriving (Typeable, Eq)
-
-instance Show (Name a) where
-  showsPrec _ (MkName n) = showChar '#' . shows n . showChar '#'
-
-instance Show (MapRList Name c) where
-    show names = "[" ++ (concat $ intersperse "," $ mapRListToList $
-                        mapMapRList (Constant . show) names) ++ "]"
-
-
--------------------------------------------------------------------------------
--- Externally visible operators
--------------------------------------------------------------------------------
-
-{-|
-  @cmpName n m@ compares names @n@ and @m@ of types @Name a@ and @Name b@,
-  respectively. When they are equal, @Some e@ is returned for @e@ a proof
-  of type @a :~: b@ that their types are equal. Otherwise, @None@ is returned.
-
-  For example:
-
-> nu $ \n -> nu $ \m -> cmpName n n   ==   nu $ \n -> nu $ \m -> Some Refl
-> nu $ \n -> nu $ \m -> cmpName n m   ==   nu $ \n -> nu $ \m -> None
--}
-cmpName :: Name a -> Name b -> Maybe (a :~: b)
-cmpName (MkName n1) (MkName n2)
-  | n1 == n2 = Just $ unsafeCoerce Refl
-  | otherwise = Nothing
-
-
-
--------------------------------------------------------------------------------
--- Hidden, unsafe operators
--------------------------------------------------------------------------------
-
-
--- building an arbitrary InCtx proof with a given length
--- (this is used internally in HobbitLib)
-
-data ExMember where ExMember :: Member c a -> ExMember
-
--- creating some Member proof of length i
-memberFromLen :: Int -> ExMember
-memberFromLen 0 = ExMember Member_Base
-memberFromLen n = case memberFromLen (n - 1) of
-  ExMember mem -> ExMember (Member_Step mem)
-
--- unsafely creating a *specific* member proof from length i;
--- this is for when we know the ith element of c must be type a
-unsafeLookupC :: Int -> Member c a
-unsafeLookupC n = case memberFromLen n of
-  ExMember mem -> unsafeCoerce mem
-
-
--- building a proxy for each type in some unknown context
-data ExProxy where ExProxy :: MapRList Proxy ctx -> ExProxy
-proxyFromLen :: Int -> ExProxy
-proxyFromLen 0 = ExProxy MNil
-proxyFromLen n = case proxyFromLen (n - 1) of
-                   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
--- unsafeProxyFromLen :: Int -> MapC Proxy ctx
--- unsafeProxyFromLen n = case proxyFromLen n of
---                          ExProxy proxy -> unsafeCoerce proxy
-
--- -- unsafely convert a list of Ints, used to represent names, to
--- -- names of certain, given types; note that the first name in the
--- -- list becomes the last name in the output, with the same reversal
--- -- used in the Mb representation (see, e.g., mbCombine)
--- unsafeNamesFromInts :: [Int] -> MapC Name ctx
--- unsafeNamesFromInts [] = unsafeCoerce Nil
--- unsafeNamesFromInts (x:xs) =
---     unsafeCoerce $ unsafeNamesFromInts xs :> MkName x
-
--------------------------------------------------------------------------------
--- encapsulated impurity
--------------------------------------------------------------------------------
-
--- README: we *cannot* inline counter, because we want all uses
--- of counter to be the same IORef
-counter :: IORef Int
-{-# NOINLINE counter #-}
-counter = unsafePerformIO (newIORef 0)
-
--- README: fresh_name takes a dummy argument that is used in a dummy
--- way to avoid let-floating its body (and thus getting a fresh name
--- exactly once)
--- README: it *is* ok to inline fresh_name because we don't care in
--- what order fresh names are created
-fresh_name :: a -> Int
-fresh_name a = unsafePerformIO $ do 
-    dummyRef <- newIORef a
-    x <- readIORef counter
-    writeIORef counter (x+1)
-    return x
-
--- -- make one fresh name for each name in a given input list
--- fresh_names :: MapC Name ctx -> MapC Name ctx
--- fresh_names Nil = Nil
--- fresh_names (names :> n) = fresh_names names :> MkName (fresh_name n)
diff --git a/Data/Binding/Hobbits/Internal/Utilities.hs b/Data/Binding/Hobbits/Internal/Utilities.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Internal/Utilities.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-{-# LANGUAGE Rank2Types #-}
-
-module Data.Binding.Hobbits.Internal.Utilities where
-
-import qualified Data.Generics as SYB
-
-
-
-everywhereButM :: Monad m =>
-  SYB.GenericQ Bool -> SYB.GenericM m -> SYB.GenericM m
-everywhereButM q f x
-  | q x       = return x
-  | otherwise = (SYB.gmapM (everywhereButM q f) x) >>= f
diff --git a/Data/Binding/Hobbits/Liftable.hs b/Data/Binding/Hobbits/Liftable.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Liftable.hs
+++ /dev/null
@@ -1,131 +0,0 @@
-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, TemplateHaskell #-}
-{-# LANGUAGE ViewPatterns, QuasiQuotes, DataKinds #-}
-
--- |
--- Module      : Data.Binding.Hobbits.Mb
--- Copyright   : (c) 2014 Edwin Westbrook
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- This module defines the type-class Liftable for lifting
--- non-binding-related data out of name-bindings. Note that this code
--- is not "trusted", i.e., it is not part of the name-binding
--- abstraction: instead, it is all written using the primitives
--- exported by the Mb
-
-module Data.Binding.Hobbits.Liftable where
-
-import Data.Type.RList
-import Data.Binding.Hobbits.Internal.Mb
-import Data.Binding.Hobbits.QQ
-import Data.Binding.Hobbits.Closed
-import Data.Binding.Hobbits.NuMatching
-
-import Data.Ratio
-
-
-{-|
-  The class @Liftable a@ gives a \"lifting function\" for a, which can
-  take any data of type @a@ out of a multi-binding of type @'Mb' ctx a@.
--}
-class NuMatching a => Liftable a where
-    mbLift :: Mb ctx a -> a
-
--------------------------------------------------------------------------------
--- * Lifting instances that must be defined inside the library abstraction boundary
--------------------------------------------------------------------------------
-
-instance Liftable Char where
-    mbLift (ensureFreshPair -> (_, c)) = c
-
-instance Liftable Int where
-    mbLift (ensureFreshPair -> (_, i)) = i
-
-instance Liftable Integer where
-    mbLift (ensureFreshPair -> (_, i)) = i
-
-instance Liftable (Closed a) where
-    mbLift (ensureFreshPair -> (_, c)) = c
-
-
--------------------------------------------------------------------------------
--- * Lifting instances and related functions that could be defined outside the library
--------------------------------------------------------------------------------
-
--- README: this requires overlapping instances, because it clashes
--- with Liftable2, but this instance is better because it does not
--- require c nor a to be liftable
-instance Liftable (Member c a) where
-    mbLift [nuP| Member_Base |] = Member_Base
-    mbLift [nuP| Member_Step m |] = Member_Step (mbLift m)
-
--- | Lift a list (but not its elements) out of a multi-binding
-mbList :: NuMatching a => Mb c [a] -> [Mb c a]
-mbList [nuP| [] |] = []
-mbList [nuP| x : xs |] = x : mbList xs
-
-instance (Integral a, NuMatching a) => NuMatching (Ratio a) where
-  nuMatchingProof =
-    isoMbTypeRepr (\r -> (numerator r, denominator r)) (\(n,d) -> n%d)
-instance (Integral a, Liftable a) => Liftable (Ratio a) where
-  mbLift mb_r =
-    (\(n,d) -> n%d) $ mbLift $ fmap (\r -> (numerator r, denominator r)) mb_r
-
-instance Liftable a => Liftable [a] where
-    mbLift [nuP| [] |] = []
-    mbLift [nuP| x : xs |] = (mbLift x) : (mbLift xs)
-
-instance Liftable () where
-    mbLift [nuP| () |] = ()
-
-instance (Liftable a, Liftable b) => Liftable (a,b) where
-    mbLift [nuP| (x,y) |] = (mbLift x, mbLift y)
-
-instance Liftable Bool where
-  mbLift [nuP| True |] = True
-  mbLift [nuP| False |] = False
-
-instance Liftable a => Liftable (Maybe a) where
-  mbLift [nuP| Nothing |] = Nothing
-  mbLift [nuP| Just mb_a |] = Just $ mbLift mb_a
-
-instance (Liftable a, Liftable b) => Liftable (Either a b) where
-  mbLift [nuP| Left mb_a |] = Left $ mbLift mb_a
-  mbLift [nuP| Right mb_b |] = Right $ mbLift mb_b
-
--- README: these lead to overlapping instances...
-
-{-
-
-{-|
-  The class @Liftable1 f@ gives a lifting function for each type @f a@
-  when @a@ itself is @Liftable@.
--}
-class Liftable1 f where
-    mbLift1 :: Liftable a => Mb ctx (f a) -> f a
-
-instance (Liftable1 f, Liftable a) => Liftable (f a) where
-    mbLift = mbLift1
-
-instance Liftable1 [] where
-    mbLift1 [nuP| [] |] = []
-    mbLift1 [nuP| x : xs |] = (mbLift x) : (mbLift1 xs)
-
-{-|
-  The class @Liftable2 f@ gives a lifting function for each type @f a b@
-  when @a@ and @b@ are @Liftable@.
--}
-class Liftable2 f where
-    mbLift2 :: (Liftable a, Liftable b) => Mb ctx (f a b) -> f a b
-
-instance Liftable2 (,) where
-    mbLift2 [nuP| (x,y) |] = (mbLift x, mbLift y)
-
-instance (Liftable2 f, Liftable a) => Liftable1 (f a) where
-    mbLift1 = mbLift2
-
--}
diff --git a/Data/Binding/Hobbits/Mb.hs b/Data/Binding/Hobbits/Mb.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Mb.hs
+++ /dev/null
@@ -1,298 +0,0 @@
-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, ViewPatterns, DataKinds #-}
-
--- |
--- Module      : Data.Binding.Hobbits.Mb
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- This module defines multi-bindings as the type 'Mb', as well as a number of
--- operations on multi-bindings. See the paper E. Westbrook, N. Frisby,
--- P. Brauner, \"Hobbits for Haskell: A Library for Higher-Order Encodings in
--- Functional Programming Languages\" for more information.
-
-module Data.Binding.Hobbits.Mb (
-  -- * Abstract types
-  Name(),      -- hides Name implementation
-  Binding(),   -- hides Binding implementation
-  Mb(),        -- hides MultiBind implementation
-  -- * Multi-binding constructors
-  nu, nuMulti, nus, emptyMb,
-  -- * Queries on names
-  cmpName, mbNameBoundP, mbCmpName,
-  -- * Operations on multi-bindings
-  elimEmptyMb, mbCombine, mbSeparate, mbToProxy, mbSwap, mbApply,
-  -- * Eliminators for multi-bindings
-  nuMultiWithElim, nuWithElim, nuMultiWithElim1, nuWithElim1
-) where
-
-import Control.Applicative
-import Control.Monad.Identity
-
-import Data.Type.Equality ((:~:)(..))
-import Data.Proxy (Proxy(..))
-
-import Unsafe.Coerce (unsafeCoerce)
-
-import Data.Type.RList
-
-import Data.Binding.Hobbits.Internal.Name
-import Data.Binding.Hobbits.Internal.Mb
---import qualified Data.Binding.Hobbits.Internal as I
-
--------------------------------------------------------------------------------
--- creating bindings
--------------------------------------------------------------------------------
-
--- | A @Binding@ is simply a multi-binding that binds one name
-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
-  showsPrec p (ensureFreshPair -> (names, b)) = showParen (p > 10) $
-    showChar '#' . shows names . showChar '.' . shows b
-
-{-|
-  @nu f@ creates a binding which binds a fresh name @n@ and whose
-  body is the result of @f n@.
--}
-nu :: (Name a -> b) -> Binding a b
-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 @'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 :: 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
-
-
--------------------------------------------------------------------------------
--- Queries on Names
--------------------------------------------------------------------------------
-
-{-|
-  Checks if a name is bound in a multi-binding, returning @Left mem@
-  when the name is bound, where @mem@ is a proof that the type of the
-  name is in the type list for the multi-binding, and returning
-  @Right n@ when the name is not bound, where @n@ is the name.
-
-  For example:
-
-> nu $ \n -> mbNameBoundP (nu $ \m -> m)  ==  nu $ \n -> Left Member_Base
-> nu $ \n -> mbNameBoundP (nu $ \m -> n)  ==  nu $ \n -> Right n
--}
-mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a)
-mbNameBoundP (ensureFreshPair -> (names, n)) = helper names n where
-    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
-  Nothing -> Right (MkName n)
-  Just i -> Left (I.unsafeLookupC i)
--}
-
-
-{-|
-  Compares two names inside bindings, taking alpha-equivalence into
-  account; i.e., if both are the @i@th name, or both are the same name
-  not bound in their respective multi-bindings, then they compare as
-  equal. The return values are the same as for 'cmpName', so that
-  @Some Refl@ is returned when the names are equal and @Nothing@ is
-  returned when they are not.
--}
-mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b)
-mbCmpName b1 b2 = case (mbNameBoundP b1, mbNameBoundP b2) of
-  (Left mem1, Left mem2) -> membersEq mem1 mem2
-  (Right n1, Right n2) -> cmpName n1 n2
-  _ -> Nothing
-
-
--------------------------------------------------------------------------------
--- Operations on multi-bindings
--------------------------------------------------------------------------------
-
--- | Creates an empty binding that binds 0 names.
-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 RNil a -> a
-elimEmptyMb (ensureFreshPair -> (_, body)) = body
-
-
--- Extract the proxy objects from an Mb inside of a fresh function
-freshFunctionProxies :: MapRList Proxy ctx1 -> (MapRList Name ctx1 -> Mb ctx2 a) ->
-                        MapRList Proxy ctx2
-freshFunctionProxies proxies1 f =
-    case f (mapMapRList (const $ MkName 0) proxies1) of
-      MkMbFun proxies2 _ -> proxies2
-      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 (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"
-    -- because these proxies should never depend on the names
-    -- themselves
-    let proxies2 = freshFunctionProxies proxies1 f1 in
-    MkMbFun
-    (appendMapRList proxies1 proxies2)
-    (\ns ->
-         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 @'MapRList' any c2@, is a \"phantom\" argument to indicate how
-  the context @c@ should be split.
--}
-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) = splitMapRList Proxy c2 ns
-mbSeparate c2 (MkMbFun proxies f) =
-    MkMbFun proxies1 (\ns1 -> MkMbFun proxies2 (\ns2 -> f (appendMapRList ns1 ns2)))
-        where
-          (proxies1, proxies2) = splitMapRList Proxy c2 proxies
-
-
--- | Returns a proxy object that enumerates all the types in ctx.
-mbToProxy :: Mb ctx a -> MapRList Proxy ctx
-mbToProxy (MkMbFun proxies _) = proxies
-mbToProxy (MkMbPair _ ns _) = mapMapRList (\_ -> Proxy) ns
-
-
-{-|
-  Take a multi-binding inside another multi-binding and move the
-  outer binding inside the ineer one.
--}
-mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
-mbSwap (ensureFreshFun -> (proxies1, f1)) =
-    let proxies2 = freshFunctionProxies proxies1 f1 in
-    MkMbFun proxies2
-      (\ns2 ->
-         MkMbFun proxies1
-         (\ns1 ->
-            snd (ensureFreshFun (f1 ns1)) ns2))
-
-{-|
-  Applies a function in a multi-binding to an argument in a
-  multi-binding that binds the same number and types of names.
--}
-mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
-mbApply (ensureFreshFun -> (proxies, f_fun)) (ensureFreshFun -> (_, f_arg)) =
-  MkMbFun proxies (\ns -> f_fun ns $ f_arg ns)
-
-
--------------------------------------------------------------------------------
--- Functor and Applicative instances
--------------------------------------------------------------------------------
-
-instance Functor (Mb ctx) where
-    fmap f mbArg =
-        mbApply (nuMulti (mbToProxy mbArg) (\_ -> f)) mbArg
-
-instance TypeCtx ctx => Applicative (Mb ctx) where
-    pure x = nuMulti typeCtxProxies (const x)
-    (<*>) = mbApply
-
-
--------------------------------------------------------------------------------
--- Eliminators for multi-bindings
--------------------------------------------------------------------------------
-
--- FIXME: add more examples!!
-{-|
-  The expression @nuWithElimMulti args f@ takes a sequence @args@ of
-  zero or more multi-bindings, each of type @Mb ctx ai@ for the same
-  type context @ctx@ of bound names, and a function @f@ and does the
-  following:
-
-  * Creates a multi-binding that binds names @n1,...,nn@, one name for
-    each type in @ctx@;
-
-  * Substitutes the names @n1,...,nn@ for the names bound by each
-    argument in the @args@ sequence, yielding the bodies of the @args@
-    (using the new name @n@); and then
-
-  * Passes the sequence @n1,...,nn@ along with the result of
-    substituting into @args@ to the function @f@, which then returns
-    the value for the newly created binding.
-
-  Note that the types in @args@ must each have a @NuMatching@ instance;
-  this is represented with the @NuMatchingList@ type class.
-
-  Here are some examples:
-
-> (<*>) :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
-> (<*>) f a =
->     nuWithElimMulti ('MNil' :>: f :>: a)
->                     (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')
--}
-nuMultiWithElim :: TypeCtx ctx =>
-                   (MapRList Name ctx -> MapRList Identity args -> b) ->
-                   MapRList (Mb ctx) args -> Mb ctx b
-nuMultiWithElim f args =
-  MkMbFun typeCtxProxies
-          (\ns ->
-            f ns $ mapMapRList (\arg ->
-                                 Identity $ snd (ensureFreshFun arg) ns) args)
-
-
-{-|
-  Similar to 'nuMultiWithElim' but binds only one name.
--}
-nuWithElim :: (Name a -> MapRList Identity args -> b) ->
-              MapRList (Mb (RNil :> a)) args ->
-              Binding a b
-nuWithElim f args =
-    nuMultiWithElim (\(MNil :>: n) -> f n) args
-
-
-{-|
-  Similar to 'nuMultiWithElim' but takes only one argument
--}
-nuMultiWithElim1 :: TypeCtx ctx => (MapRList Name ctx -> arg -> b) -> Mb ctx arg ->
-                    Mb ctx b
-nuMultiWithElim1 f arg =
-    nuMultiWithElim (\names (MNil :>: Identity arg) -> f names arg) (MNil :>: arg)
-
-
-{-|
-  Similar to 'nuMultiWithElim' but takes only one argument that binds
-  a single name.
--}
-nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b
-nuWithElim1 f 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
deleted file mode 100644
--- a/Data/Binding/Hobbits/NuMatching.hs
+++ /dev/null
@@ -1,525 +0,0 @@
-{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies #-}
-{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, DataKinds #-}
-
--- |
--- Module      : Data.Binding.Hobbits.NuMatching
--- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : westbrook@kestrel.edu
--- Stability   : experimental
--- Portability : GHC
---
--- This module defines the typeclass @'NuMatching' a@, which allows
--- pattern-matching on the bodies of multi-bindings when their bodies
--- have type a. To ensure adequacy, the actual machinery of how this
--- works is hidden from the user, but, for any given (G)ADT @a@, the
--- user can use the Template Haskell function 'mkNuMatching' to
--- create a 'NuMatching' instance for @a@.
---
-
-
-module Data.Binding.Hobbits.NuMatching (
-  NuMatching(..), mkNuMatching, NuMatchingList(..), NuMatching1(..),
-  MbTypeRepr(), isoMbTypeRepr, NuMatchingObj(..)
-) where
-
---import Data.Typeable
-import Language.Haskell.TH hiding (Name)
-import qualified Language.Haskell.TH as TH
-import Control.Monad.State
---import Control.Monad.Identity
-
-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 => MapRList Name ctx -> MapRList Name ctx -> a -> a
-mapNames = mapNamesPf nuMatchingProof
-
--- | Helper to match a data declaration in a TH version-insensitive way
-#if MIN_VERSION_template_haskell(2,11,0)
-matchDataDecl :: Dec -> Maybe (Cxt, TH.Name, [TyVarBndr], [Con])
-matchDataDecl (DataD cxt name tyvars _ constrs _) =
-  Just (cxt, name, tyvars, constrs)
-matchDataDecl (NewtypeD cxt name tyvars _ constr _) =
-  Just (cxt, name, tyvars, [constr])
-matchDataDecl _ = Nothing
-#else
-matchDataDecl :: Dec -> Maybe (Cxt, TH.Name, [TyVarBndr], [Con])
-matchDataDecl (DataD cxt name tyvars constrs _) =
-  Just (cxt, name, tyvars, constrs)
-matchDataDecl (NewtypeD cxt name tyvars constr _) =
-  Just (cxt, name, tyvars, [constr])
-matchDataDecl _ = Nothing
-#endif
-
--- | Helper to build an instance declaration in a TH version-insensitive way
-#if MIN_VERSION_template_haskell(2,11,0)
-mkInstanceD :: Cxt -> Type -> [Dec] -> Dec
-mkInstanceD = InstanceD Nothing
-#else
-mkInstanceD :: Cxt -> Type -> [Dec] -> Dec
-mkInstanceD = InstanceD
-#endif
-
-
-{-|
-  Instances of the @'NuMatching' a@ class allow pattern-matching on
-  multi-bindings whose bodies have type @a@, i.e., on multi-bindings
-  of type @'Mb' ctx a@. The structure of this class is mostly hidden
-  from the user; see 'mkNuMatching' to see how to create instances
-  of the @NuMatching@ class.
--}
-class NuMatching a where
-    nuMatchingProof :: MbTypeRepr a
-
-instance NuMatching (Name a) where
-    nuMatchingProof = MbTypeReprName
-
-instance NuMatching (Closed a) where
-    -- no need to map free variables in a Closed object
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
-
-instance (NuMatching a, NuMatching b) => NuMatching (a -> b) where
-    nuMatchingProof = MbTypeReprFun nuMatchingProof nuMatchingProof
-
-instance NuMatching a => NuMatching (Mb ctx a) where
-    nuMatchingProof = MbTypeReprMb nuMatchingProof
-
-instance NuMatching Bool where
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ _ -> id))
-
-instance NuMatching Int where
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
-
-instance NuMatching Integer where
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
-
-instance NuMatching Char where
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
-
-instance NuMatching () where
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
-
-instance (NuMatching a, NuMatching b) => NuMatching (a,b) where
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b) -> (mapNames c1 c2 a, mapNames c1 c2 b)))
-
-instance (NuMatching a, NuMatching b, NuMatching c) => NuMatching (a,b,c) where
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b,c) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c)))
-
-instance (NuMatching a, NuMatching b, NuMatching c, NuMatching d) => NuMatching (a,b,c,d) where
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b,c,d) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c, mapNames c1 c2 d)))
-
-instance NuMatching a => NuMatching (Maybe a) where
-    nuMatchingProof = MbTypeReprData
-                  (MkMbTypeReprData
-                   $ (\c1 c2 x -> case x of
-                                    Just x -> Just (mapNames c1 c2 x)
-                                    Nothing -> Nothing))
-
-instance (NuMatching a, NuMatching b) => NuMatching (Either a b) where
-    nuMatchingProof = MbTypeReprData
-                  (MkMbTypeReprData
-                   $ (\c1 c2 x -> case x of
-                                    Left l -> Left (mapNames c1 c2 l)
-                                    Right r -> Right (mapNames c1 c2 r)))
-
-instance NuMatching a => NuMatching [a] where
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> map (mapNames c1 c2)))
-
-instance NuMatching (Member c a) where
-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
-
-
-{-
-type family NuMatchingListProof args
-type instance NuMatchingListProof Nil = ()
-type instance NuMatchingListProof (args :> arg) = (NuMatchingListProof args, MbTypeReprData arg)
-
--- the NuMatchingList class, for saying that NuMatching holds for a context of types
-class NuMatchingList args where
-    nuMatchingListProof :: NuMatchingListProof args
-
-instance NuMatchingList Nil where
-    nuMatchingListProof = ()
-
-instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where
-    nuMatchingListProof = (nuMatchingListProof, nuMatchingProof)
--}
-
-data NuMatchingObj a = NuMatching a => NuMatchingObj ()
-
--- the NuMatchingList class, for saying that NuMatching holds for a context of types
-class NuMatchingList args where
-    nuMatchingListProof :: MapRList NuMatchingObj args
-
-instance NuMatchingList RNil where
-    nuMatchingListProof = MNil
-
-instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where
-    nuMatchingListProof = nuMatchingListProof :>: NuMatchingObj ()
-
-
-class NuMatching1 f where
-    nuMatchingProof1 :: NuMatching a => NuMatchingObj (f a)
-
--- README: deriving NuMatching from NuMatching1 leads to overlapping instances
--- for, e.g., Name a
-{-
-instance (NuMatching1 f, NuMatching a) => NuMatching (f a) where
-    nuMatchingProof = nuMatchingProof1 nuMatchingProof
--}
-
-instance (NuMatching1 f, NuMatchingList ctx) => NuMatching (MapRList f ctx) where
-    nuMatchingProof = MbTypeReprData $ MkMbTypeReprData $ helper nuMatchingListProof where
-        helper :: NuMatching1 f =>
-                  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) :>:
-                  mapNames c1 c2 elem
-
-
--- | Build an 'MbTypeRepr' for type @a@ by using an isomorphism with an
--- already-representable type @b@. This is useful for building 'NuMatching'
--- instances for, e.g., 'Integral' types, by mapping to and from 'Integer',
--- without having to define instances for each one in this module.
-isoMbTypeRepr :: NuMatching b => (a -> b) -> (b -> a) -> MbTypeRepr a
-isoMbTypeRepr f_to f_from =
-  MbTypeReprData $ MkMbTypeReprData $ \names1 names2 a ->
-  f_from $ mapNames names1 names2 (f_to a)
-
-
--- now we define some TH to create NuMatchings
-
-natsFrom i = i : natsFrom (i+1)
-
-fst3 :: (a,b,c) -> a
-fst3 (x,_,_) = x
-
-snd3 :: (a,b,c) -> b
-snd3 (_,y,_) = y
-
-thd3 :: (a,b,c) -> c
-thd3 (_,_,z) = z
-
-
-type Names = (TH.Name, TH.Name, TH.Name, TH.Name)
-
-mapNamesType a = [t| forall ctx. MapRList Name ctx -> MapRList Name ctx -> $a -> $a |]
-
-{-|
-  Template Haskell function for creating NuMatching instances for (G)ADTs.
-  Typical usage is to include the following line in the source file for
-  (G)ADT @T@ (here assumed to have two type arguments):
-
-> $(mkNuMatching [t| forall a b . T a b |])
-
-  The 'mkNuMatching' call here will create an instance declaration for
-  @'NuMatching' (T a b)@. It is also possible to include a context in the
-  forall type; for example, if we define the 'ID' data type as follows:
-
-> data ID a = ID a
-
-  then we can create a 'NuMatching' instance for it like this:
-
-> $( mkNuMatching [t| NuMatching a => ID a |])
-
-  Note that, when a context is included, the Haskell parser will add
-  the @forall a@ for you.
--}
-mkNuMatching :: Q Type -> Q [Dec]
-mkNuMatching tQ =
-    do t <- tQ
-       (cxt, cType, tName, constrs, tyvars) <- getMbTypeReprInfoTop t
-       fName <- newName "f"
-       x1Name <- newName "x1"
-       x2Name <- newName "x2"
-       clauses <- getClauses (tName, fName, x1Name, x2Name) constrs
-       mapNamesT <- mapNamesType (return cType)
-       return [mkInstanceD
-               cxt (AppT (ConT ''NuMatching) cType)
-               [ValD (VarP 'nuMatchingProof)
-                (NormalB
-                 $ AppE (ConE 'MbTypeReprData)
-                   $ AppE (ConE 'MkMbTypeReprData)
-                         $ LetE [SigD fName
-                                 $ ForallT (map PlainTV tyvars) cxt mapNamesT,
-                                 FunD fName clauses]
-                               (VarE fName)) []]]
-
-       {-
-       return (LetE
-               [SigD fName
-                     (ForallT tyvars reqCxt
-                     $ foldl AppT ArrowT
-                           [foldl AppT (ConT conName)
-                                      (map tyVarToType tyvars)]),
-                FunD fname clauses]
-               (VarE fname))
-        -}
-    where
-      -- extract the name from a TyVarBndr
-      tyBndrToName (PlainTV n) = n
-      tyBndrToName (KindedTV n _) = n
-
-      -- fail for getMbTypeReprInfo
-      getMbTypeReprInfoFail t extraMsg =
-          fail ("mkMbTypeRepr: " ++ show t
-                ++ " is not a type constructor for a (G)ADT applied to zero or more distinct type variables" ++ extraMsg)
-
-      -- get info for conName (top-level call)
-      getMbTypeReprInfoTop t = getMbTypeReprInfo [] [] t t
-
-      -- get info for conName
-      getMbTypeReprInfo ctx tyvars topT (ConT tName) =
-          do info <- reify tName
-             case info of
-               TyConI (matchDataDecl -> Just (_, _, tyvarsReq, constrs)) ->
-                 success tyvarsReq constrs
-               _ -> getMbTypeReprInfoFail topT (": info for " ++ (show tName) ++ " = " ++ (show info))
-          where
-            success tyvarsReq constrs =
-                let tyvarsRet = if tyvars == [] && ctx == []
-                                then map tyBndrToName tyvarsReq
-                                else tyvars in
-                return (ctx,
-                        foldl AppT (ConT tName) (map VarT tyvars),
-                        tName, constrs, tyvarsRet)
-
-      getMbTypeReprInfo ctx tyvars topT (AppT f (VarT argName)) =
-          if elem argName tyvars then
-              getMbTypeReprInfoFail topT ""
-          else
-              getMbTypeReprInfo ctx (argName:tyvars) topT f
-
-      getMbTypeReprInfo ctx tyvars topT (ForallT _ ctx' t) =
-          getMbTypeReprInfo (ctx ++ ctx') tyvars topT t
-
-      getMbTypeReprInfo ctx tyvars topT t = getMbTypeReprInfoFail topT ""
-
-      -- get the name from a data type
-      getTCtor t = getTCtorHelper t t []
-      getTCtorHelper (ConT tName) topT tyvars = Just (topT, tName, tyvars)
-      getTCtorHelper (AppT t1 (VarT var)) topT tyvars =
-          getTCtorHelper t1 topT (tyvars ++ [var])
-      getTCtorHelper (SigT t1 _) topT tyvars = getTCtorHelper t1 topT tyvars
-      getTCtorHelper _ _ _ = Nothing
-
-      -- get a list of Clauses, one for each constructor in constrs
-      getClauses :: Names -> [Con] -> Q [Clause]
-      getClauses _ [] = return []
-
-      getClauses names (NormalC cName cTypes : constrs) =
-        do clause <-
-             getClauseHelper names (map snd cTypes) (natsFrom 0)
-             (\l -> ConP cName (map (VarP . fst3) l))
-             (\l -> foldl AppE (ConE cName) (map fst3 l))
-           clauses <- getClauses names constrs
-           return $ clause : clauses
-
-      getClauses names (RecC cName cVarTypes : constrs) =
-        do clause <-
-             getClauseHelper names (map thd3 cVarTypes) (map fst3 cVarTypes)
-             (\l -> RecP cName (map (\(var,_,field) -> (field, VarP var)) l))
-             (\l -> RecConE cName (map (\(exp,_,field) -> (field, exp)) l))
-           clauses <- getClauses names constrs
-           return $ clause : clauses
-
-      getClauses names (InfixC cType1 cName cType2 : constrs) =
-        undefined -- FIXME
-
-#if MIN_VERSION_template_haskell(2,11,0)
-      getClauses names (GadtC cNames cTypes _ : constrs) =
-        do clauses1 <-
-             forM cNames $ \cName ->
-             getClauseHelper names (map snd cTypes) (natsFrom 0)
-             (\l -> ConP cName (map (VarP . fst3) l))
-             (\l -> foldl AppE (ConE cName) (map fst3 l))
-           clauses2 <- getClauses names constrs
-           return (clauses1 ++ clauses2)
-
-      getClauses names (RecGadtC cNames cVarTypes _ : constrs) =
-        do clauses1 <-
-             forM cNames $ \cName ->
-             getClauseHelper names (map thd3 cVarTypes) (map fst3 cVarTypes)
-             (\l -> RecP cName (map (\(var,_,field) -> (field, VarP var)) l))
-             (\l -> RecConE cName (map (\(exp,_,field) -> (field, exp)) l))
-           clauses2 <- getClauses names constrs
-           return (clauses1 ++ clauses2)
-#endif
-
-      getClauses names (ForallC _ _ constr : constrs) =
-        getClauses names (constr : constrs)
-
-      getClauseHelper :: Names -> [Type] -> [a] ->
-                         ([(TH.Name,Type,a)] -> Pat) ->
-                         ([(Exp,Type,a)] -> Exp) ->
-                         Q Clause
-      getClauseHelper names@(tName, fName, x1Name, x2Name) cTypes cData pFun eFun =
-          do varNames <- mapM (newName . ("x" ++) . show . fst)
-                         $ zip (natsFrom 0) cTypes
-             let varsTypesData = zip3 varNames cTypes cData
-             let expsTypesData = map (mkExpTypeData names) varsTypesData
-             return $ Clause [(VarP x1Name), (VarP x2Name), (pFun varsTypesData)]
-                        (NormalB $ eFun expsTypesData) []
-
-      mkExpTypeData :: Names -> (TH.Name,Type,a) -> (Exp,Type,a)
-      mkExpTypeData (tName, fName, x1Name, x2Name)
-                    (varName, getTCtor -> Just (t, tName', _), cData)
-          | tName == tName' =
-              -- the type of the arg is the same as the (G)ADT we are
-              -- recursing over; apply the recursive function
-              (foldl AppE (VarE fName)
-                         [(VarE x1Name), (VarE x2Name), (VarE varName)],
-               t, cData)
-      mkExpTypeData (tName, fName, x1Name, x2Name) (varName, t, cData) =
-          -- the type of the arg is not the same as the (G)ADT; call mapNames
-          (foldl AppE (VarE 'mapNames)
-                     [(VarE x1Name), (VarE x2Name), (VarE varName)],
-           t, cData)
-
--- FIXME: old stuff below
-
-type CxtStateQ a = StateT Cxt Q a
-
--- create a MkMbTypeReprData for a (G)ADT
-mkMkMbTypeReprDataOld :: Q TH.Name -> Q Exp
-mkMkMbTypeReprDataOld conNameQ =
-    do conName <- conNameQ
-       (cxt, name, tyvars, constrs) <- getMbTypeReprInfo conName
-       (clauses, reqCxt) <- runStateT (getClauses cxt name tyvars [] constrs) []
-       fname <- newName "f"
-       return (LetE
-               [SigD fname
-                     (ForallT tyvars reqCxt
-                     $ foldl AppT ArrowT
-                           [foldl AppT (ConT conName)
-                                      (map tyVarToType tyvars)]),
-                FunD fname clauses]
-               (VarE fname))
-    where
-      -- convert a TyVar to a Name
-      tyVarToType (PlainTV n) = VarT n
-      tyVarToType (KindedTV n _) = VarT n
-
-      -- get info for conName
-      getMbTypeReprInfo conName =
-          reify conName >>= \info ->
-              case info of
-                TyConI (matchDataDecl -> Just (cxt, name, tyvars, constrs)) ->
-                    return (cxt, name, tyvars, constrs)
-                _ -> fail ("mkMkMbTypeReprData: " ++ show conName
-                           ++ " is not a (G)ADT")
-      {-
-      -- report failure
-      getMbTypeReprInfoFail t =
-          fail ("mkMkMbTypeReprData: " ++ show t
-                ++ " is not a fully applied (G)ADT")
-
-      getMbTypeReprInfo (ConT conName) topT =
-          reify conName >>= \info ->
-              case info of
-                TyConI (DataD cxt name tyvars constrs _) ->
-                    return (cxt, name, tyvars, constrs)
-                _ -> getMbTypeReprInfoFail topT
-      getMbTypeReprInfo (AppT t _) topT = getMbTypeReprInfo t topT
-      getMbTypeReprInfo (SigT t _) topT = getMbTypeReprInfo t topT
-      getMbTypeReprInfo _ topT = getMbTypeReprInfoFail topT
-       -}
-
-      -- get a list of Clauses, one for each constructor in constrs
-      getClauses :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] -> [Con] ->
-                    CxtStateQ [Clause]
-      getClauses cxt name tyvars locTyvars [] = return []
-
-      getClauses cxt name tyvars locTyvars (NormalC cName cTypes : constrs) =
-        do clause <-
-             getClauseHelper cxt name tyvars locTyvars (map snd cTypes)
-             (natsFrom 0)
-             (\l -> ConP cName (map (VarP . fst3) l))
-             (\l -> foldl AppE (ConE cName) (map (VarE . fst3) l))
-           clauses <- getClauses cxt name tyvars locTyvars constrs
-           return (clause : clauses)
-
-      getClauses cxt name tyvars locTyvars (RecC cName cVarTypes : constrs) =
-        do clause <-
-             getClauseHelper cxt name tyvars locTyvars (map thd3 cVarTypes)
-             (map fst3 cVarTypes)
-             (\l -> RecP cName (map (\(var,_,field) -> (field, VarP var)) l))
-             (\l -> RecConE cName (map (\(var,_,field) -> (field, VarE var)) l))
-           clauses <- getClauses cxt name tyvars locTyvars constrs
-           return (clause : clauses)
-
-      getClauses cxt name tyvars locTyvars (InfixC cType1 cName cType2 : _) =
-        undefined -- FIXME
-
-      getClauses cxt name tyvars locTyvars (ForallC tyvars2 cxt2 constr
-                                            : constrs) =
-        do clauses1 <-
-             getClauses (cxt ++ cxt2) name tyvars (locTyvars ++ tyvars2) [constr]
-           clauses2 <- getClauses cxt name tyvars locTyvars constrs
-           return (clauses1 ++ clauses2)
-
-#if MIN_VERSION_template_haskell(2,11,0)
-      getClauses cxt name tyvars locTyvars (GadtC cNames cTypes _ : constrs) =
-        do clauses1 <-
-             forM cNames $ \cName ->
-             getClauseHelper cxt name tyvars locTyvars (map snd cTypes)
-             (natsFrom 0) (\l -> ConP cName (map (VarP . fst3) l))
-             (\l -> foldl AppE (ConE cName) (map (VarE . fst3) l))
-           clauses2 <- getClauses cxt name tyvars locTyvars constrs
-           return (clauses1 ++ clauses2)
-
-      getClauses cxt name tyvars locTyvars (RecGadtC cNames cVarTypes _
-                                            : constrs) =
-        do clauses1 <-
-             forM cNames $ \cName ->
-             getClauseHelper cxt name tyvars locTyvars
-             (map thd3 cVarTypes) (map fst3 cVarTypes)
-             (\l -> RecP cName (map (\(var,_,field) -> (field, VarP var)) l))
-             (\l -> RecConE cName (map (\(var,_,field) -> (field, VarE var)) l))
-           clauses2 <- getClauses cxt name tyvars locTyvars constrs
-           return (clauses1 ++ clauses2)
-#endif
-
-      getClauseHelper :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] ->
-                         [Type] -> [a] ->
-                         ([(TH.Name,Type,a)] -> Pat) ->
-                         ([(TH.Name,Type,a)] -> Exp) ->
-                         CxtStateQ Clause
-      getClauseHelper cxt name tyvars locTyvars cTypes cData pFun eFun =
-          do varNames <- mapM (lift . newName . ("x" ++) . show . fst)
-                         $ zip (natsFrom 0) cTypes
-             () <- ensureCxt cxt locTyvars cTypes
-             let varsTypesData = zip3 varNames cTypes cData
-             return $ Clause [(pFun varsTypesData)]
-                        (NormalB $ eFun varsTypesData) []
-
-      -- ensure that MbTypeRepr a holds for each type a in cTypes
-      ensureCxt :: Cxt -> [TyVarBndr] -> [Type] -> CxtStateQ ()
-      ensureCxt cxt locTyvars cTypes =
-          foldM (const (ensureCxt1 cxt locTyvars)) () cTypes
-
-      -- FIXME: it is not possible (or, at least, not easy) to determine
-      -- if MbTypeRepr a is implied from a current Cxt... so we just add
-      -- everything we need to the returned Cxt, except for 
-      ensureCxt1 :: Cxt -> [TyVarBndr] -> Type -> CxtStateQ ()
-      ensureCxt1 cxt locTyvars t = undefined
-      {-
-      ensureCxt1 cxt locTyvars t = do
-        curCxt = get
-        let fullCxt = cxt ++ curCxt
-        isOk <- isMbTypeRepr fullCxt 
-
-      isMbTypeRepr 
-       -}
diff --git a/Data/Binding/Hobbits/PatternParser.hs b/Data/Binding/Hobbits/PatternParser.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/PatternParser.hs
+++ /dev/null
@@ -1,42 +0,0 @@
--- |
--- Module      : Data.Binding.Hobbits.PatternParser
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- Using the haskell-src-meta package to parse Haskell patterns.
-
-module Data.Binding.Hobbits.PatternParser (parsePattern) where
-
-import Language.Haskell.TH
-
-import qualified Language.Haskell.Exts.Parser as Meta
-
-import qualified Language.Haskell.Meta.Parse as Meta
-
-import qualified Language.Haskell.Meta.Parse as Sloppy
-import qualified Language.Haskell.Meta.Syntax.Translate as Translate
-
-import qualified Language.Haskell.Exts.Extension as Exts
-
-#if MIN_VERSION_haskell_src_exts(1,14,0)
-parsePatternExtensions =
-  map Exts.EnableExtension $ Exts.ViewPatterns : Sloppy.myDefaultExtensions
-#else
-parsePatternExtensions = Exts.ViewPatterns : Sloppy.myDefaultExtensions
-#endif
-
-
-
-
-
-parsePattern :: String -> String -> Either String Pat
-parsePattern fn =
-  fmap Translate.toPat . Meta.parseResultToEither .
-  Meta.parsePatWithMode (Sloppy.myDefaultParseMode
-                    {Meta.parseFilename = fn,
-                     Meta.extensions = parsePatternExtensions })
diff --git a/Data/Binding/Hobbits/QQ.hs b/Data/Binding/Hobbits/QQ.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/QQ.hs
+++ /dev/null
@@ -1,148 +0,0 @@
-{-# LANGUAGE TemplateHaskell, FlexibleContexts #-}
-
--- |
--- Module      : Data.Binding.Hobbits.QQ
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- Defines a quasi-quoter for writing patterns that match the bodies of 'Mb'
--- multi-bindings. Uses the haskell-src-exts parser. @[nuP| P ]@ defines a
--- pattern that will match a multi-binding whose body matches @P@. Any
--- variables matched by @P@ will remain inside the binding; thus, for example,
--- in the pattern @[nuP| x |]@, @x@ matches the entire multi-binding.
---
--- Examples:
---
--- > case (nu Left) of [nuP| Left x |] -> x  ==  nu id
---
--- @[clP| P |]@ does the same for the 'Closed' type, and @[clNuP| P |]@ works
--- for both simultaneously: @'Closed' ('Mb' ctx a)@.
-
-module Data.Binding.Hobbits.QQ (nuP, clP, clNuP) where
-
-import Language.Haskell.TH.Syntax as TH
-import Language.Haskell.TH.Ppr as TH
-import Language.Haskell.TH.Quote
-
-import qualified Data.Generics as SYB
-import Control.Monad.Writer (runWriterT, tell)
-import Data.Monoid (Any(..))
-
-import qualified Data.Binding.Hobbits.Internal.Utilities as IU
-import Data.Binding.Hobbits.Internal.Mb
-import Data.Binding.Hobbits.Internal.Closed
-import Data.Binding.Hobbits.PatternParser (parsePattern)
-import Data.Binding.Hobbits.NuMatching
-
-
--- | Helper function to apply an expression to multiple arguments
-appEMulti :: Exp -> [Exp] -> Exp
-appEMulti = foldl AppE
-
--- | Helper function to apply the (.) operator on expressions
-compose :: Exp -> Exp -> Exp
-compose f g = VarE '(.) `AppE` f `AppE` g
-
--- | @patQQ str pat@ builds a quasi-quoter named @str@ that parses
--- | patterns with @pat@
-patQQ :: String -> (String -> Q Pat) -> QuasiQuoter
-patQQ n pat = QuasiQuoter (err "Exp") pat (err "Type") (err "Decs")
-  where err s = error $ "QQ `" ++ n ++ "' is for patterns, not " ++ s ++ "."
-
-
--- | A @WrapKit@ specifies a transformation to be applied to variables
--- | in a Template Haskell patterns, as follows:
---
--- * @_varView@ gives an expression for a function to be applied, as a
---   view pattern, to variables before matching them, including to
---   variables bound by @\@@ patterns;
---
--- * @_asXform@ gives a function to transform the bodies of \@
---   patterns, i.e., this function is applied to @p@ in pattern @x\@p@;
---
--- * @_topXform@ gives a function to transform the whole pattern after
---    @_varView@ and/or @_asXform@ have been applied to sub-patterns;
---    as the first argument, @_topXform@ also takes a flag indicating
---    whether any transformations have been applied to sub-patterns.
---
-data WrapKit =
-  WrapKit {_varView :: Exp, _asXform :: Pat -> Pat, _topXform :: Bool -> Pat -> Pat}
-
--- | Combine two WrapKits, composing the individual components
-combineWrapKits :: WrapKit -> WrapKit -> WrapKit
-combineWrapKits (WrapKit {_varView = varViewO, _asXform = asXformO, _topXform = topXformO})
-           (WrapKit {_varView = varViewI, _asXform = asXformI, _topXform = topXformI}) =
-  WrapKit {_varView = varViewO `compose` varViewI,
-           _asXform = asXformO . asXformI,
-           _topXform = \b -> topXformO b . topXformI b}
-
--- | Apply a 'WrapKit' to a pattern
-wrapVars :: Monad m => WrapKit -> Pat -> m Pat
-wrapVars (WrapKit {_varView = varView, _asXform = asXform, _topXform = topXform}) pat = do
-  (pat', Any usedVarView) <- runWriterT m
-  return $ topXform usedVarView pat'
-  where
-    m = IU.everywhereButM (SYB.mkQ False isExp) (SYB.mkM w) pat
-      where isExp :: Exp -> Bool
-            -- don't recur into the expression part of view patterns
-            isExp _ = True
-
-    -- this should be called if the 'varView' function is ever used
-    hit x = tell (Any True) >> return x
-
-    -- wraps up bound names
-    w p@VarP{} = hit $ ViewP varView p
-    -- wraps for the bound name, then immediately unwraps
-    -- for the rest of the pattern
-    w (AsP v p) = hit $ ViewP varView $ AsP v $ asXform p
-    -- requires the expression to be closed
-    w (ViewP (VarE n) p) = return $ ViewP (VarE 'unClosed `AppE` VarE n) p
-    w (ViewP e _) = fail $ "view function must be a single name: `" ++ show (TH.ppr e) ++ "'"
-    w p = return p
-
--- | Parse a pattern from a string, using 'parsePattern'
-parseHere :: String -> Q Pat
-parseHere s = do
-  fn <- loc_filename `fmap` location
-  case parsePattern fn s of
-    Left e -> error $ "Parse error: `" ++ e ++
-      "'\n\n\t when parsing pattern: `" ++ s ++ "'."
-    Right p -> return p
-
-
--- | A helper function used to ensure two multi-bindings have the same contexts
-same_ctx :: Mb ctx a -> Mb ctx b -> Mb ctx b
-same_ctx _ x = x
-
--- | Builds a 'WrapKit' for parsing patterns that match over 'Mb'.
--- | Takes two fresh names as arguments.
-nuKit :: TH.Name -> TH.Name -> WrapKit
-nuKit topVar namesVar = WrapKit {_varView = varView, _asXform = asXform, _topXform = topXform} where
-  varView = (VarE 'same_ctx `AppE` VarE topVar) `compose`
-        (appEMulti (ConE 'MkMbPair) [VarE 'nuMatchingProof, VarE namesVar])
-  asXform p = ViewP (VarE 'ensureFreshPair) (TupP [WildP, p])
-  topXform b p = if b then AsP topVar $ ViewP (VarE 'ensureFreshPair) (TupP [VarP namesVar, p]) else asXform p
-
--- | Quasi-quoter for patterns that match over 'Mb'
-nuP = patQQ "nuP" $ \s -> do
-  topVar <- newName "topMb"
-  namesVar <- newName "topNames"
-  parseHere s >>= wrapVars (nuKit topVar namesVar)
-
--- | Builds a 'WrapKit' for parsing patterns that match over 'Closed'
-clKit = WrapKit {_varView = ConE 'Closed, _asXform = asXform, _topXform = const asXform}
-  where asXform p = ConP 'Closed [p]
-
--- | Quasi-quoter for patterns that match over 'Closed', built using 'clKit'
-clP = patQQ "clP" $ (>>= wrapVars clKit) . parseHere
-
--- | Quasi-quoter for patterns that match over @'Closed' ('Mb' ctx a)@
-clNuP = patQQ "clNuP" $ \s -> do
-  topVar <- newName "topMb"
-  namesVar <- newName "topNames"
-  parseHere s >>= wrapVars (clKit `combineWrapKits` nuKit topVar namesVar)
diff --git a/Data/Type/RList.hs b/Data/Type/RList.hs
deleted file mode 100644
--- a/Data/Type/RList.hs
+++ /dev/null
@@ -1,208 +0,0 @@
-{-# 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.
-mapRListLookup :: Member c a -> MapRList f c -> f a
-mapRListLookup Member_Base (_ :>: x) = x
-mapRListLookup (Member_Step mem') (mc :>: _) = mapRListLookup mem' mc
---mapRListLookup _ _ = error "Should not happen! (mapRListLookup)"
-
--- | 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/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2014, Eddy Westbrook, Nicolas Frisby, Paul Brauner
+Copyright (c) 2014, Eddy Westbrook
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without modification,
diff --git a/hobbits.cabal b/hobbits.cabal
--- a/hobbits.cabal
+++ b/hobbits.cabal
@@ -1,5 +1,5 @@
 Name:                hobbits
-Version:             1.2.4
+Version:             1.3
 Synopsis:            A library for canonically representing terms with binding
 
 Description: A library for canonically representing terms with binding via a
@@ -13,28 +13,32 @@
 
 Category:            Data Structures
 
-Cabal-version: >= 1.6.0.1
+Cabal-version: >= 1.10
 Build-Type:    Simple
 
 extra-source-files: CHANGELOG
 
 Library
-  Build-Depends: base >= 4.7 && < 5
-  Build-Depends: template-haskell >= 2.9 && < 2.13
-
-  Build-Depends: syb
-  Build-Depends: mtl
-
-  Build-Depends: tagged
-  Build-Depends: deepseq
-
-  Build-Depends: haskell-src-exts >= 1.17.1 && < 1.20, haskell-src-meta,
-                 th-expand-syns >= 0.3 && < 0.5, transformers
+  build-depends:
+      base >= 4.7 && < 5
+    , template-haskell >= 2.11 && < 3
+    , syb
+    , mtl
+    , tagged
+    , deepseq
+    , haskell-src-exts >= 1.17.1 && < 2
+    , haskell-src-meta
+    , th-expand-syns >= 0.3 && < 0.5
+    , transformers
+    , containers
+    , vector
 
   GHC-Options: -fwarn-incomplete-patterns -fwarn-unused-imports
 
-  Extensions: CPP
+  hs-source-dirs: src
 
+  default-language: Haskell2010
+
   Exposed-Modules: Data.Type.RList,
 
                    Data.Binding.Hobbits,
@@ -42,9 +46,13 @@
                    Data.Binding.Hobbits.Closed,
                    Data.Binding.Hobbits.QQ,
                    Data.Binding.Hobbits.Liftable,
+                   Data.Binding.Hobbits.MonadBind,
+                   Data.Binding.Hobbits.NameMap,
+                   Data.Binding.Hobbits.NameSet,
 
                    Data.Binding.Hobbits.PatternParser,
                    Data.Binding.Hobbits.NuMatching,
+                   Data.Binding.Hobbits.NuMatchingInstances,
 
                    Data.Binding.Hobbits.Examples.LambdaLifting,
                    Data.Binding.Hobbits.Examples.LambdaLifting.Terms,
diff --git a/src/Data/Binding/Hobbits.hs b/src/Data/Binding/Hobbits.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE TypeOperators #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits
+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This library implements multi-bindings as described in the paper
+-- E. Westbrook, N. Frisby, P. Brauner, \"Hobbits for Haskell: A Library for
+-- Higher-Order Encodings in Functional Programming Languages\".
+
+module Data.Binding.Hobbits (
+  -- * Values under multi-bindings
+  module Data.Binding.Hobbits.Mb,
+  -- | The 'Data.Binding.Hobbits.Mb.Mb' type modeling multi-bindings is the
+  -- central abstract type of the library
+
+  -- * Closed terms
+  module Data.Binding.Hobbits.Closed,
+  -- | The 'Data.Binding.Hobbits.Closed.Cl' type models
+  -- super-combinators, which are safe functions to apply under
+  -- 'Data.Binding.Hobbits.Mb.Mb'.
+
+  -- * Pattern-matching multi-bindings and closed terms
+  module Data.Binding.Hobbits.QQ,
+  -- | The 'Data.Binding.Hobbits.QQ.nuP' quasiquoter allows safe pattern
+  -- matching on 'Data.Binding.Hobbits.Mb.Mb'
+  -- values. 'Data.Binding.Hobbits.QQ.superCombP' is similar.
+
+  -- * Lifting values out of multi-bindings
+  module Data.Binding.Hobbits.Liftable,
+
+  -- * Ancilliary modules
+  module Data.Proxy, module Data.Type.Equality,
+  -- | Type lists track the types of bound variables.
+
+  --module Data.Type.RList,
+  RList(..), RAssign(..), Member(..), (:++:), Append(..),
+  -- | The "Data.Binding.Hobbits.NuMatching" module exposes the NuMatching
+  -- class, which allows pattern-matching on (G)ADTs in the bodies of
+  -- multi-bindings
+  module Data.Binding.Hobbits.NuMatching,
+  module Data.Binding.Hobbits.NuMatchingInstances
+
+                            ) where
+
+import Data.Proxy
+import Data.Type.Equality
+import Data.Type.RList (RList(..), RAssign(..), Member(..), (:++:), Append(..))
+import Data.Binding.Hobbits.Mb
+import Data.Binding.Hobbits.Closed
+import Data.Binding.Hobbits.QQ
+import Data.Binding.Hobbits.Liftable
+import Data.Binding.Hobbits.NuMatching
+import Data.Binding.Hobbits.NuMatchingInstances()
diff --git a/src/Data/Binding/Hobbits/Closed.hs b/src/Data/Binding/Hobbits/Closed.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/Closed.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE TemplateHaskell, ViewPatterns, PolyKinds, GADTs, PatternGuards #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Closed
+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module uses Template Haskell to distinguish closed terms, so that the
+-- library can trust such functions to not contain any @Name@ values in their
+-- closure.
+
+module Data.Binding.Hobbits.Closed (
+  -- * Abstract types
+  Closed(),
+  -- * Operators involving 'Closed'
+  unClosed, mkClosed, noClosedNames, clApply, clMbApply, clApplyCl, unsafeClose,
+  -- * Typeclass for inherently closed types
+  Closable(..)
+) where
+
+import Data.Proxy
+import Data.Type.RList
+import Data.Binding.Hobbits.Internal.Name
+import Data.Binding.Hobbits.Internal.Mb
+import Data.Binding.Hobbits.Internal.Closed
+import Data.Binding.Hobbits.Mb
+
+-- | @noClosedNames@ encodes the hobbits guarantee that no name can escape its
+-- multi-binding.
+noClosedNames :: Closed (Name a) -> b
+noClosedNames (Closed n) =
+  -- We compare n to itself to force evaluation, in case the body of
+  -- the closed value is non-terminating...
+  case cmpName n n of
+    _ ->
+      error $
+      "... Clever girl!" ++
+      "The `noClosedNames' invariant has somehow been violated."
+
+-- | Closed terms are closed (sorry) under application.
+clApply :: Closed (a -> b) -> Closed a -> Closed b
+-- could be defined with cl were it not for the GHC stage restriction
+clApply (Closed f) (Closed a) = Closed (f a)
+
+-- | Closed multi-bindings are also closed under application.
+clMbApply :: Closed (Mb ctx (a -> b)) -> Closed (Mb ctx a) ->
+             Closed (Mb ctx b)
+clMbApply (Closed f) (Closed a) = Closed (mbApply f a)
+
+-- | When applying a closed function, the argument can be viewed as locally
+-- closed
+clApplyCl :: Closed (Closed a -> b) -> Closed a -> Closed b
+clApplyCl (Closed f) a = Closed (f a)
+
+-- | FIXME: this should not be possible!!
+closeBug :: a -> Closed a
+closeBug = $([| \x -> $(mkClosed [| x |]) |])
+
+-- | Mark an object as closed without actually traversing it. This is unsafe if
+-- the object does in fact contain any names.
+unsafeClose :: a -> Closed a
+unsafeClose = Closed
+
+-- | Typeclass for inherently closed types
+class Closable a where
+  toClosed :: a -> Closed a
+
+instance Closable Integer where
+  toClosed i = Closed i
+
+instance Closable (Member ctx a) where
+  -- NOTE: this is actually definable with mkClosed, but this is more efficient
+  toClosed memb = Closed memb
+
+instance Closable (Proxy a) where
+  toClosed Proxy = $(mkClosed [| Proxy |])
+
+instance Closable (Closed a) where
+  toClosed = clApplyCl $(mkClosed [| id |])
+
+instance Closable Bool where
+  toClosed True = $(mkClosed [| True |])
+  toClosed False = $(mkClosed [| False |])
+
+instance Closable Char where
+  toClosed = unsafeClose
+
+instance Closable Int where
+  toClosed = unsafeClose
+
+instance Closable a => Closable [a] where
+  toClosed [] = $(mkClosed [| [] |])
+  toClosed (a:as) =
+    $(mkClosed [| (:) |]) `clApply` toClosed a `clApply` toClosed as
+
+-- | Object-level reification of the 'Closable' typeclass
+data IsClosable a where IsClosable :: Closable a => IsClosable a
+
+-- | Type functors @f@ where @f a@ is always 'Closable' for any @a@
+class ClosableAny1 f where
+  closableAny1 :: f a -> IsClosable (f a)
+
+-- | Helper function to use the proof returned by 'closableAny1'
+toClosedAny1 :: ClosableAny1 f => f a -> Closed (f a)
+toClosedAny1 x | IsClosable <- closableAny1 x = toClosed x
+
+instance ClosableAny1 Proxy where
+  closableAny1 _ = IsClosable
+
+instance ClosableAny1 (Member ctx) where
+  closableAny1 _ = IsClosable
+
+instance ClosableAny1 f => Closable (RAssign f ctx) where
+  toClosed MNil = $(mkClosed [| MNil |])
+  toClosed (xs :>: x) =
+    $(mkClosed [| (:>:) |]) `clApply` toClosed xs `clApply` toClosedAny1 x
diff --git a/src/Data/Binding/Hobbits/Examples/LambdaLifting.hs b/src/Data/Binding/Hobbits/Examples/LambdaLifting.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/Examples/LambdaLifting.hs
@@ -0,0 +1,231 @@
+{-# LANGUAGE QuasiQuotes, ViewPatterns #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators, DataKinds #-}
+{-# LANGUAGE GADTs #-}
+
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Examples.LambdaLifting
+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- The lambda lifting example from the paper E. Westbrook, N. Frisby,
+-- P. Brauner, \"Hobbits for Haskell: A Library for Higher-Order Encodings in
+-- Functional Programming Languages\".
+
+-------------------------------------------------------------------------
+-- lambda lifting for the lambda calculus with top-level declarations
+-------------------------------------------------------------------------
+
+module Data.Binding.Hobbits.Examples.LambdaLifting (
+  -- * Term data types, using 'Data.Binding.Hobbits.Mb'
+  module Data.Binding.Hobbits.Examples.LambdaLifting.Terms,
+  -- * The lambda-lifting function
+  lambdaLift, mbLambdaLift
+  ) where
+
+import Data.Binding.Hobbits
+import qualified Data.Type.RList as C
+
+import Data.Binding.Hobbits.Examples.LambdaLifting.Terms
+
+-- imported for ease of use at terminal
+import Data.Binding.Hobbits.Examples.LambdaLifting.Examples
+
+import Control.Monad.Cont (Cont, runCont, cont)
+
+------------------------------------------------------------
+-- "peeling" lambdas off of a term
+------------------------------------------------------------
+
+data LType a where LType :: LType (L a)
+type LC c = RAssign LType c
+
+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
+  PeelRet :: lc ~ (lc0 :> b) => LC lc -> Mb (c :++: lc) (Term a) ->
+             PeelRet c (AddArrows lc a)
+
+peelLambdas :: Mb c (Binding (L b) (Term a)) -> PeelRet c (b -> a)
+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
+
+
+
+
+boundParams ::
+  lc ~ (lc0 :> b) => LC lc -> (RAssign 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))
+
+freeParams ::
+  LC lc -> (RAssign 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 = RAssign Name c -> RAssign Name c'
+
+------------------------------------------------------------
+-- operations on contexts of free variables
+------------------------------------------------------------
+
+data MbLName c a where
+    MbLName :: Mb c (Name (L a)) -> MbLName c (L a)
+
+type FVList c fvs = RAssign (MbLName c) fvs
+
+-- unioning free variable contexts: the data structure
+data FVUnionRet c fvs1 fvs2 where
+    FVUnionRet :: FVList c fvs -> SubC fvs1 fvs -> SubC fvs2 fvs ->
+                  FVUnionRet c fvs1 fvs2
+
+fvUnion :: FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2
+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.get 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.get idx xs) f2
+
+elemMC :: MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
+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)
+
+------------------------------------------------------------
+-- deBruijn terms, i.e., closed terms
+------------------------------------------------------------
+
+data STerm c a where
+    SWeaken :: SubC c1 c -> STerm c1 a -> STerm c a
+    SVar :: Member c (L a) -> STerm c a
+    SDVar :: Name (D a) -> STerm c a
+    SApp :: STerm c (a -> b) -> STerm c a -> STerm c b
+
+skelSubst :: STerm c a -> RAssign Name c -> DTerm a
+skelSubst (SWeaken f db) names = skelSubst db $ f names
+skelSubst (SVar inC) names = TVar $ C.get inC names
+skelSubst (SDVar dTVar) _ = TDVar dTVar
+skelSubst (SApp db1 db2) names = TApp (skelSubst db1 names) (skelSubst db2 names)
+
+-- applying a STerm to a context of names
+skelAppMultiNames ::
+  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 -> RAssign (Member fvs) args ->
+    STerm fvs a
+  skelAppMultiNamesH fvs MNil _ = fvs
+  -- flagged as non-exhaustive, in spite of type
+  skelAppMultiNamesH fvs (args :>: MbLName _) (inCs :>: inC) =
+    SApp (skelAppMultiNamesH fvs args inCs) (SVar inC)
+
+------------------------------------------------------------
+-- STerms combined with their free variables
+------------------------------------------------------------
+
+proxyCons :: Proxy r -> f a -> Proxy (r :> a)
+proxyCons _ _ = Proxy
+
+data FVSTerm c lc a where
+    FVSTerm :: FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a
+
+fvSSepLTVars ::
+  RAssign 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 'RAssign' vector.
+proxyOfRAssign :: RAssign f c -> Proxy c
+proxyOfRAssign _ = Proxy
+
+fvSSepLTVarsH ::
+  RAssign 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.get (C.weakenMemberL (proxyOfRAssign m) idx) xs)
+    Right n ->
+      SepRet (m :>: MbLName n)
+      (\xs -> case C.split c' lc xs of
+          (fvs' :>: fv', lcs) ->
+            f (C.append fvs' lcs) :>: fv')
+    where c' = proxyCons (proxyOfRAssign m) fv
+
+raiseAppName ::
+  Append c1 c2 (c1 :++: c2) -> Mb (c1 :++: c2) (Name a) -> Either (Member c2 a) (Mb c1 (Name a))
+raiseAppName app n =
+  case fmap mbNameBoundP (mbSeparate (C.proxiesFromAppend app) n) of
+    [nuP| Left mem |] -> Left $ mbLift mem
+    [nuP| Right n |] -> Right n
+
+------------------------------------------------------------
+-- lambda-lifting, woo hoo!
+------------------------------------------------------------
+
+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 (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
+  FVUnionRet names sub1 sub2 <- return $ fvUnion fvs1 fvs2
+  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.append c lc) body
+  FVSTerm fvs db <- return $ fvSSepLTVars lc llret
+  cont $ \k ->
+    Decls_Cons (freeParams (fvsToLC fvs) $ \names1 ->
+                boundParams lc $ \names2 ->
+                skelSubst db (C.append names1 names2))
+      $ nu $ \d -> k $ FVSTerm fvs (skelAppMultiNames (SDVar d) fvs)
+  where
+    fvsToLC :: FVList c lc -> LC lc
+    fvsToLC = C.mapRAssign 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 MNil (emptyMb t)) $ \(FVSTerm fvs db) ->
+  Decls_Base (skelSubst db (C.mapRAssign (\(MbLName mbn) -> elimEmptyMb mbn) fvs))
+
+mbLambdaLift :: Mb c (Term a) -> Mb c (Decls a)
+mbLambdaLift = fmap lambdaLift
diff --git a/src/Data/Binding/Hobbits/Examples/LambdaLifting/Examples.hs b/src/Data/Binding/Hobbits/Examples/LambdaLifting/Examples.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/Examples/LambdaLifting/Examples.hs
@@ -0,0 +1,52 @@
+-- |
+-- Module      : Data.Binding.Hobbits.SuperComb
+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+
+module Data.Binding.Hobbits.Examples.LambdaLifting.Examples where
+
+import Data.Binding.Hobbits.Examples.LambdaLifting.Terms
+import Data.Binding.Hobbits
+
+------------------------------------------------------------
+-- examples
+------------------------------------------------------------
+
+ex1 :: Term ((b1 -> b) -> b1 -> b)
+ex1 = lam (\f -> (lam $ \x -> App f x))
+
+ex2 :: Term ((((b2 -> b1) -> b2 -> b1) -> b) -> b)
+ex2 = lam (\f1 -> App f1 (lam (\f2 -> lam (\x -> App f2 x))))
+
+ex3 :: Term (b3 -> (((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b)
+ex3 = lam (\x -> lam (\f1 -> App f1 (lam (\f2 -> lam (\y -> f2 `App` x `App` y)))))
+
+ex4
+  :: Term
+       (((b1 -> b) -> b2 -> b)
+        -> (((b1 -> b) -> b2 -> b) -> b2 -> b1)
+        -> b2
+        -> b1)
+ex4 = lam $ \x -> lam $ \f1 ->
+      App f1 (lam $ \f2 -> lam $ \y -> f2 `App` (f1 `App` x `App` y))
+
+ex5 :: Term (((b2 -> b1) -> b) -> (b2 -> b1) -> b)
+ex5 = lam (\f1 -> lam $ \f2 -> App f1 (lam $ \x -> App f2 x))
+
+-- lambda-lift with a free variable (use mbLambdaLift)
+ex6 :: Binding (L ((b -> b) -> a)) (Term a)
+ex6 = nu (\f -> App (Var f) (lam $ \x -> x))
+
+-- lambda-lift with a free variable as part of a lambda's environment
+ex7 :: Binding (L ((b2 -> b2) -> b1)) (Term ((b1 -> b) -> b))
+ex7 = nu (\f -> lam $ \y -> App y $ App (Var f) (lam $ \x -> x))
+
+-- example from paper's Section 4
+exP :: Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b)
+exP = lam $ \f -> lam $ \g -> App f $ lam $ \x -> App g $ App g x
diff --git a/src/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs b/src/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs
@@ -0,0 +1,133 @@
+{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE TemplateHaskell, Rank2Types, QuasiQuotes, ViewPatterns #-}
+{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.SuperComb
+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+
+module Data.Binding.Hobbits.Examples.LambdaLifting.Terms
+  (L, D,
+   Term(..), lam,
+   DTerm(..), Decl(..), Decls(..)
+  ) where
+
+import Data.Binding.Hobbits
+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 RAssign (for pretty)
+newtype StringF x = StringF String
+unStringF (StringF str) = str
+
+
+------------------------------------------------------------
+-- source terms
+------------------------------------------------------------
+
+-- Term datatype; no Ds since there's no declarations yet
+data Term :: * -> * where
+  Var :: Name (L a) -> Term a
+  Lam :: Binding (L b) (Term a) -> Term (b -> a)
+  App :: Term (b -> a) -> Term b -> Term a
+
+$(mkNuMatching [t| forall a . Term a |])
+
+instance Show (Term a) where show = tpretty
+
+-- helps to build terms without explicitly using nu or Var
+lam :: (Term a -> Term b) -> Term (a -> b)
+lam f = Lam $ nu (f . Var)
+
+-- pretty print terms
+tpretty :: Term a -> String
+tpretty t = pretty' (emptyMb t) C.empty 0
+  where pretty' :: Mb c (Term a) -> RAssign StringF c -> Int -> String
+        pretty' [nuP| Var b |] varnames n =
+            case mbNameBoundP b of
+              Left pf  -> unStringF (C.get 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) ++ ")"
+        pretty' [nuP| App b1 b2 |] varnames n =
+            "(" ++ pretty' b1 varnames n ++ " " ++ pretty' b2 varnames n ++ ")"
+
+------------------------------------------------------------
+-- target terms
+------------------------------------------------------------
+
+-- terms under declarations
+data DTerm :: * -> * where
+  TVar :: Name (L a) -> DTerm a
+  TDVar :: Name (D a) -> DTerm a
+  TApp :: DTerm (a -> b) -> DTerm a -> DTerm b
+
+-- we use this type for a definiens instead of putting lambdas on the front
+data Decl :: * -> * where
+  Decl_One :: Binding (L a) (DTerm b) -> Decl (a -> b)
+  Decl_Cons :: Binding (L a) (Decl b) -> Decl (a -> b)
+
+-- top-level declarations with a return value
+data Decls :: * -> * where
+  Decls_Base :: DTerm a -> Decls a
+  Decls_Cons :: Decl b -> Binding (D b) (Decls a) -> Decls a
+
+$(mkNuMatching [t| forall a . DTerm a |])
+$(mkNuMatching [t| forall a . Decl a |])
+$(mkNuMatching [t| forall a . Decls a |])
+
+instance Show (DTerm a) where show = pretty
+instance Show (Decls a) where show = decls_pretty
+
+------------------------------------------------------------
+-- pretty printing
+------------------------------------------------------------
+
+-- pretty print terms
+pretty :: DTerm a -> String
+pretty t = mpretty (emptyMb t) C.empty
+
+mpretty :: Mb c (DTerm a) -> RAssign StringF c -> String
+mpretty [nuP| TVar b |] varnames =
+    mprettyName (mbNameBoundP b) varnames
+mpretty [nuP| TDVar b |] varnames =
+    mprettyName (mbNameBoundP b) varnames
+mpretty [nuP| TApp b1 b2 |] varnames =
+    "(" ++ mpretty b1 varnames
+        ++ " " ++ mpretty b2 varnames ++ ")"
+
+mprettyName (Left pf) varnames = unStringF (C.get pf varnames)
+mprettyName (Right n) varnames = "(free-var " ++ (show n) ++ ")"
+        
+
+-- pretty print decls
+decls_pretty :: Decls a -> String
+decls_pretty decls =
+    "let\n" ++ (mdecls_pretty (emptyMb decls) C.empty 0)
+
+mdecls_pretty :: Mb c (Decls a) -> RAssign 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)
+
+mdecl_pretty :: Mb c (Decl a) -> RAssign 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)
+mdecl_pretty [nuP| Decl_Cons d|] varnames n =
+  let vname = "x" ++ show n in
+  vname ++ " " ++ mdecl_pretty (mbCombine d) (varnames :>: StringF vname) (n+1)
diff --git a/src/Data/Binding/Hobbits/Internal/Closed.hs b/src/Data/Binding/Hobbits/Internal/Closed.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/Internal/Closed.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Closed
+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines the type @'Cl' a@ of closed objects of type
+-- @a@. Note that, in order to ensure adequacy of the Hobbits
+-- name-binding approach, this representation is hidden from the user,
+-- and so this file should never be imported directly by the user.
+--
+
+module Data.Binding.Hobbits.Internal.Closed where
+
+import Language.Haskell.TH (Q, Exp(..), Type(..))
+import qualified Language.Haskell.TH as TH
+import qualified Language.Haskell.TH.ExpandSyns as TH
+
+import qualified Data.Generics as SYB
+import qualified Language.Haskell.TH.Syntax as TH
+
+{-| The type @Closed a@ represents a closed term of type @a@, i.e., an expression
+of type @a@ with no free (Haskell) variables.  Since this cannot be checked
+directly in the Haskell type system, the @Closed@ data type is hidden, and the
+user can only create closed terms using Template Haskell, through the 'mkClosed'
+operator. -}
+newtype Closed a =
+  Closed {
+  -- | Extract the value of a 'Closed' object
+  unClosed :: a
+  }
+
+-- | Extract the type of an 'Info' object
+reifyNameType :: TH.Name -> Q Type
+reifyNameType n =
+  TH.reify n >>= \i ->
+  case i of
+    TH.VarI _ ty _ -> return ty
+    _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."
+
+-- | @mkClosed@ is used with Template Haskell quotations to create closed terms
+-- of type 'Closed'. A quoted expression is closed if all of the names occuring in
+-- it are either:
+--
+--   1) bound globally or
+--   2) bound within the quotation or
+--   3) also of type 'Closed'.
+mkClosed :: Q Exp -> Q Exp
+mkClosed e = AppE (ConE 'Closed) `fmap` e >>= SYB.everywhereM (SYB.mkM w) where
+  w e@(VarE n@(TH.Name _ flav)) = case flav of
+    TH.NameG {} -> return e -- bound globally
+    TH.NameU {} -> return e -- bound locally within this quotation
+    TH.NameL {} -> closed n >> return e -- bound locally outside this quotation
+    _ -> fail $ "`mkClosed' does not allow dynamically bound names: `"
+      ++ show n ++ "'."
+  w e = return e
+
+  closed n = do
+    ty <- reifyNameType n
+    TH.expandSyns ty >>= w ty
+      where
+        w _ (AppT (ConT m) _) | m == ''Closed = return ()
+        w top_ty (ForallT _ _ ty') = w top_ty ty'
+        w top_ty _ =
+          fail $ "`mkClosed` requires non-global variables to have type `Closed'.\n\t`"
+          ++ show (TH.ppr n) ++ "' does not. It's type is:\n\t `"
+          ++ show (TH.ppr top_ty) ++ "'."
diff --git a/src/Data/Binding/Hobbits/Internal/Mb.hs b/src/Data/Binding/Hobbits/Internal/Mb.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/Internal/Mb.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE GADTs, DeriveDataTypeable, ViewPatterns #-}
+{-# LANGUAGE RankNTypes, DataKinds, PolyKinds #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Internal.Name
+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@kestrel.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines the type @'Mb' ctx a@. In order to ensure
+-- adequacy of the Hobbits name-binding approach, this representation
+-- is hidden, and so this file should never be imported directly by
+-- the user.
+--
+
+module Data.Binding.Hobbits.Internal.Mb where
+
+import Data.Typeable
+import Data.Proxy
+import Data.Type.Equality
+import Data.Type.RList hiding (map)
+
+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 @'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
+  binding, or as "fresh pairs", which are pairs of a list of names
+  that are guaranteed to be fresh along with a body. Note that fresh
+  pairs must come with an 'MbTypeRepr' for the body type, to ensure
+  that the names given in the pair can be relaced by fresher names.
+-}
+data Mb (ctx :: RList k) b
+    = MkMbFun (RAssign Proxy ctx) (RAssign Name ctx -> b)
+    | MkMbPair (MbTypeRepr b) (RAssign Name ctx) b
+    deriving Typeable
+
+
+{-|
+   This type states that it is possible to replace free names with
+   fresh names in an object of type @a@. This type essentially just
+   captures a representation of the type a as either a Name type, a
+   multi-binding, a function type, or a (G)ADT. In order to be sure
+   that only the "right" proofs are used for (G)ADTs, however, this
+   type is hidden from the user, and can only be constructed with
+   'mkNuMatching'.
+-}
+
+data MbTypeRepr a where
+    MbTypeReprName :: MbTypeRepr (Name a)
+    MbTypeReprMb :: MbTypeRepr a -> MbTypeRepr (Mb ctx a)
+    MbTypeReprFun :: MbTypeRepr a -> MbTypeRepr b -> MbTypeRepr (a -> b)
+    MbTypeReprData :: MbTypeReprData a -> MbTypeRepr a
+
+data MbTypeReprData a =
+    MkMbTypeReprData (forall ctx. NameRefresher -> a -> a)
+
+{-|
+  The call @mapNamesPf data ns ns' a@ replaces each occurrence of a
+  free name in @a@ which is listed in @ns@ by the corresponding name
+  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 -> NameRefresher -> a -> a
+mapNamesPf MbTypeReprName refresher n = refreshName refresher n
+mapNamesPf (MbTypeReprMb tRepr) refresher (ensureFreshFun -> (proxies, f)) =
+    -- README: the fresh function created below is *guaranteed* to not
+    -- be passed elements of either names1 or names2, since it should
+    -- only ever be passed fresh names
+    MkMbFun proxies (\ns -> mapNamesPf tRepr refresher (f ns))
+mapNamesPf (MbTypeReprFun tReprIn tReprOut) refresher f =
+    (mapNamesPf tReprOut refresher) . f . (mapNamesPf tReprIn refresher)
+mapNamesPf (MbTypeReprData (MkMbTypeReprData mapFun)) refresher x =
+    mapFun refresher x
+
+
+-- | Ensures a multi-binding is in "fresh function" form
+ensureFreshFun :: Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
+ensureFreshFun (MkMbFun proxies f) = (proxies, f)
+ensureFreshFun (MkMbPair tRepr ns body) =
+    (mapRAssign (\_ -> Proxy) ns, \ns' ->
+      mapNamesPf tRepr (mkRefresher ns ns') body)
+
+-- | Ensures a multi-binding is in "fresh pair" form
+ensureFreshPair :: Mb ctx a -> (RAssign Name ctx, a)
+ensureFreshPair (MkMbPair _ ns body) = (ns, body)
+ensureFreshPair (MkMbFun proxies f) =
+    let ns = mapRAssign (MkName . fresh_name) proxies in
+    (ns, f ns)
diff --git a/src/Data/Binding/Hobbits/Internal/Name.hs b/src/Data/Binding/Hobbits/Internal/Name.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/Internal/Name.hs
@@ -0,0 +1,167 @@
+{-# LANGUAGE GADTs, DeriveDataTypeable, FlexibleInstances, TypeOperators #-}
+{-# LANGUAGE RankNTypes, DataKinds, PolyKinds #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Internal.Name
+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@kestrel.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines the type @'Name' a@ as a wrapper around a fresh
+-- integer. Note that, in order to ensure adequacy of the Hobbits
+-- name-binding approach, this representation is hidden from the user,
+-- and so this file should never be imported directly by the user.
+--
+
+module Data.Binding.Hobbits.Internal.Name where
+
+import Data.List
+import Data.Functor.Constant
+import Data.Typeable
+import Data.IntMap.Strict (IntMap)
+import qualified Data.IntMap.Strict as IntMap
+import Data.Type.Equality
+import Unsafe.Coerce (unsafeCoerce)
+import Data.IORef (IORef, newIORef, readIORef, writeIORef)
+import System.IO.Unsafe (unsafePerformIO)
+
+import Data.Type.RList
+
+
+-- | A @Name a@ is a bound name that is associated with type @a@.
+newtype Name (a :: k) = MkName Int deriving (Typeable, Eq, Ord)
+
+instance Show (Name a) where
+  showsPrec _ (MkName n) = showChar '#' . shows n . showChar '#'
+
+instance Show (RAssign Name c) where
+    show names = "[" ++ (concat $ intersperse "," $ mapToList show names) ++ "]"
+
+
+-------------------------------------------------------------------------------
+-- Externally visible operators
+-------------------------------------------------------------------------------
+
+{-|
+  @cmpName n m@ compares names @n@ and @m@ of types @Name a@ and @Name b@,
+  respectively. When they are equal, @Some e@ is returned for @e@ a proof
+  of type @a :~: b@ that their types are equal. Otherwise, @None@ is returned.
+
+  For example:
+
+> nu $ \n -> nu $ \m -> cmpName n n   ==   nu $ \n -> nu $ \m -> Some Refl
+> nu $ \n -> nu $ \m -> cmpName n m   ==   nu $ \n -> nu $ \m -> None
+-}
+cmpName :: Name a -> Name b -> Maybe (a :~: b)
+cmpName (MkName n1) (MkName n2)
+  | n1 == n2 = Just $ unsafeCoerce Refl
+  | otherwise = Nothing
+
+instance TestEquality Name where
+  testEquality = cmpName
+
+-- | Heterogeneous comparison of names, that could be at different kinds
+hcmpName :: forall (a :: k1) (b :: k2). Name a -> Name b -> Maybe (a :~~: b)
+hcmpName (MkName n1) (MkName n2)
+  | n1 == n2 = Just $ unsafeCoerce HRefl
+  | otherwise = Nothing
+
+-- | A name refresher gives new fresh indices to names
+newtype NameRefresher = NameRefresher { unNameRefresher :: IntMap Int }
+
+-- | Apply a 'NameRefresher' to a 'Name'
+refreshName :: NameRefresher -> Name a -> Name a
+refreshName (NameRefresher nmap) (MkName i) =
+  MkName $ IntMap.findWithDefault i i nmap
+
+-- | Build a 'NameRefresher' that maps one sequence of names to another
+mkRefresher :: forall (ctx :: RList k) .
+               RAssign Name ctx -> RAssign Name ctx -> NameRefresher
+mkRefresher ns1 ns2 =
+  NameRefresher $ IntMap.fromList $ toList $
+  map2 (\(MkName i) (MkName j) -> Constant (i,j)) ns1 ns2
+
+-- | Extend a 'NameRefresher' with one more name mapping
+extRefresher :: forall (a :: k). NameRefresher -> Name a -> Name a ->
+                NameRefresher
+extRefresher (NameRefresher nmap) (MkName n1) (MkName n2) =
+  NameRefresher $
+  IntMap.insertWith (\_ _ -> error "Hobbit name already in NameRefresher!")
+  n1 n2 nmap
+
+
+-------------------------------------------------------------------------------
+-- Hidden, unsafe operators
+-------------------------------------------------------------------------------
+
+
+-- building an arbitrary InCtx proof with a given length
+-- (this is used internally in HobbitLib)
+
+data ExMember where ExMember :: Member c a -> ExMember
+
+-- creating some Member proof of length i
+memberFromLen :: Int -> ExMember
+memberFromLen 0 = ExMember Member_Base
+memberFromLen n = case memberFromLen (n - 1) of
+  ExMember mem -> ExMember (Member_Step mem)
+
+-- unsafely creating a *specific* member proof from length i;
+-- this is for when we know the ith element of c must be type a
+unsafeLookupC :: Int -> Member c a
+unsafeLookupC n = case memberFromLen n of
+  ExMember mem -> unsafeCoerce mem
+
+
+-- building a proxy for each type in some unknown context
+data ExProxy where ExProxy :: RAssign Proxy ctx -> ExProxy
+proxyFromLen :: Int -> ExProxy
+proxyFromLen 0 = ExProxy MNil
+proxyFromLen n = case proxyFromLen (n - 1) of
+                   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
+-- unsafeProxyFromLen :: Int -> MapC Proxy ctx
+-- unsafeProxyFromLen n = case proxyFromLen n of
+--                          ExProxy proxy -> unsafeCoerce proxy
+
+-- -- unsafely convert a list of Ints, used to represent names, to
+-- -- names of certain, given types; note that the first name in the
+-- -- list becomes the last name in the output, with the same reversal
+-- -- used in the Mb representation (see, e.g., mbCombine)
+-- unsafeNamesFromInts :: [Int] -> MapC Name ctx
+-- unsafeNamesFromInts [] = unsafeCoerce Nil
+-- unsafeNamesFromInts (x:xs) =
+--     unsafeCoerce $ unsafeNamesFromInts xs :> MkName x
+
+-------------------------------------------------------------------------------
+-- encapsulated impurity
+-------------------------------------------------------------------------------
+
+-- README: we *cannot* inline counter, because we want all uses
+-- of counter to be the same IORef
+counter :: IORef Int
+{-# NOINLINE counter #-}
+counter = unsafePerformIO (newIORef 0)
+
+-- README: fresh_name takes a dummy argument that is used in a dummy
+-- way to avoid let-floating its body (and thus getting a fresh name
+-- exactly once)
+-- README: it *is* ok to inline fresh_name because we don't care in
+-- what order fresh names are created
+fresh_name :: a -> Int
+fresh_name a = unsafePerformIO $ do 
+    dummyRef <- newIORef a
+    x <- readIORef counter
+    writeIORef counter (x+1)
+    return x
+
+-- -- make one fresh name for each name in a given input list
+-- fresh_names :: MapC Name ctx -> MapC Name ctx
+-- fresh_names Nil = Nil
+-- fresh_names (names :> n) = fresh_names names :> MkName (fresh_name n)
diff --git a/src/Data/Binding/Hobbits/Internal/Utilities.hs b/src/Data/Binding/Hobbits/Internal/Utilities.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/Internal/Utilities.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE Rank2Types #-}
+
+module Data.Binding.Hobbits.Internal.Utilities where
+
+import qualified Data.Generics as SYB
+
+
+
+everywhereButM :: Monad m =>
+  SYB.GenericQ Bool -> SYB.GenericM m -> SYB.GenericM m
+everywhereButM q f x
+  | q x       = return x
+  | otherwise = (SYB.gmapM (everywhereButM q f) x) >>= f
diff --git a/src/Data/Binding/Hobbits/Liftable.hs b/src/Data/Binding/Hobbits/Liftable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/Liftable.hs
@@ -0,0 +1,154 @@
+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns, QuasiQuotes, DataKinds, PolyKinds #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Mb
+-- Copyright   : (c) 2014 Edwin Westbrook
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines the type-class Liftable for lifting
+-- non-binding-related data out of name-bindings. Note that this code
+-- is not "trusted", i.e., it is not part of the name-binding
+-- abstraction: instead, it is all written using the primitives
+-- exported by the Mb
+
+module Data.Binding.Hobbits.Liftable where
+
+import Data.Type.RList
+import Data.Binding.Hobbits.Mb
+import Data.Binding.Hobbits.Internal.Mb
+import Data.Binding.Hobbits.QQ
+import Data.Binding.Hobbits.Closed
+import Data.Binding.Hobbits.NuMatching
+import Data.Binding.Hobbits.NuMatchingInstances
+
+import Data.Ratio
+import Data.Proxy
+import Numeric.Natural
+import Data.Type.Equality
+
+
+{-|
+  The class @Liftable a@ gives a \"lifting function\" for a, which can
+  take any data of type @a@ out of a multi-binding of type @'Mb' ctx a@.
+-}
+class NuMatching a => Liftable a where
+    mbLift :: Mb ctx a -> a
+
+-------------------------------------------------------------------------------
+-- * Lifting instances that must be defined inside the library abstraction boundary
+-------------------------------------------------------------------------------
+
+instance Liftable Char where
+    mbLift (ensureFreshPair -> (_, c)) = c
+
+instance Liftable Int where
+    mbLift (ensureFreshPair -> (_, i)) = i
+
+instance Liftable Integer where
+    mbLift (ensureFreshPair -> (_, i)) = i
+
+instance Liftable (Closed a) where
+    mbLift (ensureFreshPair -> (_, c)) = c
+
+instance Liftable Natural where
+    mbLift (ensureFreshPair -> (_, i)) = i
+
+
+-------------------------------------------------------------------------------
+-- * Lifting instances and related functions that could be defined outside the library
+-------------------------------------------------------------------------------
+
+-- README: this requires overlapping instances, because it clashes
+-- with Liftable2, but this instance is better because it does not
+-- require c nor a to be liftable
+instance Liftable (Member c a) where
+    mbLift [nuP| Member_Base |] = Member_Base
+    mbLift [nuP| Member_Step m |] = Member_Step (mbLift m)
+
+-- | Lift a list (but not its elements) out of a multi-binding
+mbList :: NuMatching a => Mb c [a] -> [Mb c a]
+mbList [nuP| [] |] = []
+mbList [nuP| x : xs |] = x : mbList xs
+
+instance (Integral a, NuMatching a) => NuMatching (Ratio a) where
+  nuMatchingProof =
+    isoMbTypeRepr (\r -> (numerator r, denominator r)) (\(n,d) -> n%d)
+instance (Integral a, Liftable a) => Liftable (Ratio a) where
+  mbLift mb_r =
+    (\(n,d) -> n%d) $ mbLift $ fmap (\r -> (numerator r, denominator r)) mb_r
+
+instance Liftable a => Liftable [a] where
+    mbLift [nuP| [] |] = []
+    mbLift [nuP| x : xs |] = (mbLift x) : (mbLift xs)
+
+instance Liftable () where
+    mbLift [nuP| () |] = ()
+
+instance (Liftable a, Liftable b) => Liftable (a,b) where
+    mbLift [nuP| (x,y) |] = (mbLift x, mbLift y)
+
+instance Liftable Bool where
+  mbLift [nuP| True |] = True
+  mbLift [nuP| False |] = False
+
+instance Liftable a => Liftable (Maybe a) where
+  mbLift [nuP| Nothing |] = Nothing
+  mbLift [nuP| Just mb_a |] = Just $ mbLift mb_a
+
+instance (Liftable a, Liftable b) => Liftable (Either a b) where
+  mbLift [nuP| Left mb_a |] = Left $ mbLift mb_a
+  mbLift [nuP| Right mb_b |] = Right $ mbLift mb_b
+
+instance Liftable (a :~: b) where
+  mbLift [nuP| Refl |] = Refl
+
+instance Liftable (Proxy (a :: k)) where
+  mbLift [nuP| Proxy |] = Proxy
+
+-- Ideally this would be in the Mb module, but that ends up producing a circular
+-- include due to needing `mbLift`
+instance Eq a => Eq (Mb ctx a) where
+  mb1 == mb2 =
+    mbLift $ nuMultiWithElim (\_ (_ :>: a1 :>: a2) ->
+                               a1 == a2) (MNil :>: mb1 :>: mb2)
+
+
+
+-- README: these lead to overlapping instances...
+
+{-
+
+{-|
+  The class @Liftable1 f@ gives a lifting function for each type @f a@
+  when @a@ itself is @Liftable@.
+-}
+class Liftable1 f where
+    mbLift1 :: Liftable a => Mb ctx (f a) -> f a
+
+instance (Liftable1 f, Liftable a) => Liftable (f a) where
+    mbLift = mbLift1
+
+instance Liftable1 [] where
+    mbLift1 [nuP| [] |] = []
+    mbLift1 [nuP| x : xs |] = (mbLift x) : (mbLift1 xs)
+
+{-|
+  The class @Liftable2 f@ gives a lifting function for each type @f a b@
+  when @a@ and @b@ are @Liftable@.
+-}
+class Liftable2 f where
+    mbLift2 :: (Liftable a, Liftable b) => Mb ctx (f a b) -> f a b
+
+instance Liftable2 (,) where
+    mbLift2 [nuP| (x,y) |] = (mbLift x, mbLift y)
+
+instance (Liftable2 f, Liftable a) => Liftable1 (f a) where
+    mbLift1 = mbLift2
+
+-}
diff --git a/src/Data/Binding/Hobbits/Mb.hs b/src/Data/Binding/Hobbits/Mb.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/Mb.hs
@@ -0,0 +1,324 @@
+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, ViewPatterns, DataKinds #-}
+{-# LANGUAGE RankNTypes, PolyKinds #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Mb
+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines multi-bindings as the type 'Mb', as well as a number of
+-- operations on multi-bindings. See the paper E. Westbrook, N. Frisby,
+-- P. Brauner, \"Hobbits for Haskell: A Library for Higher-Order Encodings in
+-- Functional Programming Languages\" for more information.
+
+module Data.Binding.Hobbits.Mb (
+  -- * Abstract types
+  Name(),      -- hides Name implementation
+  Binding(),   -- hides Binding implementation
+  Mb(),        -- hides MultiBind implementation
+  -- * Multi-binding constructors
+  nu, nuMulti, nus, emptyMb, extMb, extMbMulti,
+  -- * Queries on names
+  cmpName, hcmpName, mbNameBoundP, mbCmpName,
+  -- * Operations on multi-bindings
+  elimEmptyMb, mbCombine, mbSeparate, mbToProxy, mbSwap, mbPure, mbApply,
+  mbMap2,
+  -- * Eliminators for multi-bindings
+  nuMultiWithElim, nuWithElim, nuMultiWithElim1, nuWithElim1
+) where
+
+import Control.Applicative
+import Control.Monad.Identity
+
+import Data.Type.Equality ((:~:)(..))
+import Data.Proxy (Proxy(..))
+
+import Unsafe.Coerce (unsafeCoerce)
+
+import Data.Type.RList
+
+import Data.Binding.Hobbits.Internal.Name
+import Data.Binding.Hobbits.Internal.Mb
+--import qualified Data.Binding.Hobbits.Internal as I
+
+-------------------------------------------------------------------------------
+-- creating bindings
+-------------------------------------------------------------------------------
+
+-- | A @Binding@ is simply a multi-binding that binds one name
+type Binding (a :: k) = Mb (RNil :> a)
+
+-- note: we reverse l to show the inner-most bindings last
+instance Show a => Show (Mb c a) where
+  showsPrec p (ensureFreshPair -> (names, b)) = showParen (p > 10) $
+    showChar '#' . shows names . showChar '.' . shows b
+
+{-|
+  @nu f@ creates a binding which binds a fresh name @n@ and whose
+  body is the result of @f n@.
+-}
+nu :: forall (a :: k1) (b :: *) . (Name a -> b) -> Binding a b
+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 @'RAssign' 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 :: RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b
+nuMulti proxies f = MkMbFun (mapRAssign (const Proxy) proxies) f
+
+-- | @nus = nuMulti@
+nus x = nuMulti x
+
+-- | Extend the context of a name-binding by adding a single type
+extMb :: Mb ctx a -> Mb (ctx :> tp) a
+extMb = mbCombine . fmap (nu . const)
+
+-- | Extend the context of a name-binding with multiple types
+extMbMulti :: RAssign f ctx2 -> Mb ctx1 a -> Mb (ctx1 :++: ctx2) a
+extMbMulti ns mb = mbCombine $ fmap (nuMulti ns . const) mb
+
+
+-------------------------------------------------------------------------------
+-- Queries on Names
+-------------------------------------------------------------------------------
+
+{-|
+  Checks if a name is bound in a multi-binding, returning @Left mem@
+  when the name is bound, where @mem@ is a proof that the type of the
+  name is in the type list for the multi-binding, and returning
+  @Right n@ when the name is not bound, where @n@ is the name.
+
+  For example:
+
+> nu $ \n -> mbNameBoundP (nu $ \m -> m)  ==  nu $ \n -> Left Member_Base
+> nu $ \n -> mbNameBoundP (nu $ \m -> n)  ==  nu $ \n -> Right n
+-}
+mbNameBoundP :: forall (a :: k1) (ctx :: RList k2).
+                Mb ctx (Name a) -> Either (Member ctx a) (Name a)
+mbNameBoundP (ensureFreshPair -> (names, n)) = helper names n where
+    helper :: RAssign 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
+  Nothing -> Right (MkName n)
+  Just i -> Left (I.unsafeLookupC i)
+-}
+
+
+{-|
+  Compares two names inside bindings, taking alpha-equivalence into
+  account; i.e., if both are the @i@th name, or both are the same name
+  not bound in their respective multi-bindings, then they compare as
+  equal. The return values are the same as for 'cmpName', so that
+  @Some Refl@ is returned when the names are equal and @Nothing@ is
+  returned when they are not.
+-}
+mbCmpName :: forall (a :: k1) (b :: k1) (c :: RList k2).
+             Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b)
+mbCmpName (ensureFreshPair -> (names, n1)) (ensureFreshFun -> (_, f2)) =
+  cmpName n1 (f2 names)
+
+
+-------------------------------------------------------------------------------
+-- Operations on multi-bindings
+-------------------------------------------------------------------------------
+
+-- | Creates an empty binding that binds 0 names.
+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 RNil a -> a
+elimEmptyMb (ensureFreshPair -> (_, body)) = body
+
+
+-- Extract the proxy objects from an Mb inside of a fresh function
+freshFunctionProxies :: RAssign Proxy ctx1 -> (RAssign Name ctx1 -> Mb ctx2 a) ->
+                        RAssign Proxy ctx2
+freshFunctionProxies proxies1 f =
+    case f (mapRAssign (const $ MkName 0) proxies1) of
+      MkMbFun proxies2 _ -> proxies2
+      MkMbPair _ ns _ -> mapRAssign (const Proxy) ns
+
+
+-- README: inner-most bindings come FIRST
+-- | Combines a binding inside another binding into a single binding.
+mbCombine :: forall (c1 :: RList k) (c2 :: RList k) a b.
+             Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
+mbCombine (MkMbPair tRepr1 l1 (MkMbPair tRepr2 l2 b)) =
+  MkMbPair tRepr2 (append 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"
+    -- because these proxies should never depend on the names
+    -- themselves
+    let proxies2 = freshFunctionProxies proxies1 f1 in
+    MkMbFun
+    (append proxies1 proxies2)
+    (\ns ->
+         let (ns1, ns2) = split Proxy proxies2 ns in
+         let (_, f2) = ensureFreshFun (f1 ns1) in
+         f2 ns2)
+
+
+{-|
+  Separates a binding into two nested bindings. The first argument, of
+  type @'RAssign' any c2@, is a \"phantom\" argument to indicate how
+  the context @c@ should be split.
+-}
+mbSeparate :: forall (ctx1 :: RList k) (ctx2 :: RList k) (any :: k -> *) a.
+              RAssign 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) = split Proxy c2 ns
+mbSeparate c2 (MkMbFun proxies f) =
+    MkMbFun proxies1 (\ns1 -> MkMbFun proxies2 (\ns2 -> f (append ns1 ns2)))
+        where
+          (proxies1, proxies2) = split Proxy c2 proxies
+
+
+-- | Returns a proxy object that enumerates all the types in ctx.
+mbToProxy :: forall (ctx :: RList k) (a :: *) .
+             Mb ctx a -> RAssign Proxy ctx
+mbToProxy (MkMbFun proxies _) = proxies
+mbToProxy (MkMbPair _ ns _) = mapRAssign (\_ -> Proxy) ns
+
+
+{-|
+  Take a multi-binding inside another multi-binding and move the
+  outer binding inside the ineer one.
+-}
+mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
+mbSwap (ensureFreshFun -> (proxies1, f1)) =
+    let proxies2 = freshFunctionProxies proxies1 f1 in
+    MkMbFun proxies2
+      (\ns2 ->
+         MkMbFun proxies1
+         (\ns1 ->
+            snd (ensureFreshFun (f1 ns1)) ns2))
+
+-- | Put a value inside a multi-binding
+mbPure :: RAssign f ctx -> a -> Mb ctx a
+mbPure prxs = nuMulti prxs . const
+
+{-|
+  Applies a function in a multi-binding to an argument in a
+  multi-binding that binds the same number and types of names.
+-}
+mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
+mbApply (ensureFreshFun -> (proxies, f_fun)) (ensureFreshFun -> (_, f_arg)) =
+  MkMbFun proxies (\ns -> f_fun ns $ f_arg ns)
+
+
+-- | Lift a binary function function to `Mb`s
+mbMap2 :: (a -> b -> c) -> Mb ctx a -> Mb ctx b -> Mb ctx c
+mbMap2 f mb1 mb2 = fmap f mb1 `mbApply` mb2
+
+-------------------------------------------------------------------------------
+-- Functor and Applicative instances
+-------------------------------------------------------------------------------
+
+instance Functor (Mb ctx) where
+    fmap f mbArg =
+        mbApply (nuMulti (mbToProxy mbArg) (\_ -> f)) mbArg
+
+instance TypeCtx ctx => Applicative (Mb ctx) where
+    pure x = nuMulti typeCtxProxies (const x)
+    (<*>) = mbApply
+
+
+-------------------------------------------------------------------------------
+-- Eliminators for multi-bindings
+-------------------------------------------------------------------------------
+
+-- FIXME: add more examples!!
+{-|
+
+  asdfasdf
+
+  The expression @nuWithElimMulti args f@ takes a sequence @args@ of one or more
+  multi-bindings (it is a runtime error to pass an empty sequence of arguments),
+  each of type @Mb ctx ai@ for the same type context @ctx@ of bound names, and a
+  function @f@ and does the following:
+
+  * Creates a multi-binding that binds names @n1,...,nn@, one name for
+    each type in @ctx@;
+
+  * Substitutes the names @n1,...,nn@ for the names bound by each
+    argument in the @args@ sequence, yielding the bodies of the @args@
+    (using the new name @n@); and then
+
+  * Passes the sequence @n1,...,nn@ along with the result of
+    substituting into @args@ to the function @f@, which then returns
+    the value for the newly created binding.
+
+  For example, here is an alternate way to implement 'mbApply':
+
+> mbApply' :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
+> mbApply' f a =
+>     nuWithElimMulti ('MNil' :>: f :>: a)
+>                     (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')
+-}
+nuMultiWithElim :: (RAssign Name ctx -> RAssign Identity args -> b) ->
+                   RAssign (Mb ctx) args -> Mb ctx b
+nuMultiWithElim f args =
+  let proxies =
+        case args of
+          MNil -> error "nuMultiWithElim"
+          (_ :>: arg1) -> mbToProxy arg1 in
+  MkMbFun proxies
+          (\ns ->
+            f ns $ mapRAssign (\arg ->
+                                Identity $ snd (ensureFreshFun arg) ns) args)
+
+
+{-|
+  Similar to 'nuMultiWithElim' but binds only one name. Note that the argument
+  list here is allowed to be empty.
+-}
+nuWithElim :: (Name a -> RAssign Identity args -> b) ->
+              RAssign (Mb (RNil :> a)) args ->
+              Binding a b
+nuWithElim f MNil = nu $ \n -> f n MNil
+nuWithElim f args =
+    nuMultiWithElim (\(MNil :>: n) -> f n) args
+
+
+{-|
+  Similar to 'nuMultiWithElim' but takes only one argument
+-}
+nuMultiWithElim1 :: (RAssign Name ctx -> arg -> b) -> Mb ctx arg -> Mb ctx b
+nuMultiWithElim1 f arg =
+    nuMultiWithElim (\names (MNil :>: Identity arg) -> f names arg)
+    (MNil :>: arg)
+
+
+{-|
+  Similar to 'nuMultiWithElim' but takes only one argument that binds
+  a single name.
+-}
+nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b
+nuWithElim1 f arg =
+  nuWithElim (\n (MNil :>: Identity arg) -> f n arg) (MNil :>: arg)
diff --git a/src/Data/Binding/Hobbits/MonadBind.hs b/src/Data/Binding/Hobbits/MonadBind.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/MonadBind.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.MonadBind
+-- Copyright   : (c) 2020 Edwin Westbrook
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@galois.com
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines monads that are compatible with the notion of
+-- name-binding, where a monad is compatible with name-binding iff it can
+-- intuitively run computations that are inside name-bindings. More formally, a
+-- /binding monad/ is a monad with an operation 'mbM' that commutes name-binding
+-- with the monadic operations, meaning:
+--
+-- > 'mbM' ('nuMulti' $ \ns -> 'return' a) == 'return' ('nuMulti' $ \ns -> a)
+-- > 'mbM' ('nuMulti' $ \ns -> m >>= f)
+-- >   == 'mbM' ('nuMulti' $ \ns -> m) >>= \mb_x ->
+-- >      'mbM' (('nuMulti' $ \ns x -> f x) `'mbApply'` mb_x)
+
+module Data.Binding.Hobbits.MonadBind (MonadBind(..), MonadStrongBind(..)) where
+
+import Data.Binding.Hobbits.Closed
+import Data.Binding.Hobbits.Liftable (mbLift)
+import Data.Binding.Hobbits.Mb
+import Data.Binding.Hobbits.NuMatching
+import Data.Binding.Hobbits.QQ
+
+import Control.Monad.Identity (Identity(..))
+import Control.Monad.Reader (ReaderT(..))
+import Control.Monad.State (StateT(..), get, lift, put, runStateT)
+
+-- | The class of name-binding monads
+class Monad m => MonadBind m where
+  mbM :: NuMatching a => Mb ctx (m a) -> m (Mb ctx a)
+
+-- | Bind a name inside a computation and return the name-binding whose body was
+-- returned by the computation
+nuM :: (MonadBind m, NuMatching b) => (Name a -> m b) -> m (Binding a b)
+nuM = mbM . nu
+
+instance MonadBind Identity where
+  mbM = Identity . fmap runIdentity
+
+instance MonadBind Maybe where
+  mbM [nuP| Just x |] = return x
+  mbM [nuP| Nothing |] = Nothing
+
+instance MonadBind m => MonadBind (ReaderT r m) where
+  mbM mb = ReaderT $ \r -> mbM $ fmap (flip runReaderT r) mb
+
+-- | A version of 'MonadBind' that does not require a 'NuMatching' instance on
+-- the element type of the multi-binding in the monad
+class MonadBind m => MonadStrongBind m where
+  strongMbM :: Mb ctx (m a) -> m (Mb ctx a)
+
+instance MonadStrongBind Identity where
+  strongMbM = Identity . fmap runIdentity
+
+instance MonadStrongBind m => MonadStrongBind (ReaderT r m) where
+  strongMbM mb = ReaderT $ \r -> strongMbM $ fmap (flip runReaderT r) mb
+
+-- | State types that can incorporate name-bindings
+class NuMatching s => BindState s where
+  bindState :: Mb ctx s -> s
+
+instance BindState (Closed s) where
+  bindState = mbLift
+
+instance (MonadBind m, BindState s) => MonadBind (StateT s m) where
+  mbM mb_m = StateT $ \s ->
+    mbM (fmap (\m -> runStateT m s) mb_m) >>= \mb_as ->
+    return (fmap fst mb_as, bindState (fmap snd mb_as))
+
+instance (MonadStrongBind m, BindState s) => MonadStrongBind (StateT s m) where
+  strongMbM mb_m = StateT $ \s ->
+    strongMbM (fmap (\m -> runStateT m s) mb_m) >>= \mb_as ->
+    return (fmap fst mb_as, bindState (fmap snd mb_as))
+
+
+-- | A monad whose effects are closed
+class Monad m => MonadClosed m where
+  closedM :: Closed (m a) -> m (Closed a)
+
+instance MonadClosed Identity where
+  closedM = Identity . clApply $(mkClosed [| runIdentity |])
+
+instance (MonadClosed m, Closable s) => MonadClosed (StateT s m) where
+  closedM clm =
+    do s <- get
+       cl_a_s <- lift $ closedM ($(mkClosed [| runStateT |]) `clApply` clm
+                                 `clApply` toClosed s)
+       put (snd $ unClosed cl_a_s)
+       return ($(mkClosed [| fst |]) `clApply` cl_a_s)
diff --git a/src/Data/Binding/Hobbits/NameMap.hs b/src/Data/Binding/Hobbits/NameMap.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/NameMap.hs
@@ -0,0 +1,197 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Mb
+-- Copyright   : (c) 2019 Edwin Westbrook
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@galois.com
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- Implements mappings from 'Name's to some associated data, using
+-- 'Data.IntMap.Strict'. Note that these mappings are strict.
+--
+-- All of the functions in this module operate in an identical manner as those
+-- of the same name in the 'Data.IntMap.Strict' module.
+
+module Data.Binding.Hobbits.NameMap (
+  NameMap(), NameAndElem(..)
+  , empty, singleton, fromList
+  , insert, delete, adjust, update, alter
+  , lookup, (!), member, null, size
+  , union, difference, (\\), intersection
+  , map, foldr, foldl
+  , assocs
+  , liftNameMap
+  ) where
+
+import Prelude hiding (lookup, null, map, foldr, foldl)
+import qualified Prelude as Prelude (map)
+import Data.IntMap.Strict (IntMap)
+import qualified Data.IntMap.Strict as IntMap
+import Unsafe.Coerce
+
+import Data.Binding.Hobbits.Internal.Name
+import Data.Binding.Hobbits.Mb
+import Data.Binding.Hobbits.NuMatching
+import Data.Binding.Hobbits.NuMatchingInstances
+import Data.Binding.Hobbits.QQ
+
+-- | An element of a 'NameMap', where the name type @a@ is existentially
+-- quantified
+data NMElem (f :: k -> *) where
+  NMElem :: f a -> NMElem f
+
+-- | Coerce an @'NMElem' f@ to an @f a@ for a specific type @a@. This assumes we
+-- know that this is the proper type to coerce it to, i.e., it is unsafe.
+coerceNMElem :: NMElem f -> f a
+coerceNMElem (NMElem x) = unsafeCoerce x
+
+-- | A heterogeneous map from 'Name's of arbitrary type @a@ to elements of @f a@
+newtype NameMap (f :: k -> *) =
+  NameMap { unNameMap :: IntMap (NMElem f) }
+
+-- | Internal-only helper function for mapping a unary function on 'IntMap's to
+-- a 'NameMap'
+mapNMap1 :: (IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
+mapNMap1 f (NameMap m) = NameMap $ f m
+
+-- | Internal-only helper function for mapping a binary function on 'IntMap's to
+-- 'NameMap's
+mapNMap2 :: (IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f)) ->
+            NameMap f -> NameMap f -> NameMap f
+mapNMap2 f (NameMap m1) (NameMap m2) = NameMap $ f m1 m2
+
+-- | The empty 'NameMap'
+empty :: NameMap f
+empty = NameMap IntMap.empty
+
+-- | The singleton 'NameMap' with precisely one 'Name' and corresponding value
+singleton :: Name a -> f a -> NameMap f
+singleton (MkName i) x = NameMap $ IntMap.singleton i $ NMElem x
+
+-- | A pair of a 'Name' of some type @a@ along with an element of type @f a@
+data NameAndElem f where
+  NameAndElem :: Name a -> f a -> NameAndElem f
+
+-- | Build a 'NameMap' from a list of pairs of names and values they map to
+fromList :: [NameAndElem f] -> NameMap f
+fromList =
+  NameMap . IntMap.fromList .
+  Prelude.map (\ne ->
+                case ne of
+                  NameAndElem (MkName i) f -> (i, NMElem f))
+
+-- | Insert a 'Name' and a value it maps to into a 'NameMap'
+insert :: Name a -> f a -> NameMap f -> NameMap f
+insert (MkName i) f = mapNMap1 $ IntMap.insert i (NMElem f)
+
+-- | Delete a 'Name' and the value it maps to from a 'NameMap'
+delete :: Name a -> NameMap f -> NameMap f
+delete (MkName i) = mapNMap1 $ IntMap.delete i
+
+-- | Apply a function to the value mapped to by a 'Name'
+adjust :: (f a -> f a) -> Name a -> NameMap f -> NameMap f
+adjust f (MkName i) = mapNMap1 $ IntMap.adjust (NMElem . f . coerceNMElem) i
+
+-- | Update the value mapped to by a 'Name', possibly deleting it
+update :: (f a -> Maybe (f a)) -> Name a -> NameMap f -> NameMap f
+update f (MkName i) = mapNMap1 $ IntMap.update (fmap NMElem . f . coerceNMElem) i
+
+-- | Apply a function to the optional value associated with a 'Name', where
+-- 'Nothing' represents the 'Name' not being present in the 'NameMap'
+alter :: (Maybe (f a) -> Maybe (f a)) -> Name a -> NameMap f -> NameMap f
+alter f (MkName i) =
+  mapNMap1 $ IntMap.alter (fmap NMElem . f . fmap coerceNMElem) i
+
+-- | Look up the value associated with a 'Name', returning 'Nothing' if there is
+-- none
+lookup :: Name a -> NameMap f -> Maybe (f a)
+lookup (MkName i) (NameMap m) = fmap coerceNMElem $ IntMap.lookup i m
+
+-- | Synonym for 'lookup' with the argument order reversed
+(!) :: NameMap f -> Name a -> f a
+(NameMap m) ! (MkName i) = coerceNMElem $ m IntMap.! i
+
+-- | Test if a 'Name' has a value in a 'NameMap'
+member :: Name a -> NameMap f -> Bool
+member (MkName i) (NameMap m) = IntMap.member i m
+
+-- | Test if a 'NameMap' is empty
+null :: NameMap f -> Bool
+null (NameMap m) = IntMap.null m
+
+-- | Return the number of 'Name's in a 'NameMap'
+size :: NameMap f -> Int
+size (NameMap m) = IntMap.size m
+
+-- | Union two 'NameMap's
+union :: NameMap f -> NameMap f -> NameMap f
+union = mapNMap2 IntMap.union
+
+-- | Remove all bindings in the first 'NameMap' for 'Name's in the second
+difference :: NameMap f -> NameMap f -> NameMap f
+difference = mapNMap2 IntMap.difference
+
+-- | Infix synonym for 'difference'
+(\\) :: NameMap f -> NameMap f -> NameMap f
+(\\) = difference
+
+-- | Intersect two 'NameMap's
+intersection :: NameMap f -> NameMap f -> NameMap f
+intersection = mapNMap2 IntMap.intersection
+
+-- | Map a function across the values associated with each 'Name'
+map :: (forall a. f a -> g a) -> NameMap f -> NameMap g
+map f (NameMap m) =
+  NameMap $ IntMap.map (\e -> case e of
+                           NMElem x -> NMElem $ f x) m
+
+-- | Perform a right fold across all values in a 'NameMap'
+foldr :: (forall a. f a -> b -> b) -> b -> NameMap f -> b
+foldr f b (NameMap m) =
+  IntMap.foldr (\e -> case e of
+                   NMElem x -> f x) b m
+
+-- | Perform a left fold across all values in a 'NameMap'
+foldl :: (forall b. a -> f b -> a) -> a -> NameMap f -> a
+foldl f a (NameMap m) =
+  IntMap.foldl (\a e -> case e of
+                   NMElem x -> f a x) a m
+
+-- | Return all 'Name's in a 'NameMap' with their associated values
+assocs :: NameMap f -> [NameAndElem f]
+assocs (NameMap m) =
+  Prelude.map (\(i, e) -> case e of
+                  NMElem f -> NameAndElem (MkName i) f) $
+  IntMap.assocs m
+
+$(mkNuMatching [t| forall f. NuMatchingAny1 f => NameAndElem f |])
+
+-- | Lift a 'NameMap' out of a name-binding using a "partial lifting function"
+-- that can lift some values in the 'NameMap' out of the binding. The resulting
+-- 'NameMap' contains those names and associated values where the names were not
+-- bound by the name-binding and the partial lifting function was able to lift
+-- their associated values.
+liftNameMap :: forall ctx f a. NuMatchingAny1 f =>
+               (forall a. Mb ctx (f a) -> Maybe (f a)) ->
+               Mb ctx (NameMap f) -> NameMap f
+liftNameMap lifter = helper . fmap assocs where
+  helper :: Mb ctx [NameAndElem f] -> NameMap f
+  helper [nuP| [] |] = empty
+  helper [nuP| (NameAndElem mb_n mb_f):mb_elems |]
+    | Right n <- mbNameBoundP mb_n
+    , Just f <- lifter mb_f
+    = insert n f (helper mb_elems)
+  helper [nuP| _:mb_elems |] = helper mb_elems
diff --git a/src/Data/Binding/Hobbits/NameSet.hs b/src/Data/Binding/Hobbits/NameSet.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/NameSet.hs
@@ -0,0 +1,135 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE PatternGuards #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.NameSet
+-- Copyright   : (c) 2020 Edwin Westbrook
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@galois.com
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- Implements sets of 'Name's using 'Data.IntSet.Strict'. Note that these
+-- mappings are strict.
+
+module Data.Binding.Hobbits.NameSet (
+  NameSet(), SomeName(..)
+  , empty, singleton, fromList, toList
+  , insert, delete, member, null, size
+  , union, unions, difference, (\\), intersection
+  , map, foldr, foldl
+  , liftNameSet
+  ) where
+
+import Prelude hiding (lookup, null, map, foldr, foldl)
+import qualified Prelude as Prelude (map)
+import Data.Maybe
+import Data.IntSet (IntSet)
+import qualified Data.IntSet as IntSet
+import Data.Kind
+import qualified Data.Foldable as Foldable
+
+import Data.Binding.Hobbits.Internal.Name
+import Data.Binding.Hobbits.Mb
+import Data.Binding.Hobbits.NuMatching
+import Data.Binding.Hobbits.QQ
+import Data.Binding.Hobbits.Liftable
+
+-- | A set of 'Name's whose types all have kind @k@
+newtype NameSet k = NameSet { unNameSet :: IntSet }
+
+-- | A 'Name' of some unknown type of kind @k@
+data SomeName k = forall (a :: k). SomeName (Name a)
+
+$(mkNuMatching [t| forall k. SomeName k |])
+
+-- | The empty 'NameSet'
+empty :: NameSet k
+empty = NameSet $ IntSet.empty
+
+-- | The singleton 'NameSet'
+singleton :: Name (a::k) -> NameSet k
+singleton (MkName i) = NameSet $ IntSet.singleton $ i
+
+-- | Convert a list of names to a 'NameSet'
+fromList :: [SomeName k] -> NameSet k
+fromList =
+  NameSet . IntSet.fromList . Prelude.map (\(SomeName (MkName i)) -> i)
+
+-- | Convert a 'NameSet' to a list
+toList :: NameSet k -> [SomeName k]
+toList (NameSet s) = Prelude.map (SomeName . MkName) (IntSet.toList s)
+
+-- | Insert a name into a 'NameSet'
+insert :: Name (a::k) -> NameSet k -> NameSet k
+insert (MkName i) (NameSet s) = NameSet $ IntSet.insert i s
+
+-- | Delete a name from a 'NameSet'
+delete :: Name (a::k) -> NameSet k -> NameSet k
+delete (MkName i) (NameSet s) = NameSet $ IntSet.delete i s
+
+-- | Test if a name is in a 'NameSet'
+member :: Name (a::k) -> NameSet k -> Bool
+member (MkName i) (NameSet s) = IntSet.member i s
+
+-- | Test if a 'NameSet' is empty
+null :: NameSet k -> Bool
+null (NameSet s) = IntSet.null s
+
+-- | Compute the cardinality of a 'NameSet'
+size :: NameSet k -> Int
+size (NameSet s) = IntSet.size s
+
+-- | Take the union of two 'NameSet's
+union :: NameSet k -> NameSet k -> NameSet k
+union (NameSet s1) (NameSet s2) = NameSet $ IntSet.union s1 s2
+
+-- | Take the union of a list of 'NameSet's
+unions :: Foldable f => f (NameSet k) -> NameSet k
+unions = Foldable.foldl' union empty
+
+-- | Take the set of all elements of the first 'NameSet' not in the second
+difference :: NameSet k -> NameSet k -> NameSet k
+difference (NameSet s1) (NameSet s2) = NameSet $ IntSet.difference s1 s2
+
+-- | Another name for 'difference'
+(\\) :: NameSet k -> NameSet k -> NameSet k
+(\\) = difference
+
+-- | Take the intersection of two 'NameSet's
+intersection :: NameSet k -> NameSet k -> NameSet k
+intersection (NameSet s1) (NameSet s2) = NameSet $ IntSet.intersection s1 s2
+
+-- | Map a function across all elements of a 'NameSet'
+map :: (forall (a::k). Name a -> Name a) -> NameSet k -> NameSet k
+map f (NameSet s) =
+  NameSet $ IntSet.map (\i -> let (MkName j) = f (MkName i) in j) s
+
+-- | Perform a right fold of a function across all elements of a 'NameSet'
+foldr :: (forall (a::k). Name a -> r -> r) -> r -> NameSet k -> r
+foldr f r (NameSet s) = IntSet.foldr (f . MkName) r s
+
+-- | Perform a left fold of a function across all elements of a 'NameSet'
+foldl :: (forall (a::k). r -> Name a -> r) -> r -> NameSet k -> r
+foldl f r (NameSet s) = IntSet.foldl (\r -> f r . MkName) r s
+
+-- | Lift a 'NameSet' out of a name-binding by lifting all names not bound by
+-- the name-binding and then forming a 'NameSet' from those lifted names
+liftNameSet :: Mb ctx (NameSet (k :: Type)) -> NameSet k
+liftNameSet mb_s = fromList $ mapMaybe helper $ mbList $ fmap toList mb_s
+  where
+    helper :: forall ctx' k'. Mb ctx' (SomeName k') -> Maybe (SomeName k')
+    helper [nuP| SomeName mb_n |]
+      | Right n <- mbNameBoundP mb_n = Just (SomeName n)
+    helper _ = Nothing
diff --git a/src/Data/Binding/Hobbits/NuMatching.hs b/src/Data/Binding/Hobbits/NuMatching.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/NuMatching.hs
@@ -0,0 +1,579 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.NuMatching
+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@kestrel.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines the typeclass @'NuMatching' a@, which allows
+-- pattern-matching on the bodies of multi-bindings when their bodies
+-- have type a. To ensure adequacy, the actual machinery of how this
+-- works is hidden from the user, but, for any given (G)ADT @a@, the
+-- user can use the Template Haskell function 'mkNuMatching' to
+-- create a 'NuMatching' instance for @a@.
+--
+
+
+module Data.Binding.Hobbits.NuMatching (
+  NuMatching(..), mkNuMatching,
+  MbTypeRepr(), isoMbTypeRepr, unsafeMbTypeRepr,
+  NuMatchingAny1(..)
+) where
+
+import Data.Vector (Vector)
+import qualified Data.Vector as Vector
+--import Data.Typeable
+import Language.Haskell.TH hiding (Name, Type(..))
+import qualified Language.Haskell.TH as TH
+import Control.Monad.State
+import Numeric.Natural
+import Data.Functor.Constant
+import Data.Kind as DK
+import Data.Word
+import Data.Proxy
+import Data.Type.Equality
+--import Control.Monad.Identity
+
+import Data.Type.RList hiding (map)
+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 => NameRefresher -> a -> a
+mapNames = mapNamesPf nuMatchingProof
+
+matchDataDecl :: Dec -> Maybe (Cxt, TH.Name, [TyVarBndr], [Con])
+matchDataDecl (DataD cxt name tyvars _ constrs _) =
+  Just (cxt, name, tyvars, constrs)
+matchDataDecl (NewtypeD cxt name tyvars _ constr _) =
+  Just (cxt, name, tyvars, [constr])
+matchDataDecl _ = Nothing
+
+
+mkInstanceD :: Cxt -> TH.Type -> [Dec] -> Dec
+mkInstanceD = InstanceD Nothing
+
+{-|
+  Instances of the @'NuMatching' a@ class allow pattern-matching on
+  multi-bindings whose bodies have type @a@, i.e., on multi-bindings
+  of type @'Mb' ctx a@. The structure of this class is mostly hidden
+  from the user; see 'mkNuMatching' to see how to create instances
+  of the @NuMatching@ class.
+-}
+class NuMatching a where
+    nuMatchingProof :: MbTypeRepr a
+
+-- | Build an 'MbTypeRepr' for type @a@ by using an isomorphism with an
+-- already-representable type @b@. This is useful for building 'NuMatching'
+-- instances for, e.g., 'Integral' types, by mapping to and from 'Integer',
+-- without having to define instances for each one in this module.
+isoMbTypeRepr :: NuMatching b => (a -> b) -> (b -> a) -> MbTypeRepr a
+isoMbTypeRepr f_to f_from =
+  MbTypeReprData $ MkMbTypeReprData $ \refresher a ->
+  f_from $ mapNames refresher (f_to a)
+
+-- | Builds an 'MbTypeRepr' proof for use in a 'NuMatching' instance. This proof
+-- is unsafe because it does no renaming of fresh names, so should only be used
+-- for types that are guaranteed not to contain any 'Name' or 'Mb' values.
+unsafeMbTypeRepr :: MbTypeRepr a
+unsafeMbTypeRepr = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching (Name a) where
+    nuMatchingProof = MbTypeReprName
+
+instance NuMatching (Closed a) where
+    -- no need to map free variables in a Closed object
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\refresher -> id))
+
+instance (NuMatching a, NuMatching b) => NuMatching (a -> b) where
+    nuMatchingProof = MbTypeReprFun nuMatchingProof nuMatchingProof
+
+instance NuMatching a => NuMatching (Mb ctx a) where
+    nuMatchingProof = MbTypeReprMb nuMatchingProof
+
+instance NuMatching Bool where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Int where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Integer where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Char where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Natural where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Float where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Double where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Word where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Word8 where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Word16 where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Word32 where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching Word64 where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance NuMatching () where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))
+
+instance (NuMatching a, NuMatching b) => NuMatching (a,b) where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ \r (a,b) ->
+                                       (mapNames r a, mapNames r b))
+
+instance (NuMatching a, NuMatching b, NuMatching c) => NuMatching (a,b,c) where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ \r (a,b,c) ->
+                                       (mapNames r a, mapNames r b, mapNames r c))
+
+instance (NuMatching a, NuMatching b,
+          NuMatching c, NuMatching d) => NuMatching (a,b,c,d) where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ \r (a,b,c,d) ->
+                                       (mapNames r a, mapNames r b,
+                                        mapNames r c, mapNames r d))
+
+instance NuMatching a => NuMatching [a] where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\r -> map (mapNames r)))
+
+instance NuMatching a => NuMatching (Vector a) where
+    nuMatchingProof =
+      MbTypeReprData (MkMbTypeReprData $ (\r -> Vector.map (mapNames r)))
+
+
+{-
+type family NuMatchingListProof args
+type instance NuMatchingListProof Nil = ()
+type instance NuMatchingListProof (args :> arg) = (NuMatchingListProof args, MbTypeReprData arg)
+
+-- the NuMatchingList class, for saying that NuMatching holds for a context of types
+class NuMatchingList args where
+    nuMatchingListProof :: NuMatchingListProof args
+
+instance NuMatchingList Nil where
+    nuMatchingListProof = ()
+
+instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where
+    nuMatchingListProof = (nuMatchingListProof, nuMatchingProof)
+-}
+
+{-
+-- | An object-level reification of the 'NuMatching' class
+data NuMatchingObj a = NuMatching a => NuMatchingObj ()
+
+class NuMatchingList args where
+    nuMatchingListProof :: RAssign NuMatchingObj args
+
+instance NuMatchingList RNil where
+    nuMatchingListProof = MNil
+
+instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where
+    nuMatchingListProof = nuMatchingListProof :>: NuMatchingObj ()
+
+
+class NuMatching1 f where
+    nuMatchingProof1 :: NuMatching a => NuMatchingObj (f a)
+-}
+
+-- README: deriving NuMatching from NuMatching1 leads to overlapping instances
+-- for, e.g., Name a
+{-
+instance (NuMatching1 f, NuMatching a) => NuMatching (f a) where
+    nuMatchingProof = nuMatchingProof1 nuMatchingProof
+-}
+
+{-
+instance {-# OVERLAPPABLE #-} (NuMatching1 f, NuMatchingList ctx) =>
+                              NuMatching (RAssign f ctx) where
+    nuMatchingProof = MbTypeReprData $ MkMbTypeReprData $ helper nuMatchingListProof where
+        helper :: NuMatching1 f =>
+                  RAssign NuMatchingObj args -> NameRefresher ->
+                  RAssign f args -> RAssign f args
+        helper MNil r MNil = MNil
+        helper (proofs :>: NuMatchingObj ()) r (elems :>: (elem :: f a)) =
+            case nuMatchingProof1 :: NuMatchingObj (f a) of
+              NuMatchingObj () ->
+                  (helper proofs r elems) :>:
+                  mapNames r elem
+-}
+
+-- | Typeclass for lifting the 'NuMatching' constraint to functors on arbitrary
+-- kinds that do not require any constraints on their input types
+class NuMatchingAny1 (f :: k -> Type) where
+  nuMatchingAny1Proof :: MbTypeRepr (f a)
+
+instance {-# INCOHERENT #-} NuMatchingAny1 f => NuMatching (f a) where
+  nuMatchingProof = nuMatchingAny1Proof
+
+instance NuMatchingAny1 Name where
+  nuMatchingAny1Proof = nuMatchingProof
+
+instance NuMatchingAny1 ((:~:) a) where
+  nuMatchingAny1Proof = nuMatchingProof
+
+instance NuMatching a => NuMatchingAny1 (Constant a) where
+  nuMatchingAny1Proof = nuMatchingProof
+
+instance {-# OVERLAPPABLE #-} NuMatchingAny1 f => NuMatching (RAssign f ctx) where
+    nuMatchingProof = MbTypeReprData $ MkMbTypeReprData helper where
+        helper :: NuMatchingAny1 f => NameRefresher -> RAssign f args ->
+                  RAssign f args
+        helper r MNil = MNil
+        helper r (elems :>: elem) = helper r elems :>: mapNames r elem
+
+
+-- now we define some TH to create NuMatchings
+
+natsFrom i = i : natsFrom (i+1)
+
+fst3 :: (a,b,c) -> a
+fst3 (x,_,_) = x
+
+snd3 :: (a,b,c) -> b
+snd3 (_,y,_) = y
+
+thd3 :: (a,b,c) -> c
+thd3 (_,_,z) = z
+
+
+type Names = (TH.Name, TH.Name, TH.Name)
+
+mapNamesType a = [t| forall ctx. NameRefresher -> $a -> $a |]
+
+{-|
+  Template Haskell function for creating NuMatching instances for (G)ADTs.
+  Typical usage is to include the following line in the source file for
+  (G)ADT @T@ (here assumed to have two type arguments):
+
+> $(mkNuMatching [t| forall a b . T a b |])
+
+  The 'mkNuMatching' call here will create an instance declaration for
+  @'NuMatching' (T a b)@. It is also possible to include a context in the
+  forall type; for example, if we define the 'ID' data type as follows:
+
+> data ID a = ID a
+
+  then we can create a 'NuMatching' instance for it like this:
+
+> $( mkNuMatching [t| NuMatching a => ID a |])
+
+  Note that, when a context is included, the Haskell parser will add
+  the @forall a@ for you.
+-}
+mkNuMatching :: Q TH.Type -> Q [Dec]
+mkNuMatching tQ =
+    do t <- tQ
+       (cxt, cType, tName, constrs, tyvars) <- getMbTypeReprInfoTop t
+       fName <- newName "f"
+       refrName <- newName "refresher"
+       clauses <- getClauses (tName, fName, refrName) constrs
+       mapNamesT <- mapNamesType (return cType)
+       return [mkInstanceD
+               cxt (TH.AppT (TH.ConT ''NuMatching) cType)
+               [ValD (VarP 'nuMatchingProof)
+                (NormalB
+                 $ AppE (ConE 'MbTypeReprData)
+                   $ AppE (ConE 'MkMbTypeReprData)
+                         $ LetE [SigD fName
+                                 $ TH.ForallT (map PlainTV tyvars) cxt mapNamesT,
+                                 FunD fName clauses]
+                               (VarE fName)) []]]
+
+       {-
+       return (LetE
+               [SigD fName
+                     (TH.ForallT tyvars reqCxt
+                     $ foldl TH.AppT TH.ArrowT
+                           [foldl TH.AppT (TH.ConT conName)
+                                      (map tyVarToType tyvars)]),
+                FunD fname clauses]
+               (VarE fname))
+        -}
+    where
+      -- extract the name from a TyVarBndr
+      tyBndrToName (PlainTV n) = n
+      tyBndrToName (KindedTV n _) = n
+
+      -- fail for getMbTypeReprInfo
+      getMbTypeReprInfoFail t extraMsg =
+          fail ("mkMbTypeRepr: " ++ show t
+                ++ " is not a type constructor for a (G)ADT applied to zero or more distinct type variables" ++ extraMsg)
+
+      -- get info for conName (top-level call)
+      getMbTypeReprInfoTop t = getMbTypeReprInfo [] [] t t
+
+      -- get info for conName
+      getMbTypeReprInfo ctx tyvars topT (TH.ConT tName) =
+          do info <- reify tName
+             case info of
+               TyConI (matchDataDecl -> Just (_, _, tyvarsReq, constrs)) ->
+                 success tyvarsReq constrs
+               _ -> getMbTypeReprInfoFail topT (": info for " ++ (show tName) ++ " = " ++ (show info))
+          where
+            success tyvarsReq constrs =
+                let tyvarsRet = if tyvars == [] && ctx == []
+                                then map tyBndrToName tyvarsReq
+                                else tyvars in
+                return (ctx,
+                        foldl TH.AppT (TH.ConT tName) (map TH.VarT tyvars),
+                        tName, constrs, tyvarsRet)
+
+      getMbTypeReprInfo ctx tyvars topT (TH.AppT f (TH.VarT argName)) =
+          if elem argName tyvars then
+              getMbTypeReprInfoFail topT ""
+          else
+              getMbTypeReprInfo ctx (argName:tyvars) topT f
+
+      getMbTypeReprInfo ctx tyvars topT (TH.ForallT _ ctx' t) =
+          getMbTypeReprInfo (ctx ++ ctx') tyvars topT t
+
+      getMbTypeReprInfo ctx tyvars topT t = getMbTypeReprInfoFail topT ""
+
+      -- get the name from a data type
+      getTCtor t = getTCtorHelper t t []
+      getTCtorHelper (TH.ConT tName) topT tyvars = Just (topT, tName, tyvars)
+      getTCtorHelper (TH.AppT t1 (TH.VarT var)) topT tyvars =
+          getTCtorHelper t1 topT (tyvars ++ [var])
+      getTCtorHelper (TH.SigT t1 _) topT tyvars = getTCtorHelper t1 topT tyvars
+      getTCtorHelper _ _ _ = Nothing
+
+      -- get a list of Clauses, one for each constructor in constrs
+      getClauses :: Names -> [Con] -> Q [Clause]
+      getClauses _ [] = return []
+
+      getClauses names (NormalC cName cTypes : constrs) =
+        do clause <-
+             getClauseHelper names (map snd cTypes) (natsFrom 0)
+             (\l -> ConP cName (map (VarP . fst3) l))
+             (\l -> foldl AppE (ConE cName) (map fst3 l))
+           clauses <- getClauses names constrs
+           return $ clause : clauses
+
+      getClauses names (RecC cName cVarTypes : constrs) =
+        do clause <-
+             getClauseHelper names (map thd3 cVarTypes) (map fst3 cVarTypes)
+             (\l -> RecP cName (map (\(var,_,field) -> (field, VarP var)) l))
+             (\l -> RecConE cName (map (\(exp,_,field) -> (field, exp)) l))
+           clauses <- getClauses names constrs
+           return $ clause : clauses
+
+      getClauses names (InfixC cType1 cName cType2 : constrs) =
+        do clause <-
+             getClauseHelper names (map snd [cType1, cType2]) (natsFrom 0)
+             (\l -> ConP cName (map (VarP . fst3) l))
+             (\l -> foldl AppE (ConE cName) (map fst3 l))
+           clauses <- getClauses names constrs
+           return $ clause : clauses
+
+      getClauses names (GadtC cNames cTypes _ : constrs) =
+        do clauses1 <-
+             forM cNames $ \cName ->
+             getClauseHelper names (map snd cTypes) (natsFrom 0)
+             (\l -> ConP cName (map (VarP . fst3) l))
+             (\l -> foldl AppE (ConE cName) (map fst3 l))
+           clauses2 <- getClauses names constrs
+           return (clauses1 ++ clauses2)
+
+      getClauses names (RecGadtC cNames cVarTypes _ : constrs) =
+        do clauses1 <-
+             forM cNames $ \cName ->
+             getClauseHelper names (map thd3 cVarTypes) (map fst3 cVarTypes)
+             (\l -> RecP cName (map (\(var,_,field) -> (field, VarP var)) l))
+             (\l -> RecConE cName (map (\(exp,_,field) -> (field, exp)) l))
+           clauses2 <- getClauses names constrs
+           return (clauses1 ++ clauses2)
+
+      getClauses names (ForallC _ _ constr : constrs) =
+        getClauses names (constr : constrs)
+
+      getClauseHelper :: Names -> [TH.Type] -> [a] ->
+                         ([(TH.Name,TH.Type,a)] -> Pat) ->
+                         ([(Exp,TH.Type,a)] -> Exp) ->
+                         Q Clause
+      getClauseHelper names@(tName, fName, refrName) cTypes cData pFun eFun =
+          do varNames <- mapM (newName . ("x" ++) . show . fst)
+                         $ zip (natsFrom 0) cTypes
+             let varsTypesData = zip3 varNames cTypes cData
+             let expsTypesData = map (mkExpTypeData names) varsTypesData
+             return $ Clause [(VarP refrName), (pFun varsTypesData)]
+                        (NormalB $ eFun expsTypesData) []
+
+      mkExpTypeData :: Names -> (TH.Name,TH.Type,a) -> (Exp,TH.Type,a)
+      mkExpTypeData (tName, fName, refrName)
+                    (varName, getTCtor -> Just (t, tName', _), cData)
+          | tName == tName' =
+              -- the type of the arg is the same as the (G)ADT we are
+              -- recursing over; apply the recursive function
+              (foldl AppE (VarE fName)
+                         [(VarE refrName), (VarE varName)],
+               t, cData)
+      mkExpTypeData (tName, fName, refrName) (varName, t, cData) =
+          -- the type of the arg is not the same as the (G)ADT; call mapNames
+          (foldl AppE (VarE 'mapNames)
+                     [(VarE refrName), (VarE varName)],
+           t, cData)
+
+-- FIXME: old stuff below
+
+type CxtStateQ a = StateT Cxt Q a
+
+-- create a MkMbTypeReprData for a (G)ADT
+mkMkMbTypeReprDataOld :: Q TH.Name -> Q Exp
+mkMkMbTypeReprDataOld conNameQ =
+    do conName <- conNameQ
+       (cxt, name, tyvars, constrs) <- getMbTypeReprInfo conName
+       (clauses, reqCxt) <- runStateT (getClauses cxt name tyvars [] constrs) []
+       fname <- newName "f"
+       return (LetE
+               [SigD fname
+                     (TH.ForallT tyvars reqCxt
+                     $ foldl TH.AppT TH.ArrowT
+                           [foldl TH.AppT (TH.ConT conName)
+                                      (map tyVarToType tyvars)]),
+                FunD fname clauses]
+               (VarE fname))
+    where
+      -- convert a TyVar to a Name
+      tyVarToType (PlainTV n) = TH.VarT n
+      tyVarToType (KindedTV n _) = TH.VarT n
+
+      -- get info for conName
+      getMbTypeReprInfo conName =
+          reify conName >>= \info ->
+              case info of
+                TyConI (matchDataDecl -> Just (cxt, name, tyvars, constrs)) ->
+                    return (cxt, name, tyvars, constrs)
+                _ -> fail ("mkMkMbTypeReprData: " ++ show conName
+                           ++ " is not a (G)ADT")
+      {-
+      -- report failure
+      getMbTypeReprInfoFail t =
+          fail ("mkMkMbTypeReprData: " ++ show t
+                ++ " is not a fully applied (G)ADT")
+
+      getMbTypeReprInfo (TH.ConT conName) topT =
+          reify conName >>= \info ->
+              case info of
+                TyConI (DataD cxt name tyvars constrs _) ->
+                    return (cxt, name, tyvars, constrs)
+                _ -> getMbTypeReprInfoFail topT
+      getMbTypeReprInfo (TH.AppT t _) topT = getMbTypeReprInfo t topT
+      getMbTypeReprInfo (TH.SigT t _) topT = getMbTypeReprInfo t topT
+      getMbTypeReprInfo _ topT = getMbTypeReprInfoFail topT
+       -}
+
+      -- get a list of Clauses, one for each constructor in constrs
+      getClauses :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] -> [Con] ->
+                    CxtStateQ [Clause]
+      getClauses cxt name tyvars locTyvars [] = return []
+
+      getClauses cxt name tyvars locTyvars (NormalC cName cTypes : constrs) =
+        do clause <-
+             getClauseHelper cxt name tyvars locTyvars (map snd cTypes)
+             (natsFrom 0)
+             (\l -> ConP cName (map (VarP . fst3) l))
+             (\l -> foldl AppE (ConE cName) (map (VarE . fst3) l))
+           clauses <- getClauses cxt name tyvars locTyvars constrs
+           return (clause : clauses)
+
+      getClauses cxt name tyvars locTyvars (RecC cName cVarTypes : constrs) =
+        do clause <-
+             getClauseHelper cxt name tyvars locTyvars (map thd3 cVarTypes)
+             (map fst3 cVarTypes)
+             (\l -> RecP cName (map (\(var,_,field) -> (field, VarP var)) l))
+             (\l -> RecConE cName (map (\(var,_,field) -> (field, VarE var)) l))
+           clauses <- getClauses cxt name tyvars locTyvars constrs
+           return (clause : clauses)
+
+      getClauses cxt name tyvars locTyvars (InfixC cType1 cName cType2 : _) =
+        undefined -- FIXME
+
+      getClauses cxt name tyvars locTyvars (ForallC tyvars2 cxt2 constr
+                                            : constrs) =
+        do clauses1 <-
+             getClauses (cxt ++ cxt2) name tyvars (locTyvars ++ tyvars2) [constr]
+           clauses2 <- getClauses cxt name tyvars locTyvars constrs
+           return (clauses1 ++ clauses2)
+
+      getClauses cxt name tyvars locTyvars (GadtC cNames cTypes _ : constrs) =
+        do clauses1 <-
+             forM cNames $ \cName ->
+             getClauseHelper cxt name tyvars locTyvars (map snd cTypes)
+             (natsFrom 0) (\l -> ConP cName (map (VarP . fst3) l))
+             (\l -> foldl AppE (ConE cName) (map (VarE . fst3) l))
+           clauses2 <- getClauses cxt name tyvars locTyvars constrs
+           return (clauses1 ++ clauses2)
+
+      getClauses cxt name tyvars locTyvars (RecGadtC cNames cVarTypes _
+                                            : constrs) =
+        do clauses1 <-
+             forM cNames $ \cName ->
+             getClauseHelper cxt name tyvars locTyvars
+             (map thd3 cVarTypes) (map fst3 cVarTypes)
+             (\l -> RecP cName (map (\(var,_,field) -> (field, VarP var)) l))
+             (\l -> RecConE cName (map (\(var,_,field) -> (field, VarE var)) l))
+           clauses2 <- getClauses cxt name tyvars locTyvars constrs
+           return (clauses1 ++ clauses2)
+
+      getClauseHelper :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] ->
+                         [TH.Type] -> [a] ->
+                         ([(TH.Name,TH.Type,a)] -> Pat) ->
+                         ([(TH.Name,TH.Type,a)] -> Exp) ->
+                         CxtStateQ Clause
+      getClauseHelper cxt name tyvars locTyvars cTypes cData pFun eFun =
+          do varNames <- mapM (lift . newName . ("x" ++) . show . fst)
+                         $ zip (natsFrom 0) cTypes
+             () <- ensureCxt cxt locTyvars cTypes
+             let varsTypesData = zip3 varNames cTypes cData
+             return $ Clause [(pFun varsTypesData)]
+                        (NormalB $ eFun varsTypesData) []
+
+      -- ensure that MbTypeRepr a holds for each type a in cTypes
+      ensureCxt :: Cxt -> [TyVarBndr] -> [TH.Type] -> CxtStateQ ()
+      ensureCxt cxt locTyvars cTypes =
+          foldM (const (ensureCxt1 cxt locTyvars)) () cTypes
+
+      -- FIXME: it is not possible (or, at least, not easy) to determine
+      -- if MbTypeRepr a is implied from a current Cxt... so we just add
+      -- everything we need to the returned Cxt, except for 
+      ensureCxt1 :: Cxt -> [TyVarBndr] -> TH.Type -> CxtStateQ ()
+      ensureCxt1 cxt locTyvars t = undefined
+      {-
+      ensureCxt1 cxt locTyvars t = do
+        curCxt = get
+        let fullCxt = cxt ++ curCxt
+        isOk <- isMbTypeRepr fullCxt 
+
+      isMbTypeRepr 
+       -}
diff --git a/src/Data/Binding/Hobbits/NuMatchingInstances.hs b/src/Data/Binding/Hobbits/NuMatchingInstances.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/NuMatchingInstances.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE QuasiQuotes #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.NuMatchingInstances
+-- Copyright   : (c) 2020 Edwin Westbrook
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@galois.com
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- Provides a set of instances of 'NuMatching' for standard types using the
+-- template Haskell 'mkNuMatching' function
+
+module Data.Binding.Hobbits.NuMatchingInstances where
+
+import Data.Proxy
+import Data.Type.Equality
+import Data.Functor.Constant
+
+import Data.Type.RList
+import Data.Binding.Hobbits.Mb
+import Data.Binding.Hobbits.NuMatching (NuMatching, NuMatchingAny1, mkNuMatching)
+import Data.Binding.Hobbits.QQ (nuP)
+
+$(mkNuMatching [t| forall a. NuMatching a => Maybe a |])
+$(mkNuMatching [t| forall a b. (NuMatching a, NuMatching b) => Either a b |])
+$(mkNuMatching [t| forall ctx a. Member ctx a |])
+$(mkNuMatching [t| forall a. Proxy a |])
+$(mkNuMatching [t| forall a b. a :~: b |])
+$(mkNuMatching [t| forall a b. NuMatching a => Constant a b |])
diff --git a/src/Data/Binding/Hobbits/PatternParser.hs b/src/Data/Binding/Hobbits/PatternParser.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/PatternParser.hs
@@ -0,0 +1,34 @@
+-- |
+-- Module      : Data.Binding.Hobbits.PatternParser
+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- Using the haskell-src-meta package to parse Haskell patterns.
+
+module Data.Binding.Hobbits.PatternParser (parsePattern) where
+
+import Language.Haskell.TH
+
+import qualified Language.Haskell.Exts.Parser as Meta
+
+import qualified Language.Haskell.Meta.Parse as Meta
+
+import qualified Language.Haskell.Meta.Parse as Sloppy
+import qualified Language.Haskell.Meta.Syntax.Translate as Translate
+
+import qualified Language.Haskell.Exts.Extension as Exts
+
+parsePatternExtensions =
+  map Exts.EnableExtension $ Exts.ViewPatterns : Sloppy.myDefaultExtensions
+
+parsePattern :: String -> String -> Either String Pat
+parsePattern fn =
+  fmap Translate.toPat . Meta.parseResultToEither .
+  Meta.parsePatWithMode (Sloppy.myDefaultParseMode
+                    {Meta.parseFilename = fn,
+                     Meta.extensions = parsePatternExtensions })
diff --git a/src/Data/Binding/Hobbits/QQ.hs b/src/Data/Binding/Hobbits/QQ.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binding/Hobbits/QQ.hs
@@ -0,0 +1,148 @@
+{-# LANGUAGE TemplateHaskell, FlexibleContexts, PolyKinds #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.QQ
+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- Defines a quasi-quoter for writing patterns that match the bodies of 'Mb'
+-- multi-bindings. Uses the haskell-src-exts parser. @[nuP| P ]@ defines a
+-- pattern that will match a multi-binding whose body matches @P@. Any
+-- variables matched by @P@ will remain inside the binding; thus, for example,
+-- in the pattern @[nuP| x |]@, @x@ matches the entire multi-binding.
+--
+-- Examples:
+--
+-- > case (nu Left) of [nuP| Left x |] -> x  ==  nu id
+--
+-- @[clP| P |]@ does the same for the 'Closed' type, and @[clNuP| P |]@ works
+-- for both simultaneously: @'Closed' ('Mb' ctx a)@.
+
+module Data.Binding.Hobbits.QQ (nuP, clP, clNuP) where
+
+import Language.Haskell.TH.Syntax as TH
+import Language.Haskell.TH.Ppr as TH
+import Language.Haskell.TH.Quote
+
+import qualified Data.Generics as SYB
+import Control.Monad.Writer (runWriterT, tell)
+import Data.Monoid (Any(..))
+
+import qualified Data.Binding.Hobbits.Internal.Utilities as IU
+import Data.Binding.Hobbits.Internal.Mb
+import Data.Binding.Hobbits.Internal.Closed
+import Data.Binding.Hobbits.PatternParser (parsePattern)
+import Data.Binding.Hobbits.NuMatching
+
+
+-- | Helper function to apply an expression to multiple arguments
+appEMulti :: Exp -> [Exp] -> Exp
+appEMulti = foldl AppE
+
+-- | Helper function to apply the (.) operator on expressions
+compose :: Exp -> Exp -> Exp
+compose f g = VarE '(.) `AppE` f `AppE` g
+
+-- | @patQQ str pat@ builds a quasi-quoter named @str@ that parses
+-- | patterns with @pat@
+patQQ :: String -> (String -> Q Pat) -> QuasiQuoter
+patQQ n pat = QuasiQuoter (err "Exp") pat (err "Type") (err "Decs")
+  where err s = error $ "QQ `" ++ n ++ "' is for patterns, not " ++ s ++ "."
+
+
+-- | A @WrapKit@ specifies a transformation to be applied to variables
+-- | in a Template Haskell patterns, as follows:
+--
+-- * @_varView@ gives an expression for a function to be applied, as a
+--   view pattern, to variables before matching them, including to
+--   variables bound by @\@@ patterns;
+--
+-- * @_asXform@ gives a function to transform the bodies of \@
+--   patterns, i.e., this function is applied to @p@ in pattern @x\@p@;
+--
+-- * @_topXform@ gives a function to transform the whole pattern after
+--    @_varView@ and/or @_asXform@ have been applied to sub-patterns;
+--    as the first argument, @_topXform@ also takes a flag indicating
+--    whether any transformations have been applied to sub-patterns.
+--
+data WrapKit =
+  WrapKit {_varView :: Exp, _asXform :: Pat -> Pat, _topXform :: Bool -> Pat -> Pat}
+
+-- | Combine two WrapKits, composing the individual components
+combineWrapKits :: WrapKit -> WrapKit -> WrapKit
+combineWrapKits (WrapKit {_varView = varViewO, _asXform = asXformO, _topXform = topXformO})
+           (WrapKit {_varView = varViewI, _asXform = asXformI, _topXform = topXformI}) =
+  WrapKit {_varView = varViewO `compose` varViewI,
+           _asXform = asXformO . asXformI,
+           _topXform = \b -> topXformO b . topXformI b}
+
+-- | Apply a 'WrapKit' to a pattern
+wrapVars :: Monad m => WrapKit -> Pat -> m Pat
+wrapVars (WrapKit {_varView = varView, _asXform = asXform, _topXform = topXform}) pat = do
+  (pat', Any usedVarView) <- runWriterT m
+  return $ topXform usedVarView pat'
+  where
+    m = IU.everywhereButM (SYB.mkQ False isExp) (SYB.mkM w) pat
+      where isExp :: Exp -> Bool
+            -- don't recur into the expression part of view patterns
+            isExp _ = True
+
+    -- this should be called if the 'varView' function is ever used
+    hit x = tell (Any True) >> return x
+
+    -- wraps up bound names
+    w p@VarP{} = hit $ ViewP varView p
+    -- wraps for the bound name, then immediately unwraps
+    -- for the rest of the pattern
+    w (AsP v p) = hit $ ViewP varView $ AsP v $ asXform p
+    -- requires the expression to be closed
+    w (ViewP (VarE n) p) = return $ ViewP (VarE 'unClosed `AppE` VarE n) p
+    w (ViewP e _) = fail $ "view function must be a single name: `" ++ show (TH.ppr e) ++ "'"
+    w p = return p
+
+-- | Parse a pattern from a string, using 'parsePattern'
+parseHere :: String -> Q Pat
+parseHere s = do
+  fn <- loc_filename `fmap` location
+  case parsePattern fn s of
+    Left e -> error $ "Parse error: `" ++ e ++
+      "'\n\n\t when parsing pattern: `" ++ s ++ "'."
+    Right p -> return p
+
+
+-- | A helper function used to ensure two multi-bindings have the same contexts
+same_ctx :: Mb ctx a -> Mb ctx b -> Mb ctx b
+same_ctx _ x = x
+
+-- | Builds a 'WrapKit' for parsing patterns that match over 'Mb'.
+-- | Takes two fresh names as arguments.
+nuKit :: TH.Name -> TH.Name -> WrapKit
+nuKit topVar namesVar = WrapKit {_varView = varView, _asXform = asXform, _topXform = topXform} where
+  varView = (VarE 'same_ctx `AppE` VarE topVar) `compose`
+        (appEMulti (ConE 'MkMbPair) [VarE 'nuMatchingProof, VarE namesVar])
+  asXform p = ViewP (VarE 'ensureFreshPair) (TupP [WildP, p])
+  topXform b p = if b then AsP topVar $ ViewP (VarE 'ensureFreshPair) (TupP [VarP namesVar, p]) else asXform p
+
+-- | Quasi-quoter for patterns that match over 'Mb'
+nuP = patQQ "nuP" $ \s -> do
+  topVar <- newName "topMb"
+  namesVar <- newName "topNames"
+  parseHere s >>= wrapVars (nuKit topVar namesVar)
+
+-- | Builds a 'WrapKit' for parsing patterns that match over 'Closed'
+clKit = WrapKit {_varView = ConE 'Closed, _asXform = asXform, _topXform = const asXform}
+  where asXform p = ConP 'Closed [p]
+
+-- | Quasi-quoter for patterns that match over 'Closed', built using 'clKit'
+clP = patQQ "clP" $ (>>= wrapVars clKit) . parseHere
+
+-- | Quasi-quoter for patterns that match over @'Closed' ('Mb' ctx a)@
+clNuP = patQQ "clNuP" $ \s -> do
+  topVar <- newName "topMb"
+  namesVar <- newName "topNames"
+  parseHere s >>= wrapVars (clKit `combineWrapKits` nuKit topVar namesVar)
diff --git a/src/Data/Type/RList.hs b/src/Data/Type/RList.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/RList.hs
@@ -0,0 +1,232 @@
+{-# LANGUAGE TypeOperators, EmptyDataDecls, RankNTypes #-}
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, KindSignatures #-}
+{-# LANGUAGE GADTs, TypeInType, PatternGuards #-}
+
+-- |
+-- 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 Prelude hiding (map, foldr)
+import Data.Kind
+import Data.Type.Equality
+import Data.Proxy (Proxy(..))
+import Data.Functor.Constant
+import Data.Typeable
+
+-------------------------------------------------------------------------------
+-- * Right-lists as a datatype
+-------------------------------------------------------------------------------
+
+-- | A form of lists where elements are added to the right instead of the left
+data RList a
+  = RNil
+  | (RList a) :> a
+
+-- | Append two 'RList's at the type level
+type family ((r1 :: RList k) :++: (r2 :: RList k)) :: RList k
+infixr 5 :++:
+type instance (r :++: 'RNil) = r
+type instance (r1 :++: (r2 ':> a)) = (r1 :++: r2) ':> a
+
+-------------------------------------------------------------------------------
+-- * 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 :: RList k1) (a :: k2) 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) where
+    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
+
+instance TestEquality (Member ctx) where
+  testEquality Member_Base Member_Base = Just Refl
+  testEquality (Member_Step memb1) (Member_Step memb2)
+    | Just Refl <- testEquality memb1 memb2
+    = Just Refl
+  testEquality _ _ = Nothing
+
+instance Eq (Member ctx a) where
+  Member_Base == Member_Base = True
+  (Member_Step memb1) == (Member_Step memb2) = memb1 == memb2
+  _ == _ = False
+
+--toEq :: Member (Nil :> a) b -> b :~: a
+--toEq Member_Base = Refl
+--toEq _ = error "Should not happen! (toEq)"
+
+-- | Weaken a 'Member' proof by prepending another context to the context it
+-- proves membership in
+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)
+
+
+------------------------------------------------------------
+-- * 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)
+
+-- | Make an 'Append' proof from any 'RAssign' vector for the second
+-- argument of the append.
+mkAppend :: RAssign 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 -> RAssign f c2 -> Append c1 c2 (c1 :++: c2)
+mkMonoAppend _ = mkAppend
+
+-- | The inverse of 'mkAppend', that builds an 'RAssign' from an 'Append'
+proxiesFromAppend :: Append c1 c2 c -> RAssign Proxy c2
+proxiesFromAppend Append_Base = MNil
+proxiesFromAppend (Append_Step a) = proxiesFromAppend a :>: Proxy
+
+
+-------------------------------------------------------------------------------
+-- * Contexts
+-------------------------------------------------------------------------------
+
+{-|
+  An @RAssign f r@ an assignment of an @f a@ for each @a@ in the 'RList' @r@
+-}
+data RAssign (f :: k -> *) (c :: RList k) where
+  MNil :: RAssign f RNil
+  (:>:) :: RAssign f c -> f a -> RAssign f (c :> a)
+
+-- | Create an empty 'RAssign' vector.
+empty :: RAssign f RNil
+empty = MNil
+
+-- | Create a singleton 'RAssign' vector.
+singleton :: f a -> RAssign f (RNil :> a)
+singleton x = MNil :>: x
+
+-- | Look up an element of an 'RAssign' vector using a 'Member' proof
+get :: Member c a -> RAssign f c -> f a
+get Member_Base (_ :>: x) = x
+get (Member_Step mem') (mc :>: _) = get mem' mc
+
+-- | Heterogeneous type application, including a proof that the input kind of
+-- the function equals the kind of the type argument
+data HApply (f :: k1 -> Type) (a :: k2) where
+  HApply :: forall (f :: k -> Type) (a :: k). f a -> HApply f a
+
+-- | Look up an element of an 'RAssign' vector using a 'Member' proof at what
+-- GHC thinks might be a different kind, i.e., heterogeneously
+hget :: forall (f :: k1 -> Type) (c :: RList k1) (a :: k2).
+        Member c a -> RAssign f c -> HApply f a
+hget Member_Base (_ :>: x) = HApply x
+hget (Member_Step mem') (mc :>: _) = hget mem' mc
+
+-- | Modify an element of an 'RAssign' vector using a 'Member' proof.
+modify :: Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c
+modify Member_Base f (xs :>: x) = xs :>: f x
+modify (Member_Step mem') f (xs :>: x) = modify mem' f xs :>: x
+
+-- | Set an element of an 'RAssign' vector using a 'Member' proof.
+set :: Member c a -> f a -> RAssign f c -> RAssign f c
+set memb x = modify memb (const x)
+
+-- | Test if an object is in an 'RAssign', returning a 'Member' proof if it is
+memberElem :: TestEquality f => f a -> RAssign f ctx -> Maybe (Member ctx a)
+memberElem _ MNil = Nothing
+memberElem x (_ :>: y) | Just Refl <- testEquality x y = Just Member_Base
+memberElem x (xs :>: _) = fmap Member_Step $ memberElem x xs
+
+-- | Map a function on all elements of an 'RAssign' vector.
+map :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c
+map _ MNil = MNil
+map f (mc :>: x) = map f mc :>: f x
+
+-- | An alternate name for 'map' that does not clash with the prelude
+mapRAssign :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c
+mapRAssign = map
+
+-- | Map a binary function on all pairs of elements of two 'RAssign' vectors.
+map2 :: (forall x. f x -> g x -> h x) ->
+                RAssign f c -> RAssign g c -> RAssign h c
+map2 _ MNil MNil = MNil
+map2 f (xs :>: x) (ys :>: y) = map2 f xs ys :>: f x y
+
+-- | Take the tail of an 'RAssign'
+tail :: RAssign f (ctx :> a) -> RAssign f ctx
+tail (xs :>: _) = xs
+
+-- | Convert a monomorphic 'RAssign' to a list
+toList :: RAssign (Constant a) c -> [a]
+toList = mapToList getConstant
+
+-- | Map a function with monomorphic output type across an 'RAssign' to create a
+-- standard list:
+--
+-- > mapToList f = toList . map (Constant . f)
+mapToList :: (forall a. f a -> b) -> RAssign f ctx -> [b]
+mapToList _ MNil = []
+mapToList f (xs :>: x) = mapToList f xs ++ [f x]
+
+-- | Append two 'RAssign' vectors.
+append :: RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
+append mc MNil = mc
+append mc1 (mc2 :>: x) = append mc1 mc2 :>: x
+
+-- | Perform a right fold across an 'RAssign'
+foldr :: (forall a. f a -> r -> r) -> r -> RAssign f ctx -> r
+foldr _ r MNil = r
+foldr f r (xs :>: x) = f x $ foldr f r xs
+
+-- | Split an 'RAssign' vector into two pieces. The first argument is a
+-- phantom argument that gives the form of the first list piece.
+split :: (c ~ (c1 :++: c2)) => prx c1 ->
+                 RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)
+split _ MNil mc = (mc, MNil)
+split _ (any :>: _) (mc :>: x) = (mc1, mc2 :>: x)
+  where (mc1, mc2) = split Proxy any mc
+
+-- | Create a vector of proofs that each type in @c@ is a 'Member' of @c@.
+members :: RAssign f c -> RAssign (Member c) c
+members MNil = MNil
+members (c :>: _) = map Member_Step (members c) :>: Member_Base
+
+-- | 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 :: RAssign Proxy ctx
+
+instance TypeCtx RNil where
+  typeCtxProxies = MNil
+
+instance TypeCtx ctx => TypeCtx (ctx :> a) where
+  typeCtxProxies = typeCtxProxies :>: Proxy