diff --git a/examples/NanoFeldspar.hs b/examples/NanoFeldspar.hs
--- a/examples/NanoFeldspar.hs
+++ b/examples/NanoFeldspar.hs
@@ -160,10 +160,8 @@
       -- arguments of higher-order constructs such as `Parallel` are always
       -- lambdas.
     sharable (sel :$ _) _
-        | Just Sel1 <- prj sel = False
-        | Just Sel2 <- prj sel = False
-        | Just Sel3 <- prj sel = False
-        | Just Sel4 <- prj sel = False
+        | Just Fst <- prj sel = False
+        | Just Snd <- prj sel = False
       -- Tuple selection not shared
     sharable (arrl :$ _ ) _
         | Just (Construct "arrLen" _) <- prj arrl = False
diff --git a/src/Data/NestTuple.hs b/src/Data/NestTuple.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/NestTuple.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+-- | Conversion between tuples and nested pairs
+
+module Data.NestTuple where
+
+
+
+import Data.NestTuple.TH
+
+
+
+-- | Tuples that can be converted to/from nested pairs
+class Nestable tup
+  where
+    -- | Representation as nested pairs
+    type Nested tup
+    -- | Convert to nested pairs
+    nest :: tup -> Nested tup
+    -- | Convert from nested pairs
+    unnest :: Nested tup -> tup
+
+mkNestableInstances 15
+
diff --git a/src/Data/NestTuple/TH.hs b/src/Data/NestTuple/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/NestTuple/TH.hs
@@ -0,0 +1,74 @@
+module Data.NestTuple.TH where
+
+
+
+import Language.Haskell.TH
+
+import Language.Syntactic.TH
+
+
+
+mkTupT :: [Type] -> Type
+mkTupT ts = foldl AppT (TupleT (length ts)) ts
+
+mkPairT :: Type -> Type -> Type
+mkPairT a b = foldl AppT (TupleT 2) [a,b]
+
+mkPairE :: Exp -> Exp -> Exp
+mkPairE a b = TupE [a,b]
+
+mkPairP :: Pat -> Pat -> Pat
+mkPairP a b = TupP [a,b]
+
+data Nest a
+    = Leaf a
+    | Pair (Nest a) (Nest a)
+  deriving (Eq, Show, Functor)
+
+foldNest :: (a -> b) -> (b -> b -> b) -> Nest a -> b
+foldNest leaf pair = go
+  where
+    go (Leaf a) = leaf a
+    go (Pair a b) = pair (go a) (go b)
+
+toNest :: [a] -> Nest a
+toNest [a] = Leaf a
+toNest as  = Pair (toNest bs) (toNest cs)
+  where
+    (bs,cs) = splitAt ((length as + 1) `div` 2) as
+
+
+
+-- Make instances of the form
+--
+-- > instance Nestable (a,...,x)
+-- >   where
+-- >     type Nested (a,...,x) = (a ... x)  -- nested pairs
+-- >     nest   (a,...,x) = (a ... x)
+-- >     unnest (a ... x) = (a,...,x)
+mkNestableInstances
+    :: Int  -- ^ Max tuple width
+    -> DecsQ
+mkNestableInstances n = return $ map nestableInstance [2..n]
+  where
+    nestableInstance w = InstanceD
+        []
+        (AppT (ConT (mkName "Nestable")) tupT)
+        [ tySynInst (mkName "Nested") [tupT] (foldNest VarT mkPairT $ toNest vars)
+        , FunD (mkName "nest")
+            [ Clause
+                [TupP (map VarP vars)]
+                (NormalB (foldNest VarE mkPairE $ toNest vars))
+                []
+            ]
+        , FunD (mkName "unnest")
+            [ Clause
+                [foldNest VarP mkPairP $ toNest vars]
+                (NormalB (TupE (map VarE vars)))
+                []
+            ]
+        ]
+      where
+        vars = take w varSupply
+        tupT = mkTupT $ map VarT vars
+
diff --git a/src/Language/Syntactic/Decoration.hs b/src/Language/Syntactic/Decoration.hs
--- a/src/Language/Syntactic/Decoration.hs
+++ b/src/Language/Syntactic/Decoration.hs
@@ -23,6 +23,7 @@
 import Language.Syntactic.Syntax
 import Language.Syntactic.Traversal
 import Language.Syntactic.Interpretation
+import Language.Syntactic.Sugar
 
 
 
@@ -135,4 +136,46 @@
     mkTree :: [Tree NodeInfo] -> AST (sym :&: info) sig -> Tree NodeInfo
     mkTree args (f :$ a)              = mkTree (mkTree [] a : args) f
     mkTree args (Sym (expr :&: info)) = Node (NodeInfo (renderSym expr) (showInfo info)) args
+
+-- | Make a smart constructor of a symbol. 'smartSymDecor' has any type of the
+-- form:
+--
+-- > smartSymDecor :: (sub :<: AST (sup :&: info))
+-- >     => info x
+-- >     -> sub (a :-> b :-> ... :-> Full x)
+-- >     -> (ASTF sup a -> ASTF sup b -> ... -> ASTF sup x)
+smartSymDecor
+    :: ( Signature sig
+       , f              ~ SmartFun (sup :&: info) sig
+       , sig            ~ SmartSig f
+       , (sup :&: info) ~ SmartSym f
+       , sub :<: sup
+       )
+    => info (DenResult sig) -> sub sig -> f
+smartSymDecor d = smartSym' . (:&: d) . inj
+
+-- | \"Sugared\" symbol application
+--
+-- 'sugarSymDecor' has any type of the form:
+--
+-- > sugarSymDecor ::
+-- >     ( sub :<: AST (sup :&: info)
+-- >     , Syntactic a
+-- >     , Syntactic b
+-- >     , ...
+-- >     , Syntactic x
+-- >     , Domain a ~ Domain b ~ ... ~ Domain x
+-- >     ) => info (Internal x)
+-- >       -> sub (Internal a :-> Internal b :-> ... :-> Full (Internal x))
+-- >       -> (a -> b -> ... -> x)
+sugarSymDecor
+    :: ( Signature sig
+       , fi             ~ SmartFun (sup :&: info) sig
+       , sig            ~ SmartSig fi
+       , (sup :&: info) ~ SmartSym fi
+       , SyntacticN f fi
+       , sub :<: sup
+       )
+    => info (DenResult sig) -> sub sig -> f
+sugarSymDecor i = sugarN . smartSymDecor i
 
diff --git a/src/Language/Syntactic/Functional.hs b/src/Language/Syntactic/Functional.hs
--- a/src/Language/Syntactic/Functional.hs
+++ b/src/Language/Syntactic/Functional.hs
@@ -45,8 +45,6 @@
     , allVars
     , renameUnique'
     , renameUnique
-      -- * Substitution
-    , parSubst
       -- * Alpha-equivalence
     , AlphaEnv
     , alphaEq'
@@ -75,7 +73,6 @@
 import Control.Monad.Reader
 import Control.Monad.State
 import Data.Dynamic
-import qualified Data.Foldable as Foldable
 import Data.List (genericIndex)
 #if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0)
 #else
@@ -87,7 +84,6 @@
 import qualified Data.Set as Set
 import Data.Tree
 
-import Data.Constraint
 import Data.Hash (hashInt)
 
 import Language.Syntactic
@@ -217,13 +213,13 @@
 -- (ICFP 2013, <http://www.cse.chalmers.se/~emax/documents/axelsson2013using.pdf>).
 lam_template :: (Project Binding sym)
     => (Name -> sym (Full a))
-         -- ^ Variable constructor
-    -> (Name -> sym (b :-> Full (a -> b)))
+         -- ^ Variable symbol constructor
+    -> (Name -> ASTF sym b -> ASTF sym (a -> b))
          -- ^ Lambda constructor
     -> (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
-lam_template mkVar mkLam f = Sym (mkLam v) :$ body
+lam_template mkVar mkLam f = mkLam v body
   where
-    body = f (Sym (mkVar v))
+    body = f $ Sym $ mkVar v
     v    = succ $ maxLam body
 
 -- | Higher-order interface for variable binding
@@ -231,7 +227,7 @@
 -- This function is 'lamT_template' specialized to domains @sym@ satisfying
 -- @(`Binding` `:<:` sym)@.
 lam :: (Binding :<: sym) => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
-lam = lam_template (inj . Var) (inj . Lam)
+lam = lam_template (inj . Var) (\v a -> Sym (inj (Lam v)) :$ a)
 
 -- | Convert from a term with De Bruijn indexes to one with explicit names
 --
@@ -317,13 +313,13 @@
 -- (ICFP 2013, <http://www.cse.chalmers.se/~emax/documents/axelsson2013using.pdf>).
 lamT_template :: Project BindingT sym
     => (Name -> sym (Full a))
-         -- ^ Variable constructor
-    -> (Name -> sym (b :-> Full (a -> b)))
+         -- ^ Variable symbol constructor
+    -> (Name -> ASTF sym b -> ASTF sym (a -> b))
          -- ^ Lambda constructor
     -> (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
-lamT_template mkVarSym mkLamSym f = Sym (mkLamSym v) :$ body
+lamT_template mkVar mkLam f = mkLam v body
   where
-    body = f (Sym $ mkVarSym v)
+    body = f $ Sym $ mkVar v
     v    = succ $ maxLamT body
 
 -- | Higher-order interface for variable binding
@@ -332,7 +328,7 @@
 -- @(`BindingT` `:<:` sym)@.
 lamT :: (BindingT :<: sym, Typeable a) =>
     (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
-lamT = lamT_template (inj . VarT) (inj . LamT)
+lamT = lamT_template (inj . VarT) (\v a -> Sym (inj (LamT v)) :$ a)
 
 -- | Higher-order interface for variable binding
 --
@@ -340,7 +336,9 @@
 -- @(sym ~ `Typed` s, `BindingT` `:<:` s)@.
 lamTyped :: (sym ~ Typed s, BindingT :<: s, Typeable a, Typeable b) =>
     (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
-lamTyped = lamT_template (Typed . inj . VarT) (Typed . inj . LamT)
+lamTyped = lamT_template
+    (Typed . inj . VarT)
+    (\v a -> Sym (Typed (inj (LamT v))) :$ a)
 
 -- | Domains that \"might\" include variables and binders
 class BindingDomain sym
@@ -584,87 +582,6 @@
 -- when renaming bound variables.
 renameUnique :: BindingDomain sym => ASTF sym a -> ASTF sym a
 renameUnique = renameUnique' []
-
-
-
-----------------------------------------------------------------------------------------------------
--- * Substitution
-----------------------------------------------------------------------------------------------------
-
--- | Name environment
-type Aliases =
-    ( Set Name       -- Reserved names
-    , Map Name Name  -- Aliases; co-domain must not contain reserved names
-    , Name  -- Fresh name; must be greater than all reserved names and all names
-            -- in the co-domain of the alias map
-    )
-  -- Invariant: The second component of the pair is a name that is greater than
-  -- all names in the co-domain of the map.
-
--- | Set up an initial alias environment from a set of reserved names
-initAliases :: Set Name -> Aliases
-initAliases res = (res, Map.empty, next)
-  where
-    next = Set.findMax (Set.insert (-1) res) + 1
-
--- | Locally rename a binding
-rename :: Name -> Aliases -> (Name,Aliases)
-rename n al@(res,mp,next)
-    | Just n' <- Map.lookup n mp = (n',al)
-        -- This is a shadowing binding, so it's safe to reuse the name of the
-        -- shadowed binding (i.e. it will shadow the same binding after renaming
-        -- as before). This case is not strictly needed, but it allows more name
-        -- reuse.
-    | not (Set.member n res) =
-          (n, (Set.insert n res, Map.insert n n mp, max next (n+1)))
-        -- Here we reuse the name because it's not reserved. It may seem
-        -- pointless to map the name to itself, but this allows `parSubst` to
-        -- use the map to see whether a name is in scope.
-    | otherwise = (next, (Set.insert next res, Map.insert n next mp, next + 1))
-        -- Here we need a fresh name. By reserving the name we ensure that no
-        -- binding will be renamed to shadow the new name (unless it was already
-        -- a shadowing binding; see above).
-
--- | Lookup a name in an alias environment
-lookAlias :: Name -> Aliases -> Maybe Name
-lookAlias n (_,mp,_) = Map.lookup n mp
-
--- | Capture-avoiding parallel substitution
---
--- Uses the "rapier" method described in "Secrets of the Glasgow Haskell
--- Compiler inliner" (Peyton Jones and Marlow, JFP 2006) to rename variables
--- where there's risk for capturing.
-parSubst :: forall sym a . BindingDomain sym
-    => (forall a b . ASTF sym a -> ASTF sym b -> Maybe (Dict (a ~ b)))
-         -- ^ Type equality
-    -> [(Name, EF (AST sym))]  -- ^ Substitution
-    -> ASTF sym a
-    -> ASTF sym a
-parSubst teq subst a = go (initAliases reserved) a
-  where
-    reserved = Set.union
-        (freeVars a)  -- TODO Not needed?
-        (Foldable.fold [freeVars b | (_, EF b) <- subst])
-
-    go :: Aliases -> ASTF sym b -> ASTF sym b
-    go aliases var
-        | Just v  <- prVar var
-        = case lookAlias v aliases of
-            Just v' -> renameBind (\_ -> v') var
-            _ -> case lookup v subst of
-              Just (EF b) | Just Dict <- teq var b -> b
-              _ -> var  -- Free variable without a substitution
-    go aliases (lam :$ body)
-        | Just v <- prLam lam
-        , let (v',aliases') = rename v aliases
-        = renameBind (\_ -> v') lam :$ go aliases' body
-    go aliases a =
-        simpleMatch (\s as -> appArgs (Sym s) $ mapArgs (go aliases) as) a
-
-  -- It is safe to use the same `subst` throughout the traversal in `go`. This
-  -- is because `lookup v subst` is only done when `v` is known not to be in
-  -- scope (variables in scope must be in the alias map). So there's no risk of
-  -- replacing a bound variable.
 
 
 
diff --git a/src/Language/Syntactic/Functional/Sharing.hs b/src/Language/Syntactic/Functional/Sharing.hs
--- a/src/Language/Syntactic/Functional/Sharing.hs
+++ b/src/Language/Syntactic/Functional/Sharing.hs
@@ -147,8 +147,9 @@
 -- * Code motion
 --------------------------------------------------------------------------------
 
--- | Substituting a sub-expression. Assumes no variable capturing in the
--- expressions involved.
+-- | Substituting a sub-expression. Assumes that the free variables of the
+-- replacing expression do not occur as binders in the whole expression (so that
+-- there is no risk of capturing).
 substitute :: forall sym a b
     .  (Equality sym, BindingDomain sym)
     => CodeMotionInterface sym
@@ -156,15 +157,27 @@
     -> ASTF sym a  -- ^ Replacing sub-expression
     -> ASTF sym b  -- ^ Whole expression
     -> ASTF sym b
-substitute iface x y a
-    | Just y' <- castExprCM iface y a, alphaEq x a = y'
-    | otherwise = subst a
+substitute iface x y a = subst a
   where
-    subst :: AST sym c -> AST sym c
-    subst (s :$ a) = subst s :$ substitute iface x y a
-    subst a = a
+    fv = freeVars x
+
+    subst :: ASTF sym c -> ASTF sym c
+    subst a
+      | Just y' <- castExprCM iface y a, alphaEq x a = y'
+      | otherwise = subst' a
+
+    subst' :: AST sym c -> AST sym c
+    subst' a@(lam :$ body)
+      | Just v <- prLam lam
+      , Set.member v fv = a
+    subst' (s :$ a) = subst' s :$ subst a
+    subst' a = a
+
   -- Note: Since `codeMotion` only uses `substitute` to replace sub-expressions
-  -- with fresh variables, there's no risk of capturing.
+  -- with fresh variables, the assumption above is fulfilled. However, the
+  -- matching in `subst` needs to be aware of free variables, which is why the
+  -- substitution stops when reaching a lambda that binds a variable that is
+  -- free in the expression to be replaced.
 
 -- | Count the number of occurrences of a sub-expression
 count :: forall sym a b
diff --git a/src/Language/Syntactic/Functional/Tuple.hs b/src/Language/Syntactic/Functional/Tuple.hs
--- a/src/Language/Syntactic/Functional/Tuple.hs
+++ b/src/Language/Syntactic/Functional/Tuple.hs
@@ -2,38 +2,21 @@
 
 -- | Construction and elimination of tuples
 
-module Language.Syntactic.Functional.Tuple
-  ( module Language.Syntactic.Functional.Tuple
-    -- * Template Haskell
-  , eqPred
-  , classPred
-  , mkSelectClassPlusInstances
-  , deriveSyntacticForTuples
-  ) where
+module Language.Syntactic.Functional.Tuple where
 
 
 
 import Language.Syntactic
 import Language.Syntactic.TH
 import Language.Syntactic.Functional
-import Language.Syntactic.Functional.Tuple.TH
 
 
 
---------------------------------------------------------------------------------
--- * Generic tuple projection
---------------------------------------------------------------------------------
-
-mkSelectClassPlusInstances 15
-
-
-
---------------------------------------------------------------------------------
--- * Symbols
---------------------------------------------------------------------------------
-
--- | Construction and elimination of tuples
-mkTupleSym "Tuple" "Tup" "Sel" 15
+data Tuple a
+  where
+    Pair :: Tuple (a :-> b :-> Full (a,b))
+    Fst  :: Tuple ((a,b) :-> Full a)
+    Snd  :: Tuple ((a,b) :-> Full b)
 
 deriveSymbol    ''Tuple
 deriveEquality  ''Tuple
@@ -43,37 +26,9 @@
 
 instance Eval Tuple
   where
-    evalSym Tup2  = (,)
-    evalSym Tup3  = (,,)
-    evalSym Tup4  = (,,,)
-    evalSym Tup5  = (,,,,)
-    evalSym Tup6  = (,,,,,)
-    evalSym Tup7  = (,,,,,,)
-    evalSym Tup8  = (,,,,,,,)
-    evalSym Tup9  = (,,,,,,,,)
-    evalSym Tup10 = (,,,,,,,,,)
-    evalSym Tup11 = (,,,,,,,,,,)
-    evalSym Tup12 = (,,,,,,,,,,,)
-    evalSym Tup13 = (,,,,,,,,,,,,)
-    evalSym Tup14 = (,,,,,,,,,,,,,)
-    evalSym Tup15 = (,,,,,,,,,,,,,,)
-    evalSym Sel1  = select1
-    evalSym Sel2  = select2
-    evalSym Sel3  = select3
-    evalSym Sel4  = select4
-    evalSym Sel5  = select5
-    evalSym Sel6  = select6
-    evalSym Sel7  = select7
-    evalSym Sel8  = select8
-    evalSym Sel9  = select9
-    evalSym Sel10 = select10
-    evalSym Sel11 = select11
-    evalSym Sel12 = select12
-    evalSym Sel13 = select13
-    evalSym Sel14 = select14
-    evalSym Sel15 = select15
-  -- It would be possible to generate this instance, but the gain would be
-  -- small, and it's very hard to get it wrong anyway.
+    evalSym Pair = (,)
+    evalSym Fst  = fst
+    evalSym Snd  = snd
 
 instance EvalEnv Tuple env
 
diff --git a/src/Language/Syntactic/Functional/Tuple/TH.hs b/src/Language/Syntactic/Functional/Tuple/TH.hs
--- a/src/Language/Syntactic/Functional/Tuple/TH.hs
+++ b/src/Language/Syntactic/Functional/Tuple/TH.hs
@@ -1,155 +1,23 @@
 {-# LANGUAGE TemplateHaskell #-}
 
--- | Generate types, classes and instances for tuples
+-- | Generate 'Syntactic' instances for tuples
 
-module Language.Syntactic.Functional.Tuple.TH where
+module Language.Syntactic.Functional.Tuple.TH
+  ( deriveSyntacticForTuples
+  ) where
 
 
 
-import Data.Generics
 import Language.Haskell.TH
 
-import Language.Syntactic ((:->), Full, AST (..), (:<:), Syntactic (..))
-import Language.Syntactic.TH
-
-
-
---------------------------------------------------------------------------------
--- * Generic selection classes and instances
---------------------------------------------------------------------------------
-
-class SelectX tup
-  where
-    type SelX tup
-    selectX :: tup -> SelX tup
-  -- Declare the class to be able to quote instances of it
-
-classTemplate :: DecsQ
-classTemplate =
-  [d| class SelectX tup
-        where
-          type SelX tup
-          selectX :: tup -> SelX tup
-  |]
-
-instanceTemplate :: DecsQ
-instanceTemplate =
-  [d| instance SelectX tup
-        where
-          type SelX tup = Double
-          selectX tup = undefined
-            -- Use `Double` and `undefined` as placeholders
-  |]
-
-mkSelectClassPlusInstances
-    :: Int    -- ^ Max tuple width
-    -> DecsQ
-mkSelectClassPlusInstances n = do
-    [classTempl]    <- classTemplate
-    [instanceTempl] <- instanceTemplate
-    let classDecs = [everywhere (mkT (fixName s)) classTempl | s <- [1..n]]
-        instDecs =
-          [ everywhere
-              ( mkT (fixTupType s w)
-              . mkT (fixTupPat s w)
-              . mkT (fixTupExp s w)
-              . mkT (fixName s)
-              )
-              instanceTempl
-            | w <- [2..n]
-            , s <- [1..w]
-          ]
-    return (classDecs ++ instDecs)
-
--- | @"SelectX_0"@ -> @"Select33"@ (for @n=33@)
-fixName :: Int -> Name -> Name
-fixName s
-    = mkName
-    . concatMap (\c -> if c=='X' then show s else [c])
-    . takeWhile (/='_')
-    . nameBase
-
-fixTupType :: Int -> Int -> Type -> Type
-fixTupType s w ty
-    | VarT tup <- ty
-    , "tup" <- show tup = foldl1 AppT ((TupleT w) : tupVars)
-    | ConT doub <- ty
-    , show doub == "Double" = tupVars !! (s-1)
-    | otherwise = ty
-  where
-    tupVars = map VarT $ take w varSupply
-
-fixTupPat :: Int -> Int -> Pat -> Pat
-fixTupPat s w pat
-    | VarP tup <- pat
-    , "tup" <- show tup = TupP tupVars
-    | otherwise = pat
-  where
-    tupVars = map VarP $ take w varSupply
-
-fixTupExp :: Int -> Int -> Exp -> Exp
-fixTupExp s w ex
-    | VarE tup <- ex
-    , "tup" <- show tup = TupE tupVars
-    | VarE undef <- ex
-    , show undef == "undefined" = tupVars !! (s-1)
-    | otherwise = ex
-  where
-    tupVars = map VarE $ take w varSupply
-
-
-
---------------------------------------------------------------------------------
--- * Symbol type for tuple construction and elimination of tuples
---------------------------------------------------------------------------------
+import Data.NestTuple
+import Data.NestTuple.TH
 
-mkTupleSym
-    :: String  -- ^ Type name
-    -> String  -- ^ Base name for constructors
-    -> String  -- ^ Base name for selectors
-    -> Int     -- ^ Max tuple width
-    -> DecsQ
-mkTupleSym tyName tupName selName n = do
-    let tupCons =
-          [ ForallC
-              (map PlainTV (take w varSupply))
-              [eqPred (VarT (mkName "sig")) (signature w)]
-              (NormalC (mkName (tupName ++ show w)) [])
-            | w <- [2..n]
-          ]
-    let selCons =
-          [ ForallC
-              [PlainTV (mkName "tup")]
-              [ eqPred
-                  (VarT (mkName "sig"))
-                  ( foldl1 AppT
-                      [ ConT ''(:->)
-                      , VarT (mkName "tup")
-                      , AppT (ConT ''Full) (AppT (ConT (mkName ("Sel" ++ show s))) (VarT (mkName "tup")))
-                      ]
-                  )
-              , classPred (mkName ("Select" ++ show s)) ConT [VarT (mkName "tup")]
-              ]
-              (NormalC (mkName (selName ++ show s)) [])
-            | s <- [1..n]
-          ]
-    return [DataD [] (mkName tyName) [PlainTV (mkName "sig")] (tupCons ++ selCons) []]
-  where
-    signature :: Int -> Type
-    signature w = foldr
-        (\a res -> foldl1 AppT [ConT ''(:->), a, res])
-        (AppT (ConT ''Full)
-        (foldl AppT (TupleT w) vars))
-        vars
-      where
-        vars = map VarT $ take w varSupply
+import Language.Syntactic ((:<:), Syntactic (..))
+import Language.Syntactic.TH
 
 
 
---------------------------------------------------------------------------------
--- * 'Syntactic' instances for tuples
---------------------------------------------------------------------------------
-
 -- Make instances of the form
 --
 -- > instance
@@ -167,21 +35,25 @@
 -- >     , Domain a ~ Domain b
 -- >     , ...
 -- >     , Domain a ~ Domain x
+-- >     , extraConstraint
 -- >     ) =>
 -- >       Syntactic (a,...,x)
 -- >   where
 -- >     type Domain (a,...,x)   = Domain a
--- >     type Internal (a,...,x) = (Internal a, ..., Internal x)
--- >     desugar (a,...,x) = Sym (symInj TupN) :$ desugar a :$ ... :$ desugar x
--- >     sugar tup         = (sugar (Sym (symInj Sel1) :$ tup), ..., sugar (Sym (symInj SelN) :$ tup))
+-- >     type Internal (a,...,x) = (Internal a ... Internal x)  -- nested pairs
+-- >     desugar = desugar . nestTup  -- use pair instance
+-- >     sugar   = unnestTup . sugar  -- use pair instance
+--
+-- Instances will be generated for width 3 and upwards. The existence of an
+-- instance for pairs is assumed.
 deriveSyntacticForTuples
     :: (Type -> Cxt)   -- ^ @internalPred@ (see above)
     -> (Type -> Type)  -- ^ @mkDomain@ (see above)
-    -> (Exp -> Exp)    -- ^ Symbol injection
+    -> Cxt             -- ^ @extraConstraint@ (see above)
     -> Int             -- ^ Max tuple width
     -> DecsQ
-deriveSyntacticForTuples internalPred mkDomain symInj n = return $
-    map deriveSyntacticForTuple [2..n]
+deriveSyntacticForTuples internalPred mkDomain extraConstraint n = return $
+    map deriveSyntacticForTuple [3..n]
   where
     deriveSyntacticForTuple w = InstanceD
         ( concat
@@ -192,6 +64,7 @@
             , [eqPred domainA (AppT (ConT ''Domain) b)
                 | b <- tail varsT
               ]
+            , extraConstraint
             ]
         )
         (AppT (ConT ''Syntactic) tupT)
@@ -199,41 +72,20 @@
         , tySynInst ''Internal [tupT] tupTI
         , FunD 'desugar
             [ Clause
-                [TupP varsP]
-                (NormalB
-                  ( foldl
-                      (\s a -> foldl1 AppE [ConE '(:$), s, AppE (VarE 'desugar) a])
-                      (AppE (ConE 'Sym) (symInj (ConE (mkName ("Tup" ++ show w)))))
-                      varsE
-                  )
-                )
                 []
+                (NormalB (foldl AppE (VarE '(.)) $ map VarE [mkName "desugar", 'nest]))
+                []
             ]
         , FunD 'sugar
             [ Clause
-                [VarP (mkName "tup")]
-                (NormalB
-                  ( TupE
-                      [ AppE
-                          (VarE 'sugar)
-                          ( foldl1 AppE
-                              [ ConE '(:$)
-                              , AppE (ConE 'Sym) (symInj (ConE (mkName ("Sel" ++ show s))))
-                              , VarE (mkName "tup")
-                              ]
-                          )
-                        | s <- [1..w]
-                      ]
-                  )
-                )
                 []
+                (NormalB (foldl AppE (VarE '(.)) $ map VarE ['unnest, mkName "sugar"]))
+                []
             ]
         ]
       where
         varsT   = map VarT $ take w varSupply
         tupT    = foldl AppT (TupleT w) varsT
-        tupTI   = foldl AppT (TupleT w) $ map (AppT (ConT ''Internal)) varsT
+        tupTI   = foldNest id mkPairT $ toNest $ map (AppT (ConT ''Internal)) varsT
         domainA = AppT (ConT ''Domain) (VarT (mkName "a"))
-        varsP   = map VarP $ take w varSupply
-        varsE   = map VarE $ take w varSupply
 
diff --git a/src/Language/Syntactic/Sugar/Tuple.hs b/src/Language/Syntactic/Sugar/Tuple.hs
--- a/src/Language/Syntactic/Sugar/Tuple.hs
+++ b/src/Language/Syntactic/Sugar/Tuple.hs
@@ -7,13 +7,27 @@
 
 
 
-import Language.Haskell.TH
-
 import Language.Syntactic
 import Language.Syntactic.Functional.Tuple
 import Language.Syntactic.Functional.Tuple.TH
 
 
 
-deriveSyntacticForTuples (const []) id (AppE (VarE 'inj)) 15
+instance
+    ( Syntactic a
+    , Syntactic b
+    , Tuple :<: Domain a
+    , Domain a ~ Domain b
+    ) =>
+      Syntactic (a,b)
+  where
+    type Domain (a,b)   = Domain a
+    type Internal (a,b) = (Internal a, Internal b)
+    desugar (a,b) = inj Pair :$ desugar a :$ desugar b
+    sugar ab      = (sugar $ inj Fst :$ ab, sugar $ inj Snd :$ ab)
+
+-- `desugar` and `sugar` can be seen as applying the eta-rule for pairs.
+-- <https://mail.haskell.org/pipermail/haskell-cafe/2016-April/123639.html>
+
+deriveSyntacticForTuples (const []) id [] 15
 
diff --git a/src/Language/Syntactic/Sugar/TupleTyped.hs b/src/Language/Syntactic/Sugar/TupleTyped.hs
--- a/src/Language/Syntactic/Sugar/TupleTyped.hs
+++ b/src/Language/Syntactic/Sugar/TupleTyped.hs
@@ -16,14 +16,35 @@
 #endif
 
 import Language.Syntactic
+import Language.Syntactic.TH
 import Language.Syntactic.Functional.Tuple
+import Language.Syntactic.Functional.Tuple.TH
 
 
 
+instance
+    ( Syntactic a
+    , Syntactic b
+    , Typeable (Internal a)
+    , Typeable (Internal b)
+    , Tuple :<: sym
+    , Domain a ~ Typed sym
+    , Domain a ~ Domain b
+    ) =>
+      Syntactic (a,b)
+  where
+    type Domain (a,b)   = Domain a
+    type Internal (a,b) = (Internal a, Internal b)
+    desugar (a,b) = Sym (Typed $ inj Pair) :$ desugar a :$ desugar b
+    sugar ab      = (sugar $ Sym (Typed $ inj Fst) :$ ab, sugar $ Sym (Typed $ inj Snd) :$ ab)
+
+-- `desugar` and `sugar` can be seen as applying the eta-rule for pairs.
+-- <https://mail.haskell.org/pipermail/haskell-cafe/2016-April/123639.html>
+
 deriveSyntacticForTuples
     (return . classPred ''Typeable ConT . return)
     (AppT (ConT ''Typed))
-    (\s -> AppE (ConE 'Typed) (AppE (VarE 'inj) s))
+    []
 #if __GLASGOW_HASKELL__ < 708
     7
 #else
diff --git a/src/Language/Syntactic/Syntax.hs b/src/Language/Syntactic/Syntax.hs
--- a/src/Language/Syntactic/Syntax.hs
+++ b/src/Language/Syntactic/Syntax.hs
@@ -175,9 +175,9 @@
 type instance SmartSym (AST sym sig) = sym
 type instance SmartSym (a -> f)      = SmartSym f
 
--- | Make a smart constructor of a symbol. 'smartSym' has any type of the form:
+-- | Make a smart constructor of a symbol. 'smartSym'' has any type of the form:
 --
--- > smartSym
+-- > smartSym'
 -- >     :: sym (a :-> b :-> ... :-> Full x)
 -- >     -> (ASTF sym a -> ASTF sym b -> ... -> ASTF sym x)
 smartSym' :: forall sig f sym
diff --git a/src/Language/Syntactic/TH.hs b/src/Language/Syntactic/TH.hs
--- a/src/Language/Syntactic/TH.hs
+++ b/src/Language/Syntactic/TH.hs
@@ -178,9 +178,12 @@
 -- * Portability
 --------------------------------------------------------------------------------
 
+-- Using `__GLASGOW_HASKELL__` instead of `MIN_VERSION_template_haskell`,
+-- because the latter doesn't work when the package is compiled with `-f-th`.
+
 -- | Portable method for constructing a 'Pred' of the form @(t1 ~ t2)@
 eqPred :: Type -> Type -> Pred
-#if MIN_VERSION_template_haskell(2,10,0)
+#if __GLASGOW_HASKELL__ >= 710
 eqPred t1 t2 = foldl1 AppT [EqualityT,t1,t2]
 #else
 eqPred = EqualP
@@ -189,10 +192,10 @@
 -- | Portable method for constructing a 'Pred' of the form @SomeClass t1 t2 ...@
 classPred
     :: Name            -- ^ Class name
-    -> (Name -> Type)  -- ^ How to make a type for the class (typically 'ConT' or VarT)
+    -> (Name -> Type)  -- ^ How to make a type for the class (typically 'ConT' or 'VarT')
     -> [Type]          -- ^ Class arguments
     -> Pred
-#if MIN_VERSION_template_haskell(2,10,0)
+#if __GLASGOW_HASKELL__ >= 710
 classPred cl con = foldl AppT (con cl)
 #else
 classPred cl con = ClassP cl
@@ -200,7 +203,7 @@
 
 -- | Portable method for constructing a type synonym instances
 tySynInst :: Name -> [Type] -> Type -> Dec
-#if MIN_VERSION_template_haskell(2,9,0)
+#if __GLASGOW_HASKELL__ >= 708
 tySynInst t as rhs = TySynInstD t (TySynEqn as rhs)
 #else
 tySynInst = TySynInstD
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        3.5
+Version:        3.6
 Synopsis:       Generic representation and manipulation of abstract syntax
 Description:    The library provides a generic representation of type-indexed abstract syntax trees
                 (or indexed data types in general). It also permits the definition of open syntax
@@ -68,13 +68,13 @@
     Language.Syntactic.Sugar.MonadTyped
   if flag(th)
     exposed-modules:
+      Data.NestTuple
+      Data.NestTuple.TH
       Language.Syntactic.TH
       Language.Syntactic.Functional.Tuple
+      Language.Syntactic.Functional.Tuple.TH
       Language.Syntactic.Sugar.Tuple
       Language.Syntactic.Sugar.TupleTyped
-
-    other-modules:
-      Language.Syntactic.Functional.Tuple.TH
 
   build-depends:
     base >= 4 && < 5,
diff --git a/tests/AlgorithmTests.hs b/tests/AlgorithmTests.hs
--- a/tests/AlgorithmTests.hs
+++ b/tests/AlgorithmTests.hs
@@ -228,10 +228,12 @@
 prop_codeMotion_vars (a :: Exp Int) = freeVars a == freeVars (cm a)
 prop_codeMotion_eval (a :: Exp Int) = evalAny a == evalAny (cm a)
 
-counter = app2 (lamm 1 (lamm 2 (varr 1))) (app1 (lamm 1 (int 0)) (app2 (lamm 0 (lamm 0 (varr 1))) (int 0) (int 0))) (varr 2)
+prop_bug1 = prop_codeMotion_eval exp
+  where
+    exp = add
+        (app2 (lamm 0 (lamm 0 (varr 1))) (int 0) (int 0))
+        (app2 (lamm 1 (lamm 2 (varr 1))) (int 0) (int 0))
 
 
 tests = $testGroupGenerator
-
-main = $defaultMainGenerator
 
diff --git a/tests/gold/fib.txt b/tests/gold/fib.txt
--- a/tests/gold/fib.txt
+++ b/tests/gold/fib.txt
@@ -1,17 +1,17 @@
 Lam v3
- └╴Sel1
+ └╴Fst
     └╴ForLoop
        ├╴v3
-       ├╴Tup2
+       ├╴Pair
        │  ├╴0
        │  └╴1
        └╴Lam v2
           └╴Lam v1
-             └╴Tup2
-                ├╴Sel2
+             └╴Pair
+                ├╴Snd
                 │  └╴v1
                 └╴(+)
-                   ├╴Sel1
+                   ├╴Fst
                    │  └╴v1
-                   └╴Sel2
+                   └╴Snd
                       └╴v1
diff --git a/tests/gold/spanVec.txt b/tests/gold/spanVec.txt
--- a/tests/gold/spanVec.txt
+++ b/tests/gold/spanVec.txt
@@ -3,7 +3,7 @@
     ├╴ForLoop
     │  ├╴arrLen
     │  │  └╴v3
-    │  ├╴Tup2
+    │  ├╴Pair
     │  │  ├╴arrIx
     │  │  │  ├╴v3
     │  │  │  └╴0
@@ -12,21 +12,21 @@
     │  │     └╴0
     │  └╴Lam v2
     │     └╴Lam v1
-    │        └╴Tup2
+    │        └╴Pair
     │           ├╴min
     │           │  ├╴arrIx
     │           │  │  ├╴v3
     │           │  │  └╴v2
-    │           │  └╴Sel1
+    │           │  └╴Fst
     │           │     └╴v1
     │           └╴max
     │              ├╴arrIx
     │              │  ├╴v3
     │              │  └╴v2
-    │              └╴Sel2
+    │              └╴Snd
     │                 └╴v1
     └╴(-)
-       ├╴Sel2
+       ├╴Snd
        │  └╴v4
-       └╴Sel1
+       └╴Fst
           └╴v4