diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,7 @@
+0.1.0.2
+---
+GHC 8.8.3 -> GHC 8.10.1
+
 0.1.0.1
 ---
 Fixed build error with Haddock documentation (missing file)
diff --git a/nom.cabal b/nom.cabal
--- a/nom.cabal
+++ b/nom.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.0
 name:               nom
-version:            0.1.0.1
+version:            0.1.0.2
 description:        Nominal-flavoured implementation of data in a context of local names, following the ideas in <https://link.springer.com/article/10.1007/s001650200016 a new approach to abstract syntax with variable binding> (see also <http://www.gabbay.org.uk/papers.html#newaas-jv author's pdfs>).
                     __The recommended landing page is "Language.Nominal", so please go there first.__ See also: a tutorial in "Language.Nominal.Examples.Tutorial"; a short development of untyped lambda-calculus in "Language.Nominal.Examples.UntypedLambda"; an example development of System F in "Language.Nominal.Examples.SystemF"; and an example development of an EUTxO-style blockchain in "Language.Nominal.Examples.IdealisedEUTxO".
 homepage:           https://github.com/bellissimogiorno/nominal#readme
@@ -44,6 +44,7 @@
       Language.Nominal.Unique
       Language.Nominal.Equivar
       Language.Nominal.Examples.SystemF
+      Language.Nominal.Examples.Graph
       Language.Nominal.Examples.IdealisedEUTxO
       Language.Nominal.Examples.UntypedLambda
       Language.Nominal.Examples.Assembly1
diff --git a/src/Language/Nominal.hs b/src/Language/Nominal.hs
--- a/src/Language/Nominal.hs
+++ b/src/Language/Nominal.hs
@@ -92,7 +92,7 @@
 /Note:/ "having empty support" does /not/ mean "having no atoms".  It means "symmetric under swapping atoms", which is not at all the same idea. 
 * 'Language.Nominal.Name.Nameless': types like @Int@, @String@, and @()@ that are guaranteed atoms-free. 
 * 'Language.Nominal.Nom.KNom' and 'Language.Nominal.Nom.Nom': An atoms-binding monad.
-* 'Language.Nominal.Nom.Binder': A typeclass for functions acting on binding types.
+* 'Language.Nominal.Binder.Binder': A typeclass for functions acting on binding types.
 * 'Language.Nominal.Abs.KAbs' and 'Language.Nominal.Abs.Abs': A name-abstracting functor.
 * 'Language.Nominal.Name.KRestrict' and 'Language.Nominal.Name.Restrict': A typeclass of types with an inherent notion of atoms-binding.
 * 'Language.Nominal.Unify.KUnifyPerm' and 'Language.Nominal.Unify.UnifyPerm': Typeclasses of types with a notion of unification by injective partial functions on atoms.
diff --git a/src/Language/Nominal/Examples/Graph.hs b/src/Language/Nominal/Examples/Graph.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Nominal/Examples/Graph.hs
@@ -0,0 +1,84 @@
+{-|
+Module      : Algebraic graphs with binding 
+Description : Extending algebraic graphs with nominal-style binding 
+Copyright   : (c) Murdoch J. Gabbay, 2020
+License     : GPL-3
+Maintainer  : murdoch.gabbay@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+A development file to build on <https://hackage.haskell.org/package/algebraic-graphs Andrey Mokhov's algebraic-graphs> library.
+__THIS FILE IS UNDER DEVELOPMENT__
+Connect should be implemented such that only /free/ vertices are connected; not bound ones.  Overlay should be capture-avoiding (which should be automatic). 
+-}
+
+{-# LANGUAGE InstanceSigs          
+           , DeriveGeneric         
+           , FlexibleContexts 
+           , LambdaCase 
+           , MultiParamTypeClasses 
+           , DeriveAnyClass       -- to derive 'Swappable' 
+           , DeriveDataTypeable   -- to derive 'Data' 
+           , FlexibleInstances     
+           , TypeOperators        -- to use :. in instances
+#-}
+
+
+module Language.Nominal.Examples.Graph
+    where
+
+import GHC.Generics
+-- import Data.Generics     hiding (Generic, typeOf)
+-- import Algebra.Graph.HigherKinded.Class 
+-- import Control.Compose -- for :.
+-- import Data.Function    ((&))
+
+import Language.Nominal.Name 
+import Language.Nominal.NameSet 
+import Language.Nominal.Nom
+
+-- | A datatype of graphs with binding.  
+-- Perhaps should parameterise over atom type (see 'KAtom').  For now, I use the default atom type 'Tom'.
+data Graph a = Empty
+             | Vertex a
+             | Overlay (Graph a) (Graph a)
+             | Connect (Graph a) (Graph a)
+             | Restrict (Nom (Graph a))
+             deriving (Show, Generic, Swappable)
+
+-- | Restriction action just passes the restriction on to the deep embedding
+instance Swappable a => KRestrict Tom (Graph a) where
+   restrict atms g = Restrict (res atms g)
+
+-- | Fold on graphs with binding.  
+-- Just like fold on graphs, but with an extra restriction operation, which we go under in a capture-avoiding manner. 
+foldg :: b -> (a -> b) -> (b -> b -> b) -> (b -> b -> b) -> (Nom b -> b) -> Graph a -> b
+foldg e v o c r = go
+  where
+    go Empty         = e
+    go (Vertex  x  ) = v x
+    go (Overlay x y) = o (go x) (go y)
+    go (Connect x y) = c (go x) (go y)
+    go (Restrict x') = r (go <$> x') -- special operators, like @@! and @@., are available to construct @r@. 
+{-# INLINE [0] foldg #-}
+
+-- | Filter a list of vertices to obtain those vertices for which @atms :: ['Atom']@ is fresh 
+filterApart :: Support a => [Atom] -> [a] -> [a]
+filterApart atms = filter $ apart atms
+
+{- instance Graph g => Graph ((KNom s) :. g) where
+   connect :: (KNom s :. g) a -> (KNom s :. g) a -> (KNom s :. g) a
+   connect g1' g2' = O $ (unO g1') @@. \gas1 g1 -> (unO g2') @@. \gas2 g2 ->
+      let h1 = filter (kapart (Proxy :: Proxy s) gas1) (vertices g1) 
+          h2 = filter (kapart (Proxy :: Proxy s) gas2) (vertices g2) 
+      in
+          res $ g1 <|> g2 <|> (biclique h1 h2)
+-}
+   
+{-
+   connect g1' g2' = O $ (genUnNom' . unO $ g1') & \(gas1, g1) -> (genUnNom' . unO $ g2') & \(gas2, g2) ->
+      let h1 = filter (kapart gas1) (vertices g1) 
+          h2 = filter (kapart gas2) (vertices g2) 
+      in
+          res $ g1 <|> g2 <|> (biclique h1 h2)
+-}
diff --git a/src/Language/Nominal/Examples/UntypedLambda.hs b/src/Language/Nominal/Examples/UntypedLambda.hs
--- a/src/Language/Nominal/Examples/UntypedLambda.hs
+++ b/src/Language/Nominal/Examples/UntypedLambda.hs
@@ -47,7 +47,7 @@
 data Exp = V Var              -- ^ Variable 
          | Exp :@ Exp         -- ^ Application 
          | Lam (KAbs Var Exp) -- ^ Lambda, using abstraction-type 
- deriving (Eq, Generic, Data, Swappable, Show)
+ deriving (Eq, Generic, Data, Swappable) -- , Show)
 
 -- | helper for building lambda-abstractions 
 lam :: Var -> Exp -> Exp 
@@ -77,14 +77,12 @@
 
 -- | weak head normal form of a lambda-term.
 whnf :: Exp -> Exp 
-whnf (f :@ a) = case whnf f of
-  Lam b' -> whnf $ b' `conc` a  
-  f'     -> f' :@ a
-whnf e = e
+whnf (Lam b' :@ a) = whnf $ b' `conc` a  
+whnf             e = e
 
 -- | (\x x) y
 example1 :: Exp
-example1 = (\[x, y] -> lam x $ V x :@ V y) `genAppC` freshNames ["x", "y"] 
+example1 = (\[x, y] -> lam x (V x) :@ V y) `genAppC` freshNames ["x", "y"] 
 -- | y
 example1whnf :: Exp
 example1whnf = whnf example1
@@ -96,3 +94,8 @@
 example2whnf :: Exp
 example2whnf = whnf example2
 
+instance Show Exp where
+   show     (V v) = show v 
+   show   (Lam e) = "(λ" ++ (show e) ++ ")"
+   show (e :@ e') = (show e) ++ " " ++ (show e')
+ 
diff --git a/src/Language/Nominal/Name.hs b/src/Language/Nominal/Name.hs
--- a/src/Language/Nominal/Name.hs
+++ b/src/Language/Nominal/Name.hs
@@ -291,7 +291,7 @@
 kswpN :: (Typeable s, Swappable a) => KName s t -> KName s t -> a -> a
 kswpN n n' = kswp (nameAtom n) (nameAtom n') 
 
--- | A name swap for a @'Tom'@-name.  Discards the names' labels and calls a @'Tom'@-atom swapping.
+-- | A name swap for a @'Tom'@-name.  Discards the names' labels and calls a @'Tom'@-swapping.
 swpN :: Swappable a => Name t -> Name t -> a -> a
 swpN = kswpN 
 
@@ -314,26 +314,28 @@
 
 deriving via Nameless Bool instance Swappable Bool
 deriving via Nameless Int  instance Swappable Int
+deriving via Nameless Integer instance Swappable Integer
 deriving via Nameless ()   instance Swappable ()
 deriving via Nameless Char instance Swappable Char
 
-
 -- * Generics support for @'KSwappable'@
 
 class GSwappable f where
     gswp :: Typeable s => KAtom s -> KAtom s -> f x -> f x
 
+-- Distributes through datatype-formers
+instance (GSwappable f, GSwappable g) => GSwappable ((:*:) f g) where  -- products
+    gswp m n (x :*: y) = gswp m n x :*: gswp m n y
+-- Action on a leaf is trivial
+instance GSwappable U1 where   -- one constructor, no arguments
+    gswp _ _ U1 = U1
+
 instance GSwappable V1 where   -- empty types, no instances
     gswp _ _ x = case x of
 
-instance GSwappable U1 where   -- one constructor, no arguments
-    gswp _ _ U1 = U1
 
 instance Swappable c => GSwappable (K1 i c) where  -- base case.  wrapper for all of some type c so we escape back out to swp.  
     gswp m n x = K1 $ kswp m n $ unK1 x
-
-instance (GSwappable f, GSwappable g) => GSwappable ((:*:) f g) where  -- products
-    gswp m n (x :*: y) = gswp m n x :*: gswp m n y
 
 instance (GSwappable f, GSwappable g) => GSwappable ((:+:) f g) where  -- sums
     gswp m n (L1 x) = L1 $ gswp m n x
diff --git a/src/Language/Nominal/NameSet.hs b/src/Language/Nominal/NameSet.hs
--- a/src/Language/Nominal/NameSet.hs
+++ b/src/Language/Nominal/NameSet.hs
@@ -89,6 +89,7 @@
 deriving via Nameless Bool instance Typeable s => KSupport s Bool
 deriving via Nameless Char instance Typeable s => KSupport s Char
 deriving via Nameless Int  instance Typeable s => KSupport s Int
+deriving via Nameless Integer instance Typeable s => KSupport s Integer
 
 -- order: nameless, tuple, list, nonempty list, maybe, sum, atom, name, nom, abs 
 instance (Typeable s, Typeable t) => KSupport s (KAtom t) where  
@@ -156,7 +157,8 @@
 
 -- | Form of restriction that takes names instead of atoms.  Just discards name labels and calls @'restrict'@.
 restrictN :: KRestrict s a => [KName s t] -> a -> a
-restrictN l = restrict (nameAtom <$> l)
+restrictN = restrict . (fmap nameAtom) 
+-- restrictN l = restrict (nameAtom <$> l)
 
 
 -- | Restriction is trivial on elements of nameless types 
@@ -187,20 +189,21 @@
 class GSupport s f where
     gsupp :: f x -> Set (KAtom s)
 
-instance GSupport s V1 where
-    gsupp x = case x of
-
+-- | Support distributes through datatype-formers, taking unions
+instance (GSupport s f, GSupport s g) => GSupport s (f :*: g) where
+    gsupp (x :*: y) = gsupp x `S.union` gsupp y
+-- | Leaf has empty support
 instance GSupport s U1 where
     gsupp U1 = S.empty
 
+instance GSupport s V1 where
+    gsupp x = case x of
+
 instance GSupport s f => GSupport s (M1 i t f) where
     gsupp = gsupp . unM1
 
 instance KSupport s c => GSupport s (K1 i c) where
     gsupp = ksupp Proxy . unK1
-
-instance (GSupport s f, GSupport s g) => GSupport s (f :*: g) where
-    gsupp (x :*: y) = gsupp x `S.union` gsupp y
 
 instance (GSupport s f, GSupport s g) => GSupport s (f :+: g) where
     gsupp (L1 x) = gsupp x
diff --git a/src/Language/Nominal/Nom.hs b/src/Language/Nominal/Nom.hs
--- a/src/Language/Nominal/Nom.hs
+++ b/src/Language/Nominal/Nom.hs
@@ -46,7 +46,9 @@
      -- * Destroying a @'Nom'@
      , unNom, nomToIO
      -- * Creating fresh ids in a @'Nom'@
-     , freshKAtom, freshAtom, freshKAtoms, freshAtoms, freshKName, freshName, freshKNames, freshNames -- , atFresh
+     , freshKAtom, freshAtom, freshKAtoms, freshAtoms 
+     , freshKName, freshName, freshKNames, freshNames 
+     , freshKNameIO, freshNameIO, freshKNamesIO, freshNamesIO 
      -- * 'KNom' and other functors
      -- $functor
      , transposeNomF 
@@ -189,7 +191,7 @@
 -- * Creating fresh ids in a @'Nom'@
 
 -- | Create a fresh atom-in-nominal-context
-freshKAtom :: Typeable s => KNom s (KAtom s)
+freshKAtom :: KNom s (KAtom s)
 freshKAtom = Nom $ do -- IO monad
    [a] <- freshKAtomsIO [()]
    return $ enter [a] a
@@ -199,7 +201,7 @@
 freshAtom = freshKAtom
 
 -- | Fresh @'Traversable' m@ of atoms (e.g. @m@ is list or stream)
-freshKAtoms :: (Traversable m, Typeable s) => m t -> KNom s (m (KAtom s))
+freshKAtoms :: Traversable m => m t -> KNom s (m (KAtom s))
 freshKAtoms = mapM (const freshKAtom)
 
 -- | Fresh @'Traversable' m@ of atoms (e.g. @m@ is list or stream).
@@ -207,12 +209,13 @@
 freshAtoms :: Traversable m => m t -> Nom (m Atom)
 freshAtoms = freshKAtoms
 
+
 -- | Create a fresh name-in-a-nominal-context with label @t@
-freshKName :: Typeable s => t -> KNom s (KName s t)
+freshKName :: t -> KNom s (KName s t)
 freshKName t = freshKAtom <&> Name t
 
 -- | Create fresh names-in-a-nominal-context
-freshKNames :: (Traversable m, Typeable s) => m t -> KNom s (m (KName s t))
+freshKNames :: Traversable m => m t -> KNom s (m (KName s t))
 freshKNames = mapM freshKName
 
 -- | Canonical version of 'freshKName' for @'Tom'@ name.
@@ -223,6 +226,24 @@
 freshNames :: Traversable m => m t -> Nom (m (Name t))
 freshNames = freshKNames
 
+
+-- | Create a fresh name-in-a-nominal-context with label @t@
+freshKNameIO :: t -> IO (KName s t)
+freshKNameIO = nomToIO . freshKName  
+
+-- | Create fresh names-in-a-nominal-context
+freshKNamesIO :: Traversable m => m t -> IO (m (KName s t))
+freshKNamesIO = nomToIO . freshKNames
+
+-- | Canonical version of 'freshKName' for @'Tom'@ name.
+freshNameIO :: t -> IO (Name t)
+freshNameIO = nomToIO . freshKName
+
+-- | Canonical version of 'freshKNames' for @'Tom'@ names.
+freshNamesIO :: Traversable m => m t -> IO (m (Name t))
+freshNamesIO = nomToIO . freshKNames
+
+
 {-- 
 -- | atFresh f returns the value of f at a fresh name with label @t@
 atFresh :: Typeable s => t -> (KName s t -> a) -> KNom s a
@@ -239,11 +260,10 @@
 * 'transposeMF'
 * 'transposeFM'
 
-Taken together, these functions are making a point that 'KNom' is compatible with your favourite container type.  Because 'KNom' can commuted, there is no need to wonder whether (for example) a graph-with-binding should be a graph with binding on the vertices, or on the edges, or on the graph overall, or any combination.  All of these are valid design decisions and one may be more /convenient/ than the other, but in the end we can isomorphically commute to a single top-level 'KNom' binding.
+Taken together, these functions are making a point that 'KNom' is compatible with your favourite container type.  Because 'KNom' commutes, there is no need to wonder whether (for example) a graph-with-binding should be a graph with binding on the vertices, or on the edges, or on the graph overall, or any combination.  All of these are valid design decisions and one may be more /convenient/ than the other, but we know we can isomorphically commute to a single top-level 'KNom' binding.
 
 In that sense, 'KNom' captures a general theory of binding.
-It is also a mathematical justification for why the 'Language.Nominal.Binder.Binder' typeclass turns out to be so useful.
-
+This also mathematically justifies why the 'Language.Nominal.Binder.Binder' typeclass is so useful.
 -}
 
 
diff --git a/src/Language/Nominal/Sub.hs b/src/Language/Nominal/Sub.hs
--- a/src/Language/Nominal/Sub.hs
+++ b/src/Language/Nominal/Sub.hs
@@ -67,10 +67,11 @@
 instance KSub n x (Nameless a) where
    sub _ _ = id
 
-deriving via Nameless Bool instance KSub n x Bool
-deriving via Nameless Int  instance KSub n x Int
 deriving via Nameless ()   instance KSub n x ()
+deriving via Nameless Bool instance KSub n x Bool
 deriving via Nameless Char instance KSub n x Char
+deriving via Nameless Int  instance KSub n x Int
+deriving via Nameless Integer instance KSub n x Integer
 
 instance (KSub n x a, KSub n x b) => KSub n x (a, b)
 instance (KSub n x a, KSub n x b, KSub n x c) => KSub n x (a, b, c)
@@ -109,20 +110,21 @@
 class GSub n x f where
     gsub :: n -> x -> f w -> f w 
 
-instance GSub n x V1 where
-    gsub _ _ y = case y of
-
+-- | Distributes through datatype-formers
+instance (GSub n x f, GSub n x g) => GSub n x (f :*: g) where
+    gsub n x (y :*: z) = gsub n x y :*: gsub n x z
+-- | Action on a leaf is trivial
 instance GSub n x U1 where
     gsub _ _ = id
 
+instance GSub n x V1 where
+    gsub _ _ y = case y of
+
 instance GSub n x f => GSub n x (M1 i t f) where
     gsub n x = M1 . gsub n x . unM1
 
 instance KSub n x c => GSub n x (K1 i c) where
     gsub n x = K1 . sub n x . unK1
-
-instance (GSub n x f, GSub n x g) => GSub n x (f :*: g) where
-    gsub n x (y :*: z) = gsub n x y :*: gsub n x z
 
 instance (GSub n x f, GSub n x g) => GSub n x (f :+: g) where
     gsub n x (L1 y) = L1 $ gsub n x y
diff --git a/src/Language/Nominal/Unify.hs b/src/Language/Nominal/Unify.hs
--- a/src/Language/Nominal/Unify.hs
+++ b/src/Language/Nominal/Unify.hs
@@ -255,10 +255,11 @@
         | otherwise = Ren Nothing
     ren _ = id
 
-deriving via Nameless Bool instance Typeable s => KUnifyPerm s Bool
-deriving via Nameless Int  instance Typeable s => KUnifyPerm s Int
 deriving via Nameless ()   instance Typeable s => KUnifyPerm s ()
+deriving via Nameless Bool instance Typeable s => KUnifyPerm s Bool
 deriving via Nameless Char instance Typeable s => KUnifyPerm s Char
+deriving via Nameless Int  instance Typeable s => KUnifyPerm s Int
+deriving via Nameless Integer instance Typeable s => KUnifyPerm s Integer
 
 instance (KUnifyPerm s a, KUnifyPerm s b) => KUnifyPerm s (a, b)
 instance (KUnifyPerm s a, KUnifyPerm s b, KUnifyPerm s c) => KUnifyPerm s (a, b, c)
@@ -330,17 +331,19 @@
     gunifyPerm :: f x -> f x -> KRen s
     gren       :: KRen s -> f x -> f x
 
-instance GUnifyPerm s V1 where
-    gunifyPerm x = case x of
-    gren _ x = case x of
+-- Unifiers accumulate on datatype-formers
+instance (GUnifyPerm s f, GUnifyPerm s g) => GUnifyPerm s (f :*: g) where
+    gunifyPerm (x1 :*: y1) (x2 :*: y2) = gunifyPerm x1 x2 <> gunifyPerm y1 y2
+    gren r (x :*: y) = gren r x :*: gren r y
 
+-- Unifier on a leaf is trivial
 instance GUnifyPerm s U1 where
     gunifyPerm U1 U1 = mempty
     gren _ U1 = U1
 
-instance (GUnifyPerm s f, GUnifyPerm s g) => GUnifyPerm s (f :*: g) where
-    gunifyPerm (x1 :*: y1) (x2 :*: y2) = gunifyPerm x1 x2 <> gunifyPerm y1 y2
-    gren r (x :*: y) = gren r x :*: gren r y
+instance GUnifyPerm s V1 where
+    gunifyPerm x = case x of
+    gren _ x = case x of
 
 instance (GUnifyPerm s f, GUnifyPerm s g) => GUnifyPerm s (f :+: g) where
 
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,9 +1,7 @@
-resolver: lts-15.8
+resolver: nightly-2020-07-14
 packages:
 - .
 extra-deps:
- - Unique-0.4.7.7@sha256:2269d3528271e25d34542e7c24a4e541e27ec33460e1ea00845da95b82eec6fa,2777
- - algebra-4.3.1@sha256:323cf20c508e0b71422b767ff3a89e4188f68aa59b2df9d0fe6e9f9bae7938fb,4129
- - extra-1.6.21
- - finite-typelits-0.1.4.2  # for Data.Finite in IdealisedEUTxOSpec
- - data-default-0.7.1.1     # for Data.Default
+- Unique-0.4.7.7@sha256:2269d3528271e25d34542e7c24a4e541e27ec33460e1ea00845da95b82eec6fa,2777
+- algebra-4.3.1@sha256:323cf20c508e0b71422b767ff3a89e4188f68aa59b2df9d0fe6e9f9bae7938fb,4129
+- extra-1.6.21@sha256:1e04429779702160356af6b3b8dd8531d5997f69bb1419f80a1a33b690c92f25,2757