diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,4 +1,11 @@
 
+1.2.2 -> 1.2.3
+- Renamed Cl and unCl to Closed and unClosed, respectively
+- Moved mkClosed to Internal/Closed.hs
+- Added the Closable typeclass
+- Added clApplyCl
+
+
 1.2.1 -> 1.2.2
 - Added NuMatching and Liftable instances for the unit type
 
diff --git a/Data/Binding/Hobbits/Closed.hs b/Data/Binding/Hobbits/Closed.hs
--- a/Data/Binding/Hobbits/Closed.hs
+++ b/Data/Binding/Hobbits/Closed.hs
@@ -16,11 +16,11 @@
 
 module Data.Binding.Hobbits.Closed (
   -- * Abstract types
-  Cl(),
-  -- * Operators involving 'Cl'
-  cl, clApply, unCl, noClosedNames,
-  -- * Synonyms
-  mkClosed, Closed, unClosed
+  Closed(),
+  -- * Operators involving 'Closed'
+  unClosed, mkClosed, noClosedNames, clApply, clMbApply, clApplyCl,
+  -- * Typeclass for inherently closed types
+  Closable(..)
 ) where
 
 import Data.Binding.Hobbits.Internal.Name
@@ -28,59 +28,10 @@
 import Data.Binding.Hobbits.Internal.Closed
 import Data.Binding.Hobbits.Mb
 
-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
-
-
--- | @cl@ is used with Template Haskell quotations to create closed terms of
--- type 'Cl'. A quoted expression is closed if all of the names occuring in it
--- are
---
---   1) bound globally or
---   2) bound within the quotation or
---   3) also of type 'Cl'.
-cl :: Q Exp -> Q Exp
-cl e = AppE (ConE 'Cl) `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 $ "`cl' does not allow dynamically bound names: `"
-      ++ show n ++ "'."
-  w e = return e
-
-  closed n = do
-    i <- TH.reify n
-    case i of
-      TH.VarI _ ty _ _ -> TH.expandSyns ty >>= w
-        where
-          w (AppT (ConT m) _) | m == ''Cl = return ()
-          w (ForallT _ _ ty) = w ty
-          w _ = fail $ "`cl` requires non-global variables to have type `Cl'.\n\t`"
-            ++ show (TH.ppr n) ++ "' does not. It's type is:\n\t `"
-            ++ show (TH.ppr ty) ++ "'."
-      _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."
-
-
-
--- | Closed terms are closed (sorry) under application.
-clApply :: Cl (a -> b) -> Cl a -> Cl b
--- could be defined with cl were it not for the GHC stage restriction
-clApply (Cl f) (Cl a) = Cl (f a)
-
--- | Closed multi-bindings are also closed under application.
-clMbApply :: Cl (Mb ctx (a -> b)) -> Cl (Mb ctx a) ->
-             Cl (Mb ctx b)
-clMbApply (Cl f) (Cl a) = Cl (mbApply f a)
-
 -- | @noClosedNames@ encodes the hobbits guarantee that no name can escape its
 -- multi-binding.
-noClosedNames :: Cl (Name a) -> b
-noClosedNames (Cl n) =
+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
@@ -89,11 +40,25 @@
       "... Clever girl!" ++
       "The `noClosedNames' invariant has somehow been violated."
 
--- | @mkClosed = cl@
-mkClosed = cl
+-- | 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 = Cl@
-type Closed = Cl
+-- | 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)
 
--- | @unClosed = unCl@
-unClosed x = unCl x
+-- | 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/Internal/Closed.hs b/Data/Binding/Hobbits/Internal/Closed.hs
--- a/Data/Binding/Hobbits/Internal/Closed.hs
+++ b/Data/Binding/Hobbits/Internal/Closed.hs
@@ -18,11 +18,45 @@
 
 module Data.Binding.Hobbits.Internal.Closed where
 
-{-|
-  The type @Cl 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 @Cl@ data type is hidden, and the user can only create
-  closed terms using Template Haskell, through the 'cl' operator.
--}
-newtype Cl a = Cl { unCl :: a }
+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 }
+
+-- | @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
+    i <- TH.reify n
+    case i of
+      TH.VarI _ ty _ _ -> TH.expandSyns ty >>= w
+        where
+          w (AppT (ConT m) _) | m == ''Closed = return ()
+          w (ForallT _ _ ty) = w ty
+          w _ = 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 ty) ++ "'."
+      _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."
diff --git a/Data/Binding/Hobbits/NuMatching.hs b/Data/Binding/Hobbits/NuMatching.hs
--- a/Data/Binding/Hobbits/NuMatching.hs
+++ b/Data/Binding/Hobbits/NuMatching.hs
@@ -23,7 +23,7 @@
 
 module Data.Binding.Hobbits.NuMatching (
   NuMatching(..), mkNuMatching, NuMatchingList(..), NuMatching1(..),
-  MbTypeRepr()
+  MbTypeRepr(), isoMbTypeRepr
 ) where
 
 --import Data.Typeable
@@ -56,7 +56,7 @@
 instance NuMatching (Name a) where
     nuMatchingProof = MbTypeReprName
 
-instance NuMatching (Cl a) where
+instance NuMatching (Closed a) where
     -- no need to map free variables in a Closed object
     nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
 
@@ -151,6 +151,16 @@
               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
diff --git a/Data/Binding/Hobbits/QQ.hs b/Data/Binding/Hobbits/QQ.hs
--- a/Data/Binding/Hobbits/QQ.hs
+++ b/Data/Binding/Hobbits/QQ.hs
@@ -20,8 +20,8 @@
 --
 -- > case (nu Left) of [nuP| Left x |] -> x  ==  nu id
 --
--- [clP| P |] does the same for the Cl type, and [clNuP| P |] works for
--- both simultaneously: Cl (Mb ctx a).
+-- @[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
 
@@ -101,7 +101,7 @@
     -- 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 'unCl `AppE` VarE n) p
+    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
 
@@ -134,14 +134,14 @@
   namesVar <- newName "topNames"
   parseHere s >>= wrapVars (nuKit topVar namesVar)
 
--- | Builds a 'WrapKit' for parsing patterns that match over 'Cl'
-clKit = WrapKit {_varView = ConE 'Cl, _asXform = asXform, _topXform = const asXform}
-  where asXform p = ConP 'Cl [p]
+-- | 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 'Cl', built using 'clKit'
+-- | Quasi-quoter for patterns that match over 'Closed', built using 'clKit'
 clP = patQQ "clP" $ (>>= wrapVars clKit) . parseHere
 
--- | Quasi-quoter for patterhs that match over @'Cl' ('Mb' ctx a)@
+-- | Quasi-quoter for patterns that match over @'Closed' ('Mb' ctx a)@
 clNuP = patQQ "clNuP" $ \s -> do
   topVar <- newName "topMb"
   namesVar <- newName "topNames"
diff --git a/hobbits.cabal b/hobbits.cabal
--- a/hobbits.cabal
+++ b/hobbits.cabal
@@ -1,5 +1,5 @@
 Name:                hobbits
-Version:             1.2.2
+Version:             1.2.3
 Synopsis:            A library for canonically representing terms with binding
 
 Description: A library for canonically representing terms with binding via a