diff --git a/examples/Monad.hs b/examples/Monad.hs
--- a/examples/Monad.hs
+++ b/examples/Monad.hs
@@ -19,7 +19,7 @@
 
 import Language.Syntactic
 import Language.Syntactic.Functional
-import Language.Syntactic.Sugar.MonadT ()
+import Language.Syntactic.Sugar.MonadTyped ()
 
 import NanoFeldspar (Type, Arithmetic (..))
 
@@ -32,28 +32,28 @@
 type IO' a = Remon Dom IO (Exp a)
 
 getDigit :: IO' Int
-getDigit = sugarSymT $ Construct "getDigit" get
+getDigit = sugarSymTyped $ Construct "getDigit" get
   where
     get = do
         c <- getChar
         if isDigit c then return (fromEnum c - fromEnum '0') else get
 
 putDigit :: Exp Int -> IO' ()
-putDigit = sugarSymT $ Construct "putDigit" print
+putDigit = sugarSymTyped $ Construct "putDigit" print
 
 iter :: Typeable a => Exp Int -> IO' a -> IO' ()
-iter = sugarSymT $ Construct "iter" replicateM_
+iter = sugarSymTyped $ Construct "iter" replicateM_
 
 -- | Literal
 value :: (Show a, Typeable a) => a -> Exp a
-value a = sugarSymT $ Construct (show a) a
+value a = sugarSymTyped $ Construct (show a) a
 
 instance (Num a, Type a) => Num (Exp a)
   where
     fromInteger = value . fromInteger
-    (+)         = sugarSymT Add
-    (-)         = sugarSymT Sub
-    (*)         = sugarSymT Mul
+    (+)         = sugarSymTyped Add
+    (-)         = sugarSymTyped Sub
+    (*)         = sugarSymTyped Mul
 
 ex1 :: Exp Int -> IO' ()
 ex1 n = iter n $ do
diff --git a/examples/NanoFeldspar.hs b/examples/NanoFeldspar.hs
--- a/examples/NanoFeldspar.hs
+++ b/examples/NanoFeldspar.hs
@@ -27,8 +27,8 @@
 import Language.Syntactic.Functional
 import Language.Syntactic.Functional.Sharing
 import Language.Syntactic.Functional.Tuple
-import Language.Syntactic.Sugar.BindingT ()
-import Language.Syntactic.Sugar.TupleT ()
+import Language.Syntactic.Sugar.BindingTyped ()
+import Language.Syntactic.Sugar.TupleTyped ()
 import Language.Syntactic.TH
 
 
@@ -146,7 +146,7 @@
 
 -- | Interface for controlling code motion
 cmInterface :: CodeMotionInterface FeldDomain
-cmInterface = defaultInterfaceT sharable (const True)
+cmInterface = defaultInterface VarT LamT sharable (const True)
   where
     sharable :: ASTF FeldDomain a -> ASTF FeldDomain b -> Bool
     sharable (Sym _) _ = False
@@ -221,36 +221,36 @@
 instance (Type a, Num a) => Num (Data a)
   where
     fromInteger = value . fromInteger
-    (+)         = sugarSymT Add
-    (-)         = sugarSymT Sub
-    (*)         = sugarSymT Mul
+    (+)         = sugarSymTyped Add
+    (-)         = sugarSymTyped Sub
+    (*)         = sugarSymTyped Mul
 
 -- | Explicit sharing
 share :: (Syntax a, Syntax b) => a -> (a -> b) -> b
-share = sugarSymT Let
+share = sugarSymTyped Let
 
 -- | Parallel array
 parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a]
-parallel = sugarSymT Parallel
+parallel = sugarSymTyped Parallel
 
 -- | For loop
 forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st
-forLoop = sugarSymT ForLoop
+forLoop = sugarSymTyped ForLoop
 
 -- | Conditional expression
 (?) :: forall a . Syntax a => Data Bool -> (a,a) -> a
-c ? (t,f) = sugarSymT sym c t f
+c ? (t,f) = sugarSymTyped sym c t f
   where
     sym :: Construct (Bool :-> Internal a :-> Internal a :-> Full (Internal a))
     sym = Construct "cond" (\c t f -> if c then t else f)
 
 -- | Get the length of an array
 arrLen :: Type a => Data [a] -> Data Length
-arrLen = sugarSymT $ Construct "arrLen" Prelude.length
+arrLen = sugarSymTyped $ Construct "arrLen" Prelude.length
 
 -- | Index into an array
 arrIx :: Type a => Data [a] -> Data Index -> Data a
-arrIx = sugarSymT $ Construct "arrIx" eval
+arrIx = sugarSymTyped $ Construct "arrIx" eval
   where
     eval as i
         | i >= len || i < 0 = error "arrIx: index out of bounds"
@@ -259,16 +259,16 @@
         len = Prelude.length as
 
 not :: Data Bool -> Data Bool
-not = sugarSymT $ Construct "not" Prelude.not
+not = sugarSymTyped $ Construct "not" Prelude.not
 
 (==) :: Type a => Data a -> Data a -> Data Bool
-(==) = sugarSymT $ Construct "(==)" (Prelude.==)
+(==) = sugarSymTyped $ Construct "(==)" (Prelude.==)
 
 max :: Type a => Data a -> Data a -> Data a
-max = sugarSymT $ Construct "max" Prelude.max
+max = sugarSymTyped $ Construct "max" Prelude.max
 
 min :: Type a => Data a -> Data a -> Data a
-min = sugarSymT $ Construct "min" Prelude.min
+min = sugarSymTyped $ Construct "min" Prelude.min
 
 
 
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
@@ -1,3 +1,15 @@
+{-# LANGUAGE CPP #-}
+
+#ifndef MIN_VERSION_GLASGOW_HASKELL
+#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0
+#endif
+  -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10
+
+#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0)
+#else
+{-# LANGUAGE OverlappingInstances #-}
+#endif
+
 -- | Construct for decorating symbols or expressions with additional information
 
 module Language.Syntactic.Decoration where
@@ -40,7 +52,7 @@
   where
     rnf1 (s :&: i) = rnf1 s `seq` rnf1 i `seq` ()
 
-instance Project sub sup => Project sub (sup :&: info)
+instance {-# OVERLAPPING #-} Project sub sup => Project sub (sup :&: info)
   where
     prj = prj . decorExpr
 
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
@@ -22,20 +22,24 @@
 module Language.Syntactic.Functional
     ( -- * Syntactic constructs
       Name (..)
+    , Literal (..)
     , Construct (..)
     , Binding (..)
     , maxLam
+    , lam_template
     , lam
     , fromDeBruijn
     , BindingT (..)
     , maxLamT
+    , lamT_template
     , lamT
+    , lamTyped
     , BindingDomain (..)
     , Let (..)
     , MONAD (..)
     , Remon (..)
     , desugarMonad
-    , desugarMonadT
+    , desugarMonadTyped
       -- * Free and bound variables
     , freeVars
     , allVars
@@ -75,7 +79,8 @@
 import qualified Data.Set as Set
 import Data.Tree
 
-import Data.Hash (hashInt)
+import Data.Hash (Hashable, hashInt)
+import qualified Data.Hash as Hash
 
 import Language.Syntactic
 
@@ -85,6 +90,22 @@
 -- * Syntactic constructs
 ----------------------------------------------------------------------------------------------------
 
+-- | Literal
+data Literal sig
+  where
+    Literal :: Show a => a -> Literal (Full a)
+
+instance Symbol Literal
+  where
+    symSig (Literal _) = signature
+
+instance Render Literal
+  where
+    renderSym (Literal a) = show a
+
+instance Equality Literal
+instance StringTree Literal
+
 -- | Generic N-ary syntactic construct
 --
 -- 'Construct' gives a quick way to introduce a syntactic construct by giving its name and semantic
@@ -168,12 +189,12 @@
 --
 -- \[1\] Ordered binders means that the names of 'Lam' nodes are decreasing along every path from
 -- the root.
-maxLam :: (Binding :<: s) => AST s a -> Name
+maxLam :: (Project Binding s) => AST s a -> Name
 maxLam (Sym lam :$ _) | Just (Lam v) <- prj lam = v
 maxLam (s :$ a) = maxLam s `Prelude.max` maxLam a
 maxLam _ = 0
 
--- | Higher-order interface for variable binding
+-- | Higher-order interface for variable binding for domains based on 'Binding'
 --
 -- Assumptions:
 --
@@ -186,12 +207,24 @@
 --
 -- See \"Using Circular Programs for Higher-Order Syntax\"
 -- (ICFP 2013, <http://www.cse.chalmers.se/~emax/documents/axelsson2013using.pdf>).
-lam :: (Binding :<: s) => (ASTF s a -> ASTF s b) -> ASTF s (a -> b)
-lam f = smartSym (Lam v) body
+lam_template :: (Project Binding sym)
+    => (Name -> sym (Full a))
+         -- ^ Variable constructor
+    -> (Name -> sym (b :-> Full (a -> b)))
+         -- ^ Lambda constructor
+    -> (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
+lam_template mkVar mkLam f = Sym (mkLam v) :$ body
   where
-    body = f (smartSym (Var v))
+    body = f (Sym (mkVar v))
     v    = succ $ maxLam body
 
+-- | Higher-order interface for variable binding
+--
+-- 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)
+
 -- | Convert from a term with De Bruijn indexes to one with explicit names
 --
 -- In the argument term, variable 'Name's are treated as De Bruijn indexes, and lambda 'Name's are
@@ -261,7 +294,7 @@
 maxLamT (s :$ a) = maxLamT s `Prelude.max` maxLamT a
 maxLamT _ = 0
 
--- | Higher-order interface for typed variable binding
+-- | Higher-order interface for variable binding
 --
 -- Assumptions:
 --
@@ -274,18 +307,33 @@
 --
 -- See \"Using Circular Programs for Higher-Order Syntax\"
 -- (ICFP 2013, <http://www.cse.chalmers.se/~emax/documents/axelsson2013using.pdf>).
-lamT :: forall sym symT a b
-    .  ( BindingT :<: sym
-       , symT ~ Typed sym
-       , Typeable a
-       , Typeable b
-       )
-    => (ASTF symT a -> ASTF symT b) -> ASTF symT (a -> b)
-lamT f = smartSymT (LamT v) body
+lamT_template :: Project BindingT sym
+    => (Name -> sym (Full a))
+         -- ^ Variable constructor
+    -> (Name -> sym (b :-> Full (a -> b)))
+         -- ^ Lambda constructor
+    -> (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
+lamT_template mkVarSym mkLamSym f = Sym (mkLamSym v) :$ body
   where
-    body = f (smartSymT (VarT v))
+    body = f (Sym $ mkVarSym v)
     v    = succ $ maxLamT body
 
+-- | Higher-order interface for variable binding
+--
+-- This function is 'lamT_template' specialized to domains @sym@ satisfying
+-- @(`BindingT` `:<:` sym)@.
+lamT :: (BindingT :<: sym, Typeable a) =>
+    (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
+lamT = lamT_template (inj . VarT) (inj . LamT)
+
+-- | Higher-order interface for variable binding
+--
+-- This function is 'lamT_template' specialized to domains @sym@ satisfying
+-- @(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)
+
 -- | Domains that \"might\" include variables and binders
 class BindingDomain sym
   where
@@ -348,8 +396,6 @@
 
 instance Symbol Let where symSig Let = signature
 instance Render Let where renderSym Let = "letBind"
-instance Eval Let where evalSym Let = flip ($)
-instance EvalEnv Let env
 
 instance Equality Let
   where
@@ -428,14 +474,14 @@
 desugarMonad = flip runCont (sugarSym Return) . unRemon
 
 -- | One-layer desugaring of monadic actions
-desugarMonadT
-    :: ( MONAD m :<: sym
-       , symT ~ Typed sym
+desugarMonadTyped
+    :: ( MONAD m :<: s
+       , sym ~ Typed s
        , Typeable a
        , TYPEABLE m
        )
-    => Remon symT m (ASTF symT a) -> ASTF symT (m a)
-desugarMonadT = flip runCont (sugarSymT Return) . unRemon
+    => Remon sym m (ASTF sym a) -> ASTF sym (m a)
+desugarMonadTyped = flip runCont (sugarSymTyped Return) . unRemon
 
 
 
@@ -537,10 +583,18 @@
   where
     evalSym = evalSym . decorExpr
 
+instance Eval Literal
+  where
+    evalSym (Literal a) = a
+
 instance Eval Construct
   where
     evalSym (Construct _ d) = d
 
+instance Eval Let
+  where
+    evalSym Let = flip ($)
+
 instance Monad m => Eval (MONAD m)
   where
     evalSym Return = return
@@ -588,10 +642,10 @@
 -- | Evaluation
 class EvalEnv sym env
   where
+    compileSym :: proxy env -> sym sig -> DenotationM (Reader env) sig
+
     default compileSym :: (Symbol sym, Eval sym) =>
         proxy env -> sym sig -> DenotationM (Reader env) sig
-
-    compileSym :: proxy env -> sym sig -> DenotationM (Reader env) sig
     compileSym p s = compileSymDefault (symSig s) p s
 
 -- | Simple implementation of `compileSym` from a 'Denotation'
@@ -616,11 +670,11 @@
   where
     compileSym p = compileSym p . decorExpr
 
+instance EvalEnv Literal env
+
 instance EvalEnv Construct env
-  where
-    compileSym _ s@(Construct _ d) = liftDenotationM signature p s d
-      where
-        p = Proxy :: Proxy (Reader env)
+
+instance EvalEnv Let env
 
 instance Monad m => EvalEnv (MONAD m) env
 
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
@@ -11,7 +11,7 @@
       InjDict (..)
     , CodeMotionInterface (..)
     , defaultInterface
-    , defaultInterfaceT
+    , defaultInterfaceDecor
       -- * Code motion
     , codeMotion
     ) where
@@ -22,7 +22,10 @@
 import Data.Maybe (isNothing)
 import Data.Set (Set)
 import qualified Data.Set as Set
+import Data.Typeable
 
+import Data.Constraint (Dict (..))
+
 import Language.Syntactic
 import Language.Syntactic.Functional
 
@@ -61,17 +64,22 @@
 
 -- | Default 'CodeMotionInterface' for domains of the form
 -- @`Typed` (... `:+:` `Binding` `:+:` ...)@.
-defaultInterface :: forall sym symT
-    .  ( Binding :<: sym
+defaultInterface :: forall binding sym symT
+    .  ( binding :<: sym
        , Let     :<: sym
        , symT ~ Typed sym
        )
-    => (forall a b . ASTF symT a -> ASTF symT b -> Bool)
+    => (forall a .   Typeable a => Name -> binding (Full a))
+         -- ^ Variable constructor (e.g. 'Var' or 'VarT')
+    -> (forall a b . Typeable a => Name -> binding (b :-> Full (a -> b)))
+         -- ^ Lambda constructor (e.g. 'Lam' or 'LamT')
+    -> (forall a b . ASTF symT a -> ASTF symT b -> Bool)
          -- ^ Can the expression represented by the first argument be shared in
          -- the second argument?
-    -> (forall a . ASTF symT a -> Bool)  -- ^ Can we hoist over this expression?
+    -> (forall a . ASTF symT a -> Bool)
+         -- ^ Can we hoist over this expression?
     -> CodeMotionInterface symT
-defaultInterface sharable hoistOver = Interface {..}
+defaultInterface var lam sharable hoistOver = Interface {..}
   where
     mkInjDict :: ASTF symT a -> ASTF symT b -> Maybe (InjDict symT a b)
     mkInjDict a b | not (sharable a b) = Nothing
@@ -79,8 +87,8 @@
         simpleMatch
           (\(Typed _) _ -> simpleMatch
             (\(Typed _) _ ->
-              let injVariable = Typed . inj . Var
-                  injLambda   = Typed . inj . Lam
+              let injVariable = Typed . inj . var
+                  injLambda   = Typed . inj . lam
                   injLet      = Typed $ inj Let
               in  Just InjDict {..}
             ) b
@@ -89,33 +97,51 @@
     castExprCM = castExpr
 
 -- | Default 'CodeMotionInterface' for domains of the form
--- @`Typed` (... `:+:` `BindingT` `:+:` ...)@.
-defaultInterfaceT :: forall sym symT
-    .  ( BindingT :<: sym
-       , Let      :<: sym
-       , symT ~ Typed sym
+-- @(... `:&:` info)@, where @info@ can be used to witness type casting
+defaultInterfaceDecor :: forall binding sym symI info
+    .  ( binding :<: sym
+       , Let     :<: sym
+       , symI ~ (sym :&: info)
        )
-    => (forall a b . ASTF symT a -> ASTF symT b -> Bool)
+    => (forall a b . info a -> info b -> Maybe (Dict (a ~ b)))
+         -- ^ Construct a type equality witness
+    -> (forall a b . info a -> info b -> info (a -> b))
+         -- ^ Construct info for a function, given info for the argument and the
+         -- result
+    -> (forall a . info a -> Name -> binding (Full a))
+         -- ^ Variable constructor
+    -> (forall a b . info a -> info b -> Name -> binding (b :-> Full (a -> b)))
+         -- ^ Lambda constructor
+    -> (forall a b . ASTF symI a -> ASTF symI b -> Bool)
          -- ^ Can the expression represented by the first argument be shared in
          -- the second argument?
-    -> (forall a . ASTF symT a -> Bool)  -- ^ Can we hoist over this expression?
-    -> CodeMotionInterface symT
-defaultInterfaceT sharable hoistOver = Interface {..}
+    -> (forall a . ASTF symI a -> Bool)
+         -- ^ Can we hoist over this expression?
+    -> CodeMotionInterface symI
+defaultInterfaceDecor kaka mkFunInfo var lam sharable hoistOver = Interface {..}
   where
-    mkInjDict :: ASTF symT a -> ASTF symT b -> Maybe (InjDict symT a b)
+    mkInjDict :: ASTF symI a -> ASTF symI b -> Maybe (InjDict symI a b)
     mkInjDict a b | not (sharable a b) = Nothing
     mkInjDict a b =
         simpleMatch
-          (\(Typed _) _ -> simpleMatch
-            (\(Typed _) _ ->
-              let injVariable = Typed . inj . VarT
-                  injLambda   = Typed . inj . LamT
-                  injLet      = Typed $ inj Let
+          (\(_ :&: aInfo) _ -> simpleMatch
+            (\(_ :&: bInfo) _ ->
+              let injVariable v = inj (var aInfo v) :&: aInfo
+                  injLambda   v = inj (lam aInfo bInfo v) :&: mkFunInfo aInfo bInfo
+                  injLet        = inj Let :&: bInfo
               in  Just InjDict {..}
             ) b
           ) a
 
-    castExprCM = castExpr
+    castExprCM :: ASTF symI a -> ASTF symI b -> Maybe (ASTF symI b)
+    castExprCM a b =
+        simpleMatch
+          (\(_ :&: aInfo) _ -> simpleMatch
+            (\(_ :&: bInfo) _ -> case kaka aInfo bInfo of
+              Just Dict -> Just a
+              _ -> Nothing
+            ) b
+          ) a
 
 
 
@@ -255,5 +281,5 @@
     -> ASTF sym a
 codeMotion iface a = flip evalState maxVar $ codeMotionM iface a
   where
-    maxVar = succ $ Set.findMax $ allVars a
+    maxVar = succ $ Set.findMax $ Set.insert 0 $ allVars a
 
diff --git a/src/Language/Syntactic/Sugar.hs b/src/Language/Syntactic/Sugar.hs
--- a/src/Language/Syntactic/Sugar.hs
+++ b/src/Language/Syntactic/Sugar.hs
@@ -115,9 +115,9 @@
 
 -- | \"Sugared\" symbol application
 --
--- 'sugarSym' has any type of the form:
+-- 'sugarSymTyped' has any type of the form:
 --
--- > sugarSym ::
+-- > sugarSymTyped ::
 -- >     ( sub :<: AST (Typed sup)
 -- >     , Syntactic a
 -- >     , Syntactic b
@@ -127,7 +127,7 @@
 -- >     , Typeable (Internal x)
 -- >     ) => sub (Internal a :-> Internal b :-> ... :-> Full (Internal x))
 -- >       -> (a -> b -> ... -> x)
-sugarSymT
+sugarSymTyped
     :: ( Signature sig
        , fi        ~ SmartFun (Typed sup) sig
        , sig       ~ SmartSig fi
@@ -137,5 +137,5 @@
        , Typeable (DenResult sig)
        )
     => sub sig -> f
-sugarSymT = sugarN . smartSymT
+sugarSymTyped = sugarN . smartSymTyped
 
diff --git a/src/Language/Syntactic/Sugar/Binding.hs b/src/Language/Syntactic/Sugar/Binding.hs
--- a/src/Language/Syntactic/Sugar/Binding.hs
+++ b/src/Language/Syntactic/Sugar/Binding.hs
@@ -1,9 +1,6 @@
 {-# LANGUAGE UndecidableInstances #-}
 
--- | 'Syntactic' instance for functions
---
--- This module is based on having 'Binding' in the domain. For 'BindingT' import
--- module "Language.Syntactic.Sugar.BindingT" instead.
+-- | 'Syntactic' instance for functions for domains based on 'Binding'
 
 module Language.Syntactic.Sugar.Binding where
 
diff --git a/src/Language/Syntactic/Sugar/BindingT.hs b/src/Language/Syntactic/Sugar/BindingT.hs
deleted file mode 100644
--- a/src/Language/Syntactic/Sugar/BindingT.hs
+++ /dev/null
@@ -1,32 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
--- | 'Syntactic' instance for functions
---
--- This module is based on having 'BindingT' in the domain. For 'Binding' import
--- module "Language.Syntactic.Sugar.Binding" instead.
-
-module Language.Syntactic.Sugar.BindingT where
-
-
-
-import Data.Typeable
-
-import Language.Syntactic
-import Language.Syntactic.Functional
-
-
-
-instance
-    ( Syntactic a, Domain a ~ Typed dom
-    , Syntactic b, Domain b ~ Typed dom
-    , BindingT :<: dom
-    , Typeable (Internal a)
-    , Typeable (Internal b)
-    ) =>
-      Syntactic (a -> b)
-  where
-    type Domain (a -> b)   = Domain a
-    type Internal (a -> b) = Internal a -> Internal b
-    desugar f = lamT (desugar . f . sugar)
-    sugar     = error "sugar not implemented for (a -> b)"
-
diff --git a/src/Language/Syntactic/Sugar/BindingTyped.hs b/src/Language/Syntactic/Sugar/BindingTyped.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Syntactic/Sugar/BindingTyped.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | 'Syntactic' instance for functions for domains based on 'Typed' and
+-- 'BindingT'
+
+module Language.Syntactic.Sugar.BindingTyped where
+
+
+
+import Data.Typeable
+
+import Language.Syntactic
+import Language.Syntactic.Functional
+
+
+
+instance
+    ( sym ~ Typed s
+    , Syntactic a, Domain a ~ sym
+    , Syntactic b, Domain b ~ sym
+    , BindingT :<: s
+    , Typeable (Internal a)
+    , Typeable (Internal b)
+    ) =>
+      Syntactic (a -> b)
+  where
+    type Domain (a -> b)   = Domain a
+    type Internal (a -> b) = Internal a -> Internal b
+    desugar f = lamTyped (desugar . f . sugar)
+    sugar     = error "sugar not implemented for (a -> b)"
+
diff --git a/src/Language/Syntactic/Sugar/Monad.hs b/src/Language/Syntactic/Sugar/Monad.hs
--- a/src/Language/Syntactic/Sugar/Monad.hs
+++ b/src/Language/Syntactic/Sugar/Monad.hs
@@ -7,7 +7,7 @@
 #define TYPEABLE Typeable
 #endif
 
--- | 'Syntactic' instance for 'Remon' using 'Binding' to handle variable binding
+-- | 'Syntactic' instance for 'Remon' for domains based on 'Binding'
 
 module Language.Syntactic.Sugar.Monad where
 
diff --git a/src/Language/Syntactic/Sugar/MonadT.hs b/src/Language/Syntactic/Sugar/MonadT.hs
deleted file mode 100644
--- a/src/Language/Syntactic/Sugar/MonadT.hs
+++ /dev/null
@@ -1,51 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-#if __GLASGOW_HASKELL__ < 708
-#define TYPEABLE Typeable1
-#else
-#define TYPEABLE Typeable
-#endif
-
--- | 'Syntactic' instance for 'Remon' using 'BindingT' to handle variable binding
-
-module Language.Syntactic.Sugar.MonadT where
-
-
-
-import Control.Monad.Cont
-import Data.Typeable
-
-import Language.Syntactic
-import Language.Syntactic.Functional
-import Language.Syntactic.Sugar.BindingT ()
-
-
-
--- | One-layer sugaring of monadic actions
-sugarMonad
-    :: ( BindingT :<: sym
-       , MONAD m  :<: sym
-       , symT ~ Typed sym
-       , TYPEABLE m
-       , Typeable a
-       )
-    => ASTF symT (m a) -> Remon symT m (ASTF symT a)
-sugarMonad ma = Remon $ cont $ sugarSymT Bind ma
-
-instance
-    ( Syntactic a
-    , Domain a ~ symT
-    , symT ~ Typed sym
-    , BindingT :<: sym
-    , MONAD m  :<: sym
-    , TYPEABLE m
-    , Typeable (Internal a)
-    ) =>
-      Syntactic (Remon symT m a)
-  where
-    type Domain (Remon symT m a)   = symT
-    type Internal (Remon symT m a) = m (Internal a)
-    desugar = desugarMonadT . fmap desugar
-    sugar   = fmap sugar   . sugarMonad
-
diff --git a/src/Language/Syntactic/Sugar/MonadTyped.hs b/src/Language/Syntactic/Sugar/MonadTyped.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Syntactic/Sugar/MonadTyped.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if __GLASGOW_HASKELL__ < 708
+#define TYPEABLE Typeable1
+#else
+#define TYPEABLE Typeable
+#endif
+
+-- | 'Syntactic' instance for 'Remon' for domains based on 'Typed' and
+-- 'BindingT'
+
+module Language.Syntactic.Sugar.MonadTyped where
+
+
+
+import Control.Monad.Cont
+import Data.Typeable
+
+import Language.Syntactic
+import Language.Syntactic.Functional
+import Language.Syntactic.Sugar.BindingTyped ()
+
+
+
+-- | One-layer sugaring of monadic actions
+sugarMonad
+    :: ( sym ~ Typed s
+       , BindingT :<: s
+       , MONAD m  :<: s
+       , TYPEABLE m
+       , Typeable a
+       )
+    => ASTF sym (m a) -> Remon sym m (ASTF sym a)
+sugarMonad ma = Remon $ cont $ sugarSymTyped Bind ma
+
+instance
+    ( sym ~ Typed s
+    , Syntactic a, Domain a ~ sym
+    , BindingT :<: s
+    , MONAD m  :<: s
+    , TYPEABLE m
+    , Typeable (Internal a)
+    ) =>
+      Syntactic (Remon sym m a)
+  where
+    type Domain (Remon sym m a)   = sym
+    type Internal (Remon sym m a) = m (Internal a)
+    desugar = desugarMonadTyped . fmap desugar
+    sugar   = fmap sugar   . sugarMonad
+
diff --git a/src/Language/Syntactic/Sugar/TupleT.hs b/src/Language/Syntactic/Sugar/TupleT.hs
deleted file mode 100644
--- a/src/Language/Syntactic/Sugar/TupleT.hs
+++ /dev/null
@@ -1,72 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
--- | 'Syntactic' instances for tuples and 'Typed' symbol domains
-
-module Language.Syntactic.Sugar.TupleT where
-
-
-
-import Data.Typeable
-
-import Language.Syntactic
-import Language.Syntactic.Functional.Tuple
-
-
-
-instance
-    ( Syntactic a
-    , Syntactic b
-    , Typeable (Internal a)
-    , Typeable (Internal b)
-    , Domain a ~ Typed sym
-    , Domain a ~ Domain b
-    , Tuple :<: sym
-    ) =>
-      Syntactic (a,b)
-  where
-    type Domain (a,b)   = Domain a
-    type Internal (a,b) = (Internal a, Internal b)
-    desugar (a,b) = sugarSymT Tup2 a b
-    sugar ab      = (sugarSymT Sel1 ab, sugarSymT Sel2 ab)
-
-instance
-    ( Syntactic a
-    , Syntactic b
-    , Syntactic c
-    , Typeable (Internal a)
-    , Typeable (Internal b)
-    , Typeable (Internal c)
-    , Domain a ~ Typed sym
-    , Domain a ~ Domain b
-    , Domain a ~ Domain c
-    , Tuple :<: sym
-    ) =>
-      Syntactic (a,b,c)
-  where
-    type Domain (a,b,c)   = Domain a
-    type Internal (a,b,c) = (Internal a, Internal b, Internal c)
-    desugar (a,b,c) = sugarSymT Tup3 a b c
-    sugar abc       = (sugarSymT Sel1 abc, sugarSymT Sel2 abc, sugarSymT Sel3 abc)
-
-instance
-    ( Syntactic a
-    , Syntactic b
-    , Syntactic c
-    , Syntactic d
-    , Typeable (Internal a)
-    , Typeable (Internal b)
-    , Typeable (Internal c)
-    , Typeable (Internal d)
-    , Domain a ~ Typed sym
-    , Domain a ~ Domain b
-    , Domain a ~ Domain c
-    , Domain a ~ Domain d
-    , Tuple :<: sym
-    ) =>
-      Syntactic (a,b,c,d)
-  where
-    type Domain (a,b,c,d)   = Domain a
-    type Internal (a,b,c,d) = (Internal a, Internal b, Internal c, Internal d)
-    desugar (a,b,c,d) = sugarSymT Tup4 a b c d
-    sugar abcd        = (sugarSymT Sel1 abcd, sugarSymT Sel2 abcd, sugarSymT Sel3 abcd, sugarSymT Sel4 abcd)
-
diff --git a/src/Language/Syntactic/Sugar/TupleTyped.hs b/src/Language/Syntactic/Sugar/TupleTyped.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Syntactic/Sugar/TupleTyped.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | 'Syntactic' instances for tuples and 'Typed' symbol domains
+
+module Language.Syntactic.Sugar.TupleTyped where
+
+
+
+import Data.Typeable
+
+import Language.Syntactic
+import Language.Syntactic.Functional.Tuple
+
+
+
+instance
+    ( Syntactic a
+    , Syntactic b
+    , Typeable (Internal a)
+    , Typeable (Internal b)
+    , Domain a ~ Typed sym
+    , Domain a ~ Domain b
+    , Tuple :<: sym
+    ) =>
+      Syntactic (a,b)
+  where
+    type Domain (a,b)   = Domain a
+    type Internal (a,b) = (Internal a, Internal b)
+    desugar (a,b) = sugarSymTyped Tup2 a b
+    sugar ab      = (sugarSymTyped Sel1 ab, sugarSymTyped Sel2 ab)
+
+instance
+    ( Syntactic a
+    , Syntactic b
+    , Syntactic c
+    , Typeable (Internal a)
+    , Typeable (Internal b)
+    , Typeable (Internal c)
+    , Domain a ~ Typed sym
+    , Domain a ~ Domain b
+    , Domain a ~ Domain c
+    , Tuple :<: sym
+    ) =>
+      Syntactic (a,b,c)
+  where
+    type Domain (a,b,c)   = Domain a
+    type Internal (a,b,c) = (Internal a, Internal b, Internal c)
+    desugar (a,b,c) = sugarSymTyped Tup3 a b c
+    sugar abc       = (sugarSymTyped Sel1 abc, sugarSymTyped Sel2 abc, sugarSymTyped Sel3 abc)
+
+instance
+    ( Syntactic a
+    , Syntactic b
+    , Syntactic c
+    , Syntactic d
+    , Typeable (Internal a)
+    , Typeable (Internal b)
+    , Typeable (Internal c)
+    , Typeable (Internal d)
+    , Domain a ~ Typed sym
+    , Domain a ~ Domain b
+    , Domain a ~ Domain c
+    , Domain a ~ Domain d
+    , Tuple :<: sym
+    ) =>
+      Syntactic (a,b,c,d)
+  where
+    type Domain (a,b,c,d)   = Domain a
+    type Internal (a,b,c,d) = (Internal a, Internal b, Internal c, Internal d)
+    desugar (a,b,c,d) = sugarSymTyped Tup4 a b c d
+    sugar abcd        = (sugarSymTyped Sel1 abcd, sugarSymTyped Sel2 abcd, sugarSymTyped Sel3 abcd, sugarSymTyped Sel4 abcd)
+
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
@@ -37,7 +37,7 @@
     , Project (..)
     , (:<:) (..)
     , smartSym
-    , smartSymT
+    , smartSymTyped
     , Empty
       -- * Existential quantification
     , E (..)
@@ -287,12 +287,13 @@
     => sub sig -> f
 smartSym = smartSym' . inj
 
--- | Make a smart constructor of a symbol. 'smartSymT' has any type of the form:
+-- | Make a smart constructor of a symbol. 'smartSymTyped' has any type of the
+-- form:
 --
--- > smartSym :: (sub :<: AST (Typed sup), Typeable x)
+-- > smartSymTyped :: (sub :<: AST (Typed sup), Typeable x)
 -- >     => sub (a :-> b :-> ... :-> Full x)
 -- >     -> (ASTF sup a -> ASTF sup b -> ... -> ASTF sup x)
-smartSymT
+smartSymTyped
     :: ( Signature sig
        , f         ~ SmartFun (Typed sup) sig
        , sig       ~ SmartSig f
@@ -301,7 +302,7 @@
        , Typeable (DenResult sig)
        )
     => sub sig -> f
-smartSymT = smartSym' . Typed . inj
+smartSymTyped = smartSym' . Typed . inj
 
 -- | Empty symbol type
 --
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        3.1
+Version:        3.2
 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
@@ -64,17 +64,18 @@
     Language.Syntactic.Functional.Tuple
     Language.Syntactic.Functional.WellScoped
     Language.Syntactic.Sugar.Binding
-    Language.Syntactic.Sugar.BindingT
+    Language.Syntactic.Sugar.BindingTyped
     Language.Syntactic.Sugar.Monad
-    Language.Syntactic.Sugar.MonadT
+    Language.Syntactic.Sugar.MonadTyped
     Language.Syntactic.Sugar.Tuple
-    Language.Syntactic.Sugar.TupleT
+    Language.Syntactic.Sugar.TupleTyped
   if flag(th)
     exposed-modules:
       Language.Syntactic.TH
 
   build-depends:
     base >= 4 && < 5,
+    constraints,
     containers,
     data-hash,
     deepseq,