diff --git a/Examples/NanoFeldspar/Core.hs b/Examples/NanoFeldspar/Core.hs
--- a/Examples/NanoFeldspar/Core.hs
+++ b/Examples/NanoFeldspar/Core.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- | A minimal Feldspar core language implementation. The intention of this
@@ -12,10 +13,10 @@
 --
 -- A more realistic implementation would use custom contexts to restrict the
 -- types at which constructors operate. Currently, all general features (such as
--- 'Literal' and 'Tuple') use a 'Poly' context, which means that the types are
--- not restricted. A real implementation would also probably use custom types
--- for primitive functions, since the 'Sym' feature is quite unsafe (uses only
--- a 'String' to distinguish between functions).
+-- 'Literal' and 'Tuple') use a 'SimpleCtx' context, which means that the types
+-- are quite unrestricted. A real implementation would also probably use custom
+-- types for primitive functions, since the 'Sym' feature is quite unsafe (uses
+-- only a 'String' to distinguish between functions).
 
 module NanoFeldspar.Core where
 
@@ -32,8 +33,6 @@
 import Language.Syntactic.Features.Tuple
 import Language.Syntactic.Features.Binding
 import Language.Syntactic.Features.Binding.HigherOrder
-import Language.Syntactic.Sharing.Graph
-import Language.Syntactic.Sharing.ReifyHO
 
 
 
@@ -56,17 +55,21 @@
 
 data Parallel a
   where
-    Parallel :: Parallel (Length :-> (Index -> a) :-> Full [a])
+    Parallel :: Type a => Parallel (Length :-> (Index -> a) :-> Full [a])
 
+instance WitnessCons Parallel
+  where
+    witnessCons Parallel = ConsWit
+
 instance IsSymbol Parallel
   where
     toSym Parallel = Sym "parallel" parallel
       where
         parallel len ixf = map ixf [0 .. len-1]
 
-instance ExprEq Parallel where exprEq = exprEqFunc; exprHash = exprHashFunc
-instance Render Parallel where renderPart = renderPartFunc
-instance Eval   Parallel where evaluate   = evaluateFunc
+instance ExprEq Parallel where exprEq = exprEqSym; exprHash = exprHashSym
+instance Render Parallel where renderPart = renderPartSym
+instance Eval   Parallel where evaluate   = evaluateSym
 instance ToTree Parallel
 
 
@@ -77,17 +80,22 @@
 
 data ForLoop a
   where
-    ForLoop :: ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)
+    ForLoop :: Type st =>
+        ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)
 
+instance WitnessCons ForLoop
+  where
+    witnessCons ForLoop = ConsWit
+
 instance IsSymbol ForLoop
   where
     toSym ForLoop = Sym "forLoop" forLoop
       where
         forLoop len init body = foldl (flip body) init [0 .. len-1]
 
-instance ExprEq ForLoop where exprEq = exprEqFunc; exprHash = exprHashFunc
-instance Render ForLoop where renderPart = renderPartFunc
-instance Eval   ForLoop where evaluate   = evaluateFunc
+instance ExprEq ForLoop where exprEq = exprEqSym; exprHash = exprHashSym
+instance Render ForLoop where renderPart = renderPartSym
+instance Eval   ForLoop where evaluate   = evaluateSym
 instance ToTree ForLoop
 
 
@@ -98,18 +106,19 @@
 
 -- | The Feldspar domain
 type FeldDomain
-    =   Literal Poly
-    :+: Sym
-    :+: Condition Poly
-    :+: Tuple Poly
-    :+: Select Poly
-    :+: Let Poly Poly
+    =   Literal SimpleCtx
+    :+: Sym SimpleCtx
+    :+: Condition SimpleCtx
+    :+: Tuple SimpleCtx
+    :+: Select SimpleCtx
+    :+: Let SimpleCtx SimpleCtx
     :+: Parallel
     :+: ForLoop
 
-data Data a = Type a => Data { unData :: HOAST Poly FeldDomain (Full a) }
+data Data a = Type a => Data { unData :: HOAST SimpleCtx FeldDomain (Full a) }
 
-type FeldDomainAll = HOLambda Poly FeldDomain :+: Variable Poly :+: FeldDomain
+type FeldDomainAll =
+    HOLambda SimpleCtx FeldDomain :+: Variable SimpleCtx :+: FeldDomain
 
 -- | Declaring 'Data' as syntactic sugar
 instance Type a => Syntactic (Data a) FeldDomainAll
@@ -140,42 +149,16 @@
 --------------------------------------------------------------------------------
 
 -- | Print the expression
-printFeld :: Reifiable Poly a FeldDomain internal => a -> IO ()
-printFeld = printExpr . reify
+printFeld :: Reifiable SimpleCtx a FeldDomain internal => a -> IO ()
+printFeld = printExpr . reifyCtx simpleCtx
 
 -- | Draw the syntax tree
-drawFeld :: Reifiable Poly a FeldDomain internal => a -> IO ()
-drawFeld = drawAST . reify
-
--- | A predicate deciding which constructs can be shared. Variables and literals
--- are not shared.
-canShare :: HOASTF Poly FeldDomain a -> Maybe (Witness' Poly a)
-canShare (prjVariable poly -> Just _) = Nothing
-canShare (prjLiteral poly  -> Just _) = Nothing
-canShare _                            = Just Witness'
-
--- | Draw the syntax graph after common sub-expression elimination
-drawFeldCSE :: Reifiable Poly a FeldDomain internal => a -> IO ()
-drawFeldCSE a = do
-    (g,_) <- reifyGraph canShare a
-    drawASG
-      $ reindexNodesFrom0
-      $ inlineSingle
-      $ cse
-      $ g
-
--- | Draw the syntax graph after observing sharing
-drawFeldObs :: Reifiable Poly a FeldDomain internal => a -> IO ()
-drawFeldObs a = do
-    (g,_) <- reifyGraph canShare a
-    drawASG
-      $ reindexNodesFrom0
-      $ inlineSingle
-      $ g
+drawFeld :: Reifiable SimpleCtx a FeldDomain internal => a -> IO ()
+drawFeld = drawAST . reifyCtx simpleCtx
 
 -- | Evaluation
-eval :: Reifiable Poly a FeldDomain internal => a -> NAryEval internal
-eval = evalLambda . reify
+eval :: Reifiable SimpleCtx a FeldDomain internal => a -> NAryEval internal
+eval = evalLambda . reifyCtx simpleCtx
 
 
 
@@ -185,7 +168,7 @@
 
 -- | Literal
 value :: Syntax a => Internal a -> a
-value = sugar . lit
+value = sugar . litCtx simpleCtx
 
 -- | For types containing some kind of \"thunk\", this function can be used to
 -- force computation
@@ -194,26 +177,31 @@
 
 -- | Share a value using let binding
 share :: (Syntax a, Syntax b) => a -> (a -> b) -> b
-share a f = sugar $ letBind (desugar a) (desugarN f)
+share a f = sugar $ letBindCtx simpleCtx (desugar a) (desugarN f)
 
 -- | Alpha equivalence
 instance Eq (Data a)
   where
-    Data a == Data b = alphaEq poly (reify a) (reify b)
+    Data a == Data b =
+        alphaEq simpleCtx (reifyCtx simpleCtx a) (reifyCtx simpleCtx b)
 
 instance Show (Data a)
   where
-    show (Data a) = render $ reify a
+    show (Data a) = render $ reifyCtx simpleCtx a
 
 instance (Type a, Num a) => Num (Data a)
   where
     fromInteger = value . fromInteger
-    abs         = sugarN $ sym1 "abs" abs
-    signum      = sugarN $ sym1 "signum" signum
-    (+)         = sugarN $ sym2 "(+)" (+)
-    (-)         = sugarN $ sym2 "(-)" (-)
-    (*)         = sugarN $ sym2 "(*)" (*)
+    abs         = sugarN $ sym1 simpleCtx "abs" abs
+    signum      = sugarN $ sym1 simpleCtx "signum" signum
+    (+)         = sugarN $ sym2 simpleCtx "(+)" (+)
+    (-)         = sugarN $ sym2 simpleCtx "(-)" (-)
+    (*)         = sugarN $ sym2 simpleCtx "(*)" (*)
 
+(?) :: Syntax a => Data Bool -> (a,a) -> a
+cond ? (t,e) = sugar $
+    conditionCtx simpleCtx (desugar cond) (desugar t) (desugar e)
+
 -- | Parallel array
 parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a]
 parallel len ixf
@@ -231,11 +219,11 @@
     :$: lambdaN (desugarN body)
 
 arrLength :: Type a => Data [a] -> Data Length
-arrLength = sugarN $ sym1 "arrLength" Prelude.length
+arrLength = sugarN $ sym1 simpleCtx "arrLength" Prelude.length
 
 -- | Array indexing
 getIx :: Type a => Data [a] -> Data Index -> Data a
-getIx = sugarN $ sym2 "getIx" eval
+getIx = sugarN $ sym2 simpleCtx "getIx" eval
   where
     eval as i
         | i >= len || i < 0 = error "getIx: index out of bounds"
@@ -244,8 +232,8 @@
         len = Prelude.length as
 
 max :: Type a => Data a -> Data a -> Data a
-max = sugarN $ sym2 "max" Prelude.max
+max = sugarN $ sym2 simpleCtx "max" Prelude.max
 
 min :: Type a => Data a -> Data a -> Data a
-min = sugarN $ sym2 "min" Prelude.min
+min = sugarN $ sym2 simpleCtx "min" Prelude.min
 
diff --git a/Examples/NanoFeldspar/Extra.hs b/Examples/NanoFeldspar/Extra.hs
new file mode 100644
--- /dev/null
+++ b/Examples/NanoFeldspar/Extra.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module NanoFeldspar.Extra where
+
+
+
+import Language.Syntactic
+import Language.Syntactic.Features.Symbol
+import Language.Syntactic.Features.Literal
+import Language.Syntactic.Features.Binding
+import Language.Syntactic.Features.Binding.HigherOrder
+import Language.Syntactic.Features.Binding.PartialEval
+import Language.Syntactic.Sharing.Graph
+import Language.Syntactic.Sharing.ReifyHO
+
+import NanoFeldspar.Core
+
+
+
+-- | A predicate deciding which constructs can be shared. Variables and literals
+-- are not shared.
+mkSimpleWit :: (Sym SimpleCtx :<: dom, Parallel :<: dom, ForLoop :<: dom) =>
+    ASTF dom a -> Maybe (Witness' SimpleCtx a)
+mkSimpleWit ((project -> Just Parallel) :$: _ :$: _)      = Just Witness'
+mkSimpleWit ((project -> Just ForLoop) :$: _ :$: _ :$: _) = Just Witness'
+mkSimpleWit expr = witnessSatSym simpleCtx expr
+
+
+
+--------------------------------------------------------------------------------
+-- * Graph reification
+--------------------------------------------------------------------------------
+
+-- | Draw the syntax graph after common sub-expression elimination
+drawFeldCSE :: Reifiable SimpleCtx a FeldDomain internal => a -> IO ()
+drawFeldCSE a = do
+    (g,_) <- reifyGraph mkSimpleWit a
+    drawASG
+      $ reindexNodesFrom0
+      $ inlineSingle
+      $ cse
+      $ g
+
+-- | Draw the syntax graph after observing sharing
+drawFeldObs :: Reifiable SimpleCtx a FeldDomain internal => a -> IO ()
+drawFeldObs a = do
+    (g,_) <- reifyGraph mkSimpleWit a
+    drawASG
+      $ reindexNodesFrom0
+      $ inlineSingle
+      $ g
+
+--------------------------------------------------------------------------------
+-- * Partial evaluation
+--------------------------------------------------------------------------------
+
+instance (ForLoop :<: dom, PartialEval dom ctx dom) =>
+    PartialEval ForLoop ctx dom
+  where
+    partEvalFeat = partEvalFeatDefault
+
+instance (Parallel :<: dom, PartialEval dom ctx dom) =>
+    PartialEval Parallel ctx dom
+  where
+    partEvalFeat = partEvalFeatDefault
+
+
+
+constFold :: forall a
+    .  ASTF (Lambda SimpleCtx :+: Variable SimpleCtx :+: FeldDomain) a
+    -> a
+    -> ASTF (Lambda SimpleCtx :+: Variable SimpleCtx :+: FeldDomain) a
+constFold expr a = case mkSimpleWit expr of
+    Just Witness' -> case witness :: Witness SimpleCtx a of
+        SimpleWit -> litCtx simpleCtx a
+    _ -> expr
+
+drawFeldPart :: Reifiable SimpleCtx a FeldDomain internal => a -> IO ()
+drawFeldPart = drawAST . partialEval simpleCtx constFold . reifyCtx simpleCtx
+
diff --git a/Examples/NanoFeldspar/Test.hs b/Examples/NanoFeldspar/Test.hs
--- a/Examples/NanoFeldspar/Test.hs
+++ b/Examples/NanoFeldspar/Test.hs
@@ -1,8 +1,9 @@
 import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith)
 
-import Language.Syntactic.Features.TupleSyntacticPoly
+import Language.Syntactic.Features.TupleSyntacticSimple
 
 import NanoFeldspar.Core
+import NanoFeldspar.Extra
 import NanoFeldspar.Vector
 
 
@@ -69,9 +70,9 @@
 
 test7_3 = drawFeldObs prog7
   -- Draws a graph with some duplication. The 'forLoop' introduced by 'sum' is
-  -- not shared, because 'sum as' is repeated twice in source code of 'prog7'.
-  -- But the 'parallel' introduced by 'force' is shared, because 'force' only
-  -- appears once.
+  -- not shared, because 'sum as' is repeated twice in source code. But the
+  -- 'parallel' introduced by 'force' is shared, because 'force' only appears
+  -- once.
 
 -- Note that we're still missing a way to rebuild an expression with let
 -- bindings from the graph. This is ongoing work.
diff --git a/Examples/NanoFeldspar/Vector.hs b/Examples/NanoFeldspar/Vector.hs
--- a/Examples/NanoFeldspar/Vector.hs
+++ b/Examples/NanoFeldspar/Vector.hs
@@ -1,8 +1,7 @@
-{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
 
 -- | A simple vector library for NanoFeldspar. The intention of this module is
 -- to demonstrate how to add language features without extending the underlying
@@ -23,7 +22,6 @@
 import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith)
 
 import Language.Syntactic
-import Language.Syntactic.Features.Binding.HigherOrder
 
 import NanoFeldspar.Core
 
diff --git a/Language/Syntactic.hs b/Language/Syntactic.hs
--- a/Language/Syntactic.hs
+++ b/Language/Syntactic.hs
@@ -5,17 +5,17 @@
 
 module Language.Syntactic
     ( module Language.Syntactic.Syntax
-    , module Language.Syntactic.Analysis.Equality
-    , module Language.Syntactic.Analysis.Render
-    , module Language.Syntactic.Analysis.Evaluation
+    , module Language.Syntactic.Interpretation.Equality
+    , module Language.Syntactic.Interpretation.Render
+    , module Language.Syntactic.Interpretation.Evaluation
     , module Language.Syntactic.Features.Annotate
     ) where
 
 
 
 import Language.Syntactic.Syntax
-import Language.Syntactic.Analysis.Equality
-import Language.Syntactic.Analysis.Render
-import Language.Syntactic.Analysis.Evaluation
+import Language.Syntactic.Interpretation.Equality
+import Language.Syntactic.Interpretation.Render
+import Language.Syntactic.Interpretation.Evaluation
 import Language.Syntactic.Features.Annotate
 
diff --git a/Language/Syntactic/Analysis/Equality.hs b/Language/Syntactic/Analysis/Equality.hs
deleted file mode 100644
--- a/Language/Syntactic/Analysis/Equality.hs
+++ /dev/null
@@ -1,52 +0,0 @@
-module Language.Syntactic.Analysis.Equality where
-
-
-
-import Data.Hash
-
-import Language.Syntactic.Syntax
-
-
-
--- | Equality for expressions. The difference between 'Eq' and 'ExprEq' is that
--- 'ExprEq' allows comparison of expressions with different value types. It is
--- assumed that when the types differ, the expressions also differ. The reason
--- for allowing comparison of different types is that this is convenient when
--- the types are existentially quantified.
-class ExprEq expr
-  where
-    exprEq :: expr a -> expr b -> Bool
-
-    -- | Computes a 'Hash' for an expression. Expressions that are equal
-    -- according to 'exprEq' must result in the same hash:
-    --
-    -- @`exprEq` a b  ==>  `exprHash` a == `exprHash` b@
-    exprHash :: expr a -> Hash
-
-
-instance ExprEq dom => ExprEq (AST dom)
-  where
-    exprEq (Symbol a)  (Symbol b)  = exprEq a b
-    exprEq (f1 :$: a1) (f2 :$: a2) = exprEq f1 f2 && exprEq a1 a2
-    exprEq _ _ = False
-
-    exprHash (Symbol a) = hashInt 0 `combine` exprHash a
-    exprHash (f :$: a)  = hashInt 1 `combine` exprHash f `combine` exprHash a
-
-instance ExprEq dom => Eq (AST dom a)
-  where
-    (==) = exprEq
-
-instance (ExprEq expr1, ExprEq expr2) => ExprEq (expr1 :+: expr2)
-  where
-    exprEq (InjectL a) (InjectL b) = exprEq a b
-    exprEq (InjectR a) (InjectR b) = exprEq a b
-    exprEq _ _ = False
-
-    exprHash (InjectL a) = hashInt 0 `combine` exprHash a
-    exprHash (InjectR a) = hashInt 1 `combine` exprHash a
-
-instance (ExprEq expr1, ExprEq expr2) => Eq ((expr1 :+: expr2) a)
-  where
-    (==) = exprEq
-
diff --git a/Language/Syntactic/Analysis/Evaluation.hs b/Language/Syntactic/Analysis/Evaluation.hs
deleted file mode 100644
--- a/Language/Syntactic/Analysis/Evaluation.hs
+++ /dev/null
@@ -1,26 +0,0 @@
-module Language.Syntactic.Analysis.Evaluation where
-
-
-
-import Language.Syntactic.Syntax
-
-
-
-class Eval expr
-  where
-    -- | Evaluation of expressions
-    evaluate :: expr a -> a
-
-instance Eval dom => Eval (AST dom)
-  where
-    evaluate (Symbol a) = evaluate a
-    evaluate (f :$: a)  = evaluate f $: result (evaluate a)
-
-instance (Eval expr1, Eval expr2) => Eval (expr1 :+: expr2)
-  where
-    evaluate (InjectL a) = evaluate a
-    evaluate (InjectR a) = evaluate a
-
-evalFull :: Eval dom => ASTF dom a -> a
-evalFull = result . evaluate
-
diff --git a/Language/Syntactic/Analysis/Render.hs b/Language/Syntactic/Analysis/Render.hs
deleted file mode 100644
--- a/Language/Syntactic/Analysis/Render.hs
+++ /dev/null
@@ -1,83 +0,0 @@
-module Language.Syntactic.Analysis.Render
-    ( Render (..)
-    , printExpr
-    , ToTree (..)
-    , showAST
-    , drawAST
-    ) where
-
-
-
-import Data.Tree
-
-import Language.Syntactic.Syntax
-
-
-
--- | Render an expression as concrete syntax. A complete instance must define
--- either of the methods 'render' and 'renderPart'.
-class Render expr
-  where
-    -- | Render an expression as a 'String'
-    render :: expr a -> String
-    render = renderPart []
-
-    -- | Render a partially applied constructor given a list of rendered missing
-    -- arguments
-    renderPart :: [String] -> expr a -> String
-    renderPart []   a = render a
-    renderPart args a = "(" ++ unwords (render a : args) ++ ")"
-
-instance Render dom => Render (AST dom)
-  where
-    renderPart args (Symbol a) = renderPart args a
-    renderPart args (f :$: a)  = renderPart (render a : args) f
-
-instance Render dom => Show (AST dom a)
-  where
-    show = render
-
-instance (Render expr1, Render expr2) => Render (expr1 :+: expr2)
-  where
-    renderPart args (InjectL a) = renderPart args a
-    renderPart args (InjectR a) = renderPart args a
-
-instance (Render expr1, Render expr2) => Show ((expr1 :+: expr2) a)
-  where
-    show = render
-
--- | Print an expression
-printExpr :: Render expr => expr a -> IO ()
-printExpr = putStrLn . render
-
-
-
-class Render expr => ToTree expr
-  where
-    -- | Convert a partially applied constructor to a syntax tree given a list
-    -- of rendered missing arguments
-    toTreePart :: [Tree String] -> expr a -> Tree String
-    toTreePart args a = Node (render a) args
-
-instance ToTree dom => ToTree (AST dom)
-  where
-    toTreePart args (Symbol a) = toTreePart args a
-    toTreePart args (f :$: a)  = toTreePart (toTree a : args) f
-
-instance (ToTree expr1, ToTree expr2) => ToTree (expr1 :+: expr2)
-  where
-    toTreePart args (InjectL a) = toTreePart args a
-    toTreePart args (InjectR a) = toTreePart args a
-
--- | Convert an expression to a syntax tree
-toTree :: ToTree expr => expr a -> Tree String
-toTree = toTreePart []
-
--- | Show syntax tree using ASCII art
-showAST :: ToTree dom => AST dom a -> String
-showAST = drawTree . toTree
-
--- | Print syntax tree using ASCII art
-drawAST :: ToTree dom => AST dom a -> IO ()
-drawAST = putStrLn . showAST
-
diff --git a/Language/Syntactic/Features/Annotate.hs b/Language/Syntactic/Features/Annotate.hs
--- a/Language/Syntactic/Features/Annotate.hs
+++ b/Language/Syntactic/Features/Annotate.hs
@@ -4,10 +4,12 @@
 
 
 
+import Data.Tree
+
 import Language.Syntactic.Syntax
-import Language.Syntactic.Analysis.Equality
-import Language.Syntactic.Analysis.Render
-import Language.Syntactic.Analysis.Evaluation
+import Language.Syntactic.Interpretation.Equality
+import Language.Syntactic.Interpretation.Render
+import Language.Syntactic.Interpretation.Evaluation
 
 
 
@@ -75,4 +77,23 @@
 collectInfo :: (forall a . info a -> b) -> AST (Ann info dom) a -> [b]
 collectInfo coll (Symbol (Ann info _)) = [coll info]
 collectInfo coll (f :$: a) = collectInfo coll f ++ collectInfo coll a
+
+-- | Rendering of annotated syntax trees
+toTreeAnn :: forall info dom a . (Render info, ToTree dom) =>
+    ASTF (Ann info dom) a -> Tree String
+toTreeAnn a = mkTree [] a
+  where
+    mkTree :: [Tree String] -> AST (Ann info dom) b -> Tree String
+    mkTree args (Symbol (Ann info expr)) = Node infoStr [toTreePart args expr]
+      where
+        infoStr = "<<" ++ render info ++ ">>"
+    mkTree args (f :$: a) = mkTree (mkTree [] a : args) f
+
+-- | Show an annotated syntax tree using ASCII art
+showANN :: (Render info, ToTree dom) => ASTF (Ann info dom) a -> String
+showANN = drawTree . toTreeAnn
+
+-- | Print an annotated syntax tree using ASCII art
+drawANN :: (Render info, ToTree dom) => ASTF (Ann info dom) a -> IO ()
+drawANN = putStrLn . showANN
 
diff --git a/Language/Syntactic/Features/Binding.hs b/Language/Syntactic/Features/Binding.hs
--- a/Language/Syntactic/Features/Binding.hs
+++ b/Language/Syntactic/Features/Binding.hs
@@ -113,84 +113,7 @@
 prjLambda _ = project
 
 
--- | Alpha equivalence in an environment of variable equivalences. The supplied
--- equivalence function gets called when the argument expressions are not both
--- 'Variable's, both 'Lambda's or both ':$:'.
-alphaEqM :: (Lambda ctx :<: dom, Variable ctx :<: dom)
-    => Proxy ctx
-    -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool)
-    -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool)
 
--- TODO This function is not ideal, since the type says nothing about which
---      cases have been handled when calling 'eq'.
-
-alphaEqM ctx eq
-    ((prjLambda ctx -> Just (Lambda v1)) :$: a1)
-    ((prjLambda ctx -> Just (Lambda v2)) :$: a2) =
-        local ((v1,v2):) $ alphaEqM ctx eq a1 a2
-
-alphaEqM ctx eq
-    (prjVariable ctx -> Just (Variable v1))
-    (prjVariable ctx -> Just (Variable v2)) = do
-        env <- ask
-        case lookup v1 env of
-          Nothing  -> return (v1==v2)   -- Free variables
-          Just v2' -> return (v2==v2')
-
-alphaEqM ctx eq (f1 :$: a1) (f2 :$: a2) = do
-    e <- alphaEqM ctx eq f1 f2
-    if e then alphaEqM ctx eq a1 a2 else return False
-
-alphaEqM _ eq a b = eq a b
-
-
-
--- | Alpha-equivalence on lambda expressions. Free variables are taken to be
--- equivalent if they have the same identifier.
-alphaEq :: (Lambda ctx :<: dom, Variable ctx :<: dom, ExprEq dom) =>
-    Proxy ctx -> AST dom a -> AST dom b -> Bool
-alphaEq ctx a b = runReader (alphaEqM ctx (\a b -> return $ exprEq a b) a b) []
-
-
-
--- | Evaluation of possibly open lambda expressions
-evalLambdaM :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>
-    ASTF (Lambda ctx :+: Variable ctx :+: dom) a -> m a
-evalLambdaM = liftM result . eval
-  where
-    eval :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>
-        AST (Lambda ctx :+: Variable ctx :+: dom) a -> m a
-    eval (Symbol (InjectR (InjectL (Variable v)))) = do
-        env <- ask
-        case lookup v env of
-          Nothing -> return $ error "eval: evaluating free variable"
-          Just a  -> case fromDynamic a of
-            Just a -> return (Full a)
-            _      -> return $ error "eval: internal type error"
-
-    eval (Symbol (InjectL (Lambda v)) :$: body) = do
-        env <- ask
-        return
-            $ Full
-            $ \a -> flip runReader ((v,toDyn a):env)
-            $ liftM result
-            $ eval body
-
-    eval (f :$: a) = do
-        f' <- eval f
-        a' <- eval a
-        return (f' $: result a')
-
-    eval (Symbol (InjectR (InjectR a))) = return (evaluate a)
-
-
-
--- | Evaluation of closed lambda expressions
-evalLambda :: Eval dom => ASTF (Lambda ctx :+: Variable ctx :+: dom) a -> a
-evalLambda = flip runReader [] . evalLambdaM
-
-
-
 -- | The class of n-ary binding functions
 class NAry ctx a dom | a -> dom
     -- Note: using a functional dependency rather than an associated type,
@@ -268,4 +191,86 @@
 prjLet :: (Let ctxa ctxb :<: sup) =>
     Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a)
 prjLet _ _ = project
+
+
+
+--------------------------------------------------------------------------------
+-- * Interpretation
+--------------------------------------------------------------------------------
+
+-- | Alpha equivalence in an environment of variable equivalences. The supplied
+-- equivalence function gets called when the argument expressions are not both
+-- 'Variable's, both 'Lambda's or both ':$:'.
+alphaEqM :: (Lambda ctx :<: dom, Variable ctx :<: dom)
+    => Proxy ctx
+    -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool)
+    -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool)
+
+-- TODO This function is not ideal, since the type says nothing about which
+--      cases have been handled when calling 'eq'.
+
+alphaEqM ctx eq
+    ((prjLambda ctx -> Just (Lambda v1)) :$: a1)
+    ((prjLambda ctx -> Just (Lambda v2)) :$: a2) =
+        local ((v1,v2):) $ alphaEqM ctx eq a1 a2
+
+alphaEqM ctx eq
+    (prjVariable ctx -> Just (Variable v1))
+    (prjVariable ctx -> Just (Variable v2)) = do
+        env <- ask
+        case lookup v1 env of
+          Nothing  -> return (v1==v2)   -- Free variables
+          Just v2' -> return (v2==v2')
+
+alphaEqM ctx eq (f1 :$: a1) (f2 :$: a2) = do
+    e <- alphaEqM ctx eq f1 f2
+    if e then alphaEqM ctx eq a1 a2 else return False
+
+alphaEqM _ eq a b = eq a b
+
+
+
+-- | Alpha-equivalence on lambda expressions. Free variables are taken to be
+-- equivalent if they have the same identifier.
+alphaEq :: (Lambda ctx :<: dom, Variable ctx :<: dom, ExprEq dom) =>
+    Proxy ctx -> AST dom a -> AST dom b -> Bool
+alphaEq ctx a b = runReader (alphaEqM ctx (\a b -> return $ exprEq a b) a b) []
+
+
+
+-- | Evaluation of possibly open lambda expressions
+evalLambdaM :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>
+    ASTF (Lambda ctx :+: Variable ctx :+: dom) a -> m a
+evalLambdaM = liftM result . eval
+  where
+    eval :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>
+        AST (Lambda ctx :+: Variable ctx :+: dom) a -> m a
+    eval (Symbol (InjectR (InjectL (Variable v)))) = do
+        env <- ask
+        case lookup v env of
+          Nothing -> return $ error "eval: evaluating free variable"
+          Just a  -> case fromDynamic a of
+            Just a -> return (Full a)
+            _      -> return $ error "eval: internal type error"
+
+    eval (Symbol (InjectL (Lambda v)) :$: body) = do
+        env <- ask
+        return
+            $ Full
+            $ \a -> flip runReader ((v,toDyn a):env)
+            $ liftM result
+            $ eval body
+
+    eval (f :$: a) = do
+        f' <- eval f
+        a' <- eval a
+        return (f' $: result a')
+
+    eval (Symbol (InjectR (InjectR a))) = return (evaluate a)
+
+
+
+-- | Evaluation of closed lambda expressions
+evalLambda :: Eval dom => ASTF (Lambda ctx :+: Variable ctx :+: dom) a -> a
+evalLambda = flip runReader [] . evalLambdaM
 
diff --git a/Language/Syntactic/Features/Binding/PartialEval.hs b/Language/Syntactic/Features/Binding/PartialEval.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Features/Binding/PartialEval.hs
@@ -0,0 +1,144 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Partial evaluation
+
+module Language.Syntactic.Features.Binding.PartialEval where
+
+
+
+import Control.Monad.Writer
+import Data.Set as Set
+
+import Data.Proxy
+
+import Language.Syntactic
+import Language.Syntactic.Features.Symbol
+import Language.Syntactic.Features.Literal
+import Language.Syntactic.Features.Condition
+import Language.Syntactic.Features.Tuple
+import Language.Syntactic.Features.Binding
+
+
+
+-- | Constant folder
+--
+-- Given an expression and the statically known value of that expression,
+-- returns a (possibly) new expression with the same meaning as the original.
+-- Typically, the result will be a 'Literal', if the relevant type constraints
+-- are satisfied.
+type ConstFolder ctx dom = forall a
+    .  ASTF (Lambda ctx :+: Variable ctx :+: dom) a
+    -> a
+    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a
+
+-- | Partial evaluation
+class Eval dom => PartialEval feature ctx dom
+  where
+    -- | Partial evaluation of a feature. The @(`Set` `VarId`)@ returned is the
+    -- set of free variables of the expression. However, free variables are
+    -- counted in a \"lazy\" sense: free variables from sub-expressions that are
+    -- never evaluated may not be counted. (The instance for 'Conditional' will
+    -- throw away the free variables of the pruned branch when the condition is
+    -- statically known. This is one reason why partial evaluation and free
+    -- variable calculation have to be done simultaneously.)
+    partEvalFeat
+        :: Proxy ctx
+        -> ConstFolder ctx dom
+        -> feature a
+        -> HList (AST (Lambda ctx :+: Variable ctx :+: dom)) a
+        -> Writer
+            (Set VarId)
+            (ASTF (Lambda ctx :+: Variable ctx :+: dom) (EvalResult a))
+
+instance (PartialEval sub1 ctx dom, PartialEval sub2 ctx dom) =>
+    PartialEval (sub1 :+: sub2) ctx dom
+  where
+    partEvalFeat ctx constFold (InjectL a) = partEvalFeat ctx constFold a
+    partEvalFeat ctx constFold (InjectR a) = partEvalFeat ctx constFold a
+
+partialEvalM :: PartialEval dom ctx dom
+    => Proxy ctx
+    -> ConstFolder ctx dom
+    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a
+    -> Writer (Set VarId) (ASTF (Lambda ctx :+: Variable ctx :+: dom) a)
+partialEvalM ctx constFold = transformNodeC (partEvalFeat ctx constFold)
+
+-- | Partially evaluate an expression
+partialEval :: PartialEval dom ctx dom
+    => Proxy ctx
+    -> ConstFolder ctx dom
+    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a
+    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a
+partialEval ctx constFold = fst . runWriter . partialEvalM ctx constFold
+
+
+
+-- | Convenient default implementation of 'partEvalFeat' (uses 'evalLambda' to
+-- evaluate)
+partEvalFeatDefault
+    :: ( feature :<: dom
+       , WitnessCons feature
+       , PartialEval dom ctx dom
+       )
+    => Proxy ctx
+    -> ConstFolder ctx dom
+    -> feature a
+    -> HList (AST (Lambda ctx :+: Variable ctx :+: dom)) a
+    -> Writer
+        (Set VarId)
+        (ASTF (Lambda ctx :+: Variable ctx :+: dom) (EvalResult a))
+partEvalFeatDefault ctx constFold feat@(witnessCons -> ConsWit) args = do
+    (args',vars) <- listen $ mapHListM (partialEvalM ctx constFold) args
+    let result = appHList (Symbol $ InjectR $ InjectR $ inject feat) args'
+        value  = evalLambda result
+    if Set.null vars
+      then return $ constFold result value
+      else return result
+
+instance (Sym ctx' :<: dom, PartialEval dom ctx dom) =>
+    PartialEval (Sym ctx') ctx dom
+  where
+    partEvalFeat = partEvalFeatDefault
+
+instance (Literal ctx' :<: dom, PartialEval dom ctx dom) =>
+    PartialEval (Literal ctx') ctx dom
+  where
+    partEvalFeat = partEvalFeatDefault
+
+instance (Condition ctx' :<: dom, PartialEval dom ctx dom) =>
+    PartialEval (Condition ctx') ctx dom
+  where
+    partEvalFeat ctx constFold cond@Condition args@(c :*: t :*: e :*: Nil)
+        | Set.null cVars = partialEvalM ctx constFold t_or_e
+        | otherwise      = partEvalFeatDefault ctx constFold cond args
+      where
+        (c',cVars) = runWriter $ partialEvalM ctx constFold c
+        t_or_e     = if evalLambda c' then t else e
+
+instance (Tuple ctx' :<: dom, PartialEval dom ctx dom) =>
+    PartialEval (Tuple ctx') ctx dom
+  where
+    partEvalFeat = partEvalFeatDefault
+
+instance (Select ctx' :<: dom, PartialEval dom ctx dom) =>
+    PartialEval (Select ctx') ctx dom
+  where
+    partEvalFeat = partEvalFeatDefault
+
+instance PartialEval dom ctx dom => PartialEval (Variable ctx) ctx dom
+  where
+    partEvalFeat _ _ var@(Variable v) Nil = do
+        tell (singleton v)
+        return (inject var)
+
+instance PartialEval dom ctx dom => PartialEval (Lambda ctx) ctx dom
+  where
+    partEvalFeat ctx constFold lam@(Lambda v) (body :*: Nil) = do
+        body' <- censor (delete v) $ partialEvalM ctx constFold body
+        return $ inject lam :$: body'
+
+instance (Let ctxa ctxb :<: dom, PartialEval dom ctx dom) =>
+    PartialEval (Let ctxa ctxb) ctx dom
+  where
+    partEvalFeat = partEvalFeatDefault
+
diff --git a/Language/Syntactic/Features/Condition.hs b/Language/Syntactic/Features/Condition.hs
--- a/Language/Syntactic/Features/Condition.hs
+++ b/Language/Syntactic/Features/Condition.hs
@@ -8,6 +8,7 @@
 import Data.Proxy
 
 import Language.Syntactic
+import Language.Syntactic.Features.Symbol
 
 
 
@@ -24,21 +25,14 @@
     type Context (Condition ctx) = ctx
     witnessSat Condition = Witness'
 
-instance ExprEq (Condition ctx)
-  where
-    exprEq Condition Condition = True
-    exprHash Condition         = hashInt 0
-
-instance Render (Condition ctx)
+instance IsSymbol (Condition ctx)
   where
-    render Condition = "condition"
+    toSym Condition = Sym "condition" (\c t e -> if c then t else e)
 
+instance ExprEq (Condition ctx) where exprEq = exprEqSym; exprHash = exprHashSym
+instance Render (Condition ctx) where renderPart = renderPartSym
+instance Eval   (Condition ctx) where evaluate   = evaluateSym
 instance ToTree (Condition ctx)
-
-instance Eval (Condition ctx)
-  where
-    evaluate Condition = fromEval $
-        \cond tHEN eLSE -> if cond then tHEN else eLSE
 
 
 
diff --git a/Language/Syntactic/Features/Symbol.hs b/Language/Syntactic/Features/Symbol.hs
--- a/Language/Syntactic/Features/Symbol.hs
+++ b/Language/Syntactic/Features/Symbol.hs
@@ -12,25 +12,43 @@
 import Data.Typeable
 
 import Data.Hash
+import Data.Proxy
 
 import Language.Syntactic
 
 
 
-data Sym a
+data Sym ctx a
   where
-    Sym :: ConsType a => String -> ConsEval a -> Sym a
+    Sym :: (ConsType a, Sat ctx (EvalResult a)) =>
+        String -> ConsEval a -> Sym ctx a
 
-instance WitnessCons Sym
+instance WitnessCons (Sym ctx)
   where
     witnessCons (Sym _ _) = ConsWit
 
-instance ExprEq Sym
+instance WitnessSat (Sym ctx)
   where
+    type Context (Sym ctx) = ctx
+    witnessSat (Sym _ _) = Witness'
+
+witnessSatSym :: forall ctx dom a . (Sym ctx :<: dom)
+    => Proxy ctx
+    -> ASTF dom a
+    -> Maybe (Witness' ctx a)
+witnessSatSym ctx = witSym
+  where
+    witSym :: (EvalResult b ~ a) => AST dom b -> Maybe (Witness' ctx a)
+    witSym (prjSym ctx -> Just (Sym _ _)) = Just Witness'
+    witSym (f :$: _) = witSym f
+    witSym _         = Nothing
+
+instance ExprEq (Sym ctx)
+  where
     exprEq (Sym a _) (Sym b _) = a==b
     exprHash (Sym name _)      = hash name
 
-instance Render Sym
+instance Render (Sym ctx)
   where
     renderPart [] (Sym name _) = name
     renderPart args (Sym name _)
@@ -45,9 +63,9 @@
           && last name == ')'
           && length args == 2
 
-instance ToTree Sym
+instance ToTree (Sym ctx)
 
-instance Eval Sym
+instance Eval (Sym ctx)
   where
     evaluate (Sym _ a) = fromEval a
 
@@ -55,52 +73,59 @@
 
 -- | A zero-argument symbol
 sym0
-    :: ( Typeable a
-       , Sym :<: dom
+    :: ( Sat ctx a
+       , Sym ctx :<: dom
        )
-    => String
+    => Proxy ctx
+    -> String
     -> a
     -> ASTF dom a
-sym0 name a = inject (Sym name a)
+sym0 ctx name a = inject (Sym name a `withContext` ctx)
 
 -- | A one-argument symbol
 sym1
     :: ( Typeable a
-       , Sym :<: dom
+       , Sat ctx b
+       , Sym ctx :<: dom
        )
-    => String
+    => Proxy ctx
+    -> String
     -> (a -> b)
     -> ASTF dom a
     -> ASTF dom b
-sym1 name f a = inject (Sym name f) :$: a
+sym1 ctx name f a = inject (Sym name f `withContext` ctx) :$: a
 
 -- | A two-argument symbol
 sym2
     :: ( Typeable a
        , Typeable b
-       , Sym :<: dom
+       , Sat ctx c
+       , Sym ctx :<: dom
        )
-    => String
+    => Proxy ctx
+    -> String
     -> (a -> b -> c)
     -> ASTF dom a
     -> ASTF dom b
     -> ASTF dom c
-sym2 name f a b = inject (Sym name f) :$: a :$: b
+sym2 ctx name f a b = inject (Sym name f `withContext` ctx) :$: a :$: b
 
 -- | A three-argument symbol
 sym3
     :: ( Typeable a
        , Typeable b
        , Typeable c
-       , Sym :<: dom
+       , Sat ctx d
+       , Sym ctx :<: dom
        )
-    => String
+    => Proxy ctx
+    -> String
     -> (a -> b -> c -> d)
     -> ASTF dom a
     -> ASTF dom b
     -> ASTF dom c
     -> ASTF dom d
-sym3 name f a b c = inject (Sym name f) :$: a :$: b :$: c
+sym3 ctx name f a b c = inject (Sym name f `withContext` ctx) :$: a :$: b :$: c
 
 -- | A four-argument symbol
 sym4
@@ -108,37 +133,47 @@
        , Typeable b
        , Typeable c
        , Typeable d
-       , Sym :<: dom
+       , Sat ctx e
+       , Sym ctx :<: dom
        )
-    => String
+    => Proxy ctx
+    -> String
     -> (a -> b -> c -> d -> e)
     -> ASTF dom a
     -> ASTF dom b
     -> ASTF dom c
     -> ASTF dom d
     -> ASTF dom e
-sym4 name f a b c d = inject (Sym name f) :$: a :$: b :$: c :$: d
+sym4 ctx name f a b c d =
+    inject (Sym name f `withContext` ctx) :$: a :$: b :$: c :$: d
 
 
 
+-- | Partial symbol projection with explicit context
+prjSym :: (Sym ctx :<: sup) =>
+    Proxy ctx -> sup a -> Maybe (Sym ctx a)
+prjSym _ = project
+
+
+
 -- | Class of expressions that can be treated as symbols
 class IsSymbol expr
   where
-    toSym :: expr a -> Sym a
+    toSym :: expr a -> Sym Poly a
 
 -- | Default implementation of 'exprEq'
-exprEqFunc :: IsSymbol expr => expr a -> expr b -> Bool
-exprEqFunc a b = exprEq (toSym a) (toSym b)
+exprEqSym :: IsSymbol expr => expr a -> expr b -> Bool
+exprEqSym a b = exprEq (toSym a) (toSym b)
 
 -- | Default implementation of 'exprHash'
-exprHashFunc :: IsSymbol expr => expr a -> Hash
-exprHashFunc = exprHash . toSym
+exprHashSym :: IsSymbol expr => expr a -> Hash
+exprHashSym = exprHash . toSym
 
 -- | Default implementation of 'renderPart'
-renderPartFunc :: IsSymbol expr => [String] -> expr a -> String
-renderPartFunc args = renderPart args . toSym
+renderPartSym :: IsSymbol expr => [String] -> expr a -> String
+renderPartSym args = renderPart args . toSym
 
 -- | Default implementation of 'evaluate'
-evaluateFunc :: IsSymbol expr => expr a -> a
-evaluateFunc = evaluate . toSym
+evaluateSym :: IsSymbol expr => expr a -> a
+evaluateSym = evaluate . toSym
 
diff --git a/Language/Syntactic/Features/Tuple.hs b/Language/Syntactic/Features/Tuple.hs
--- a/Language/Syntactic/Features/Tuple.hs
+++ b/Language/Syntactic/Features/Tuple.hs
@@ -64,9 +64,9 @@
     toSym Tup6 = Sym "tup6" (,,,,,)
     toSym Tup7 = Sym "tup7" (,,,,,,)
 
-instance ExprEq (Tuple ctx) where exprEq = exprEqFunc; exprHash = exprHashFunc
-instance Render (Tuple ctx) where renderPart = renderPartFunc
-instance Eval   (Tuple ctx) where evaluate   = evaluateFunc
+instance ExprEq (Tuple ctx) where exprEq = exprEqSym; exprHash = exprHashSym
+instance Render (Tuple ctx) where renderPart = renderPartSym
+instance Eval   (Tuple ctx) where evaluate   = evaluateSym
 instance ToTree (Tuple ctx)
 
 -- | Partial `Tuple` projection with explicit context
@@ -231,9 +231,9 @@
     toSym Sel6 = Sym "sel6" sel6
     toSym Sel7 = Sym "sel7" sel7
 
-instance ExprEq (Select ctx) where exprEq = exprEqFunc; exprHash = exprHashFunc
-instance Render (Select ctx) where renderPart = renderPartFunc
-instance Eval   (Select ctx) where evaluate   = evaluateFunc
+instance ExprEq (Select ctx) where exprEq = exprEqSym; exprHash = exprHashSym
+instance Render (Select ctx) where renderPart = renderPartSym
+instance Eval   (Select ctx) where evaluate   = evaluateSym
 instance ToTree (Select ctx)
 
 -- | Partial `Select` projection with explicit context
diff --git a/Language/Syntactic/Features/TupleSyntacticSimple.hs b/Language/Syntactic/Features/TupleSyntacticSimple.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Features/TupleSyntacticSimple.hs
@@ -0,0 +1,138 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | 'Syntactic' instances for tuples with 'SimpleCtx' context
+module Language.Syntactic.Features.TupleSyntacticSimple where
+
+
+
+import Language.Syntactic.Syntax
+import Language.Syntactic.Features.Tuple
+
+
+
+instance
+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)
+    , Syntactic b dom, Eq (Internal b), Show (Internal b)
+    , Tuple  SimpleCtx :<: dom
+    , Select SimpleCtx :<: dom
+    ) =>
+      Syntactic (a,b) dom
+  where
+    type Internal (a,b) =
+        ( Internal a
+        , Internal b
+        )
+
+    desugar = desugarTup2 simpleCtx
+    sugar   = sugarTup2 simpleCtx
+
+instance
+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)
+    , Syntactic b dom, Eq (Internal b), Show (Internal b)
+    , Syntactic c dom, Eq (Internal c), Show (Internal c)
+    , Tuple  SimpleCtx :<: dom
+    , Select SimpleCtx :<: dom
+    ) =>
+      Syntactic (a,b,c) dom
+  where
+    type Internal (a,b,c) =
+        ( Internal a
+        , Internal b
+        , Internal c
+        )
+
+    desugar = desugarTup3 simpleCtx
+    sugar   = sugarTup3 simpleCtx
+
+instance
+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)
+    , Syntactic b dom, Eq (Internal b), Show (Internal b)
+    , Syntactic c dom, Eq (Internal c), Show (Internal c)
+    , Syntactic d dom, Eq (Internal d), Show (Internal d)
+    , Tuple  SimpleCtx :<: dom
+    , Select SimpleCtx :<: dom
+    ) =>
+      Syntactic (a,b,c,d) dom
+  where
+    type Internal (a,b,c,d) =
+        ( Internal a
+        , Internal b
+        , Internal c
+        , Internal d
+        )
+
+    desugar = desugarTup4 simpleCtx
+    sugar   = sugarTup4 simpleCtx
+
+instance
+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)
+    , Syntactic b dom, Eq (Internal b), Show (Internal b)
+    , Syntactic c dom, Eq (Internal c), Show (Internal c)
+    , Syntactic d dom, Eq (Internal d), Show (Internal d)
+    , Syntactic e dom, Eq (Internal e), Show (Internal e)
+    , Tuple  SimpleCtx :<: dom
+    , Select SimpleCtx :<: dom
+    ) =>
+      Syntactic (a,b,c,d,e) dom
+  where
+    type Internal (a,b,c,d,e) =
+        ( Internal a
+        , Internal b
+        , Internal c
+        , Internal d
+        , Internal e
+        )
+
+    desugar = desugarTup5 simpleCtx
+    sugar   = sugarTup5 simpleCtx
+
+instance
+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)
+    , Syntactic b dom, Eq (Internal b), Show (Internal b)
+    , Syntactic c dom, Eq (Internal c), Show (Internal c)
+    , Syntactic d dom, Eq (Internal d), Show (Internal d)
+    , Syntactic e dom, Eq (Internal e), Show (Internal e)
+    , Syntactic f dom, Eq (Internal f), Show (Internal f)
+    , Tuple  SimpleCtx :<: dom
+    , Select SimpleCtx :<: dom
+    ) =>
+      Syntactic (a,b,c,d,e,f) dom
+  where
+    type Internal (a,b,c,d,e,f) =
+        ( Internal a
+        , Internal b
+        , Internal c
+        , Internal d
+        , Internal e
+        , Internal f
+        )
+
+    desugar = desugarTup6 simpleCtx
+    sugar   = sugarTup6 simpleCtx
+
+instance
+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)
+    , Syntactic b dom, Eq (Internal b), Show (Internal b)
+    , Syntactic c dom, Eq (Internal c), Show (Internal c)
+    , Syntactic d dom, Eq (Internal d), Show (Internal d)
+    , Syntactic e dom, Eq (Internal e), Show (Internal e)
+    , Syntactic f dom, Eq (Internal f), Show (Internal f)
+    , Syntactic g dom, Eq (Internal g), Show (Internal g)
+    , Tuple  SimpleCtx :<: dom
+    , Select SimpleCtx :<: dom
+    ) =>
+      Syntactic (a,b,c,d,e,f,g) dom
+  where
+    type Internal (a,b,c,d,e,f,g) =
+        ( Internal a
+        , Internal b
+        , Internal c
+        , Internal d
+        , Internal e
+        , Internal f
+        , Internal g
+        )
+
+    desugar = desugarTup7 simpleCtx
+    sugar   = sugarTup7 simpleCtx
+
diff --git a/Language/Syntactic/Interpretation/Equality.hs b/Language/Syntactic/Interpretation/Equality.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Interpretation/Equality.hs
@@ -0,0 +1,52 @@
+module Language.Syntactic.Interpretation.Equality where
+
+
+
+import Data.Hash
+
+import Language.Syntactic.Syntax
+
+
+
+-- | Equality for expressions. The difference between 'Eq' and 'ExprEq' is that
+-- 'ExprEq' allows comparison of expressions with different value types. It is
+-- assumed that when the types differ, the expressions also differ. The reason
+-- for allowing comparison of different types is that this is convenient when
+-- the types are existentially quantified.
+class ExprEq expr
+  where
+    exprEq :: expr a -> expr b -> Bool
+
+    -- | Computes a 'Hash' for an expression. Expressions that are equal
+    -- according to 'exprEq' must result in the same hash:
+    --
+    -- @`exprEq` a b  ==>  `exprHash` a == `exprHash` b@
+    exprHash :: expr a -> Hash
+
+
+instance ExprEq dom => ExprEq (AST dom)
+  where
+    exprEq (Symbol a)  (Symbol b)  = exprEq a b
+    exprEq (f1 :$: a1) (f2 :$: a2) = exprEq f1 f2 && exprEq a1 a2
+    exprEq _ _ = False
+
+    exprHash (Symbol a) = hashInt 0 `combine` exprHash a
+    exprHash (f :$: a)  = hashInt 1 `combine` exprHash f `combine` exprHash a
+
+instance ExprEq dom => Eq (AST dom a)
+  where
+    (==) = exprEq
+
+instance (ExprEq expr1, ExprEq expr2) => ExprEq (expr1 :+: expr2)
+  where
+    exprEq (InjectL a) (InjectL b) = exprEq a b
+    exprEq (InjectR a) (InjectR b) = exprEq a b
+    exprEq _ _ = False
+
+    exprHash (InjectL a) = hashInt 0 `combine` exprHash a
+    exprHash (InjectR a) = hashInt 1 `combine` exprHash a
+
+instance (ExprEq expr1, ExprEq expr2) => Eq ((expr1 :+: expr2) a)
+  where
+    (==) = exprEq
+
diff --git a/Language/Syntactic/Interpretation/Evaluation.hs b/Language/Syntactic/Interpretation/Evaluation.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Interpretation/Evaluation.hs
@@ -0,0 +1,26 @@
+module Language.Syntactic.Interpretation.Evaluation where
+
+
+
+import Language.Syntactic.Syntax
+
+
+
+class Eval expr
+  where
+    -- | Evaluation of expressions
+    evaluate :: expr a -> a
+
+instance Eval dom => Eval (AST dom)
+  where
+    evaluate (Symbol a) = evaluate a
+    evaluate (f :$: a)  = evaluate f $: result (evaluate a)
+
+instance (Eval expr1, Eval expr2) => Eval (expr1 :+: expr2)
+  where
+    evaluate (InjectL a) = evaluate a
+    evaluate (InjectR a) = evaluate a
+
+evalFull :: Eval dom => ASTF dom a -> a
+evalFull = result . evaluate
+
diff --git a/Language/Syntactic/Interpretation/Render.hs b/Language/Syntactic/Interpretation/Render.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Interpretation/Render.hs
@@ -0,0 +1,83 @@
+module Language.Syntactic.Interpretation.Render
+    ( Render (..)
+    , printExpr
+    , ToTree (..)
+    , showAST
+    , drawAST
+    ) where
+
+
+
+import Data.Tree
+
+import Language.Syntactic.Syntax
+
+
+
+-- | Render an expression as concrete syntax. A complete instance must define
+-- either of the methods 'render' and 'renderPart'.
+class Render expr
+  where
+    -- | Render an expression as a 'String'
+    render :: expr a -> String
+    render = renderPart []
+
+    -- | Render a partially applied constructor given a list of rendered missing
+    -- arguments
+    renderPart :: [String] -> expr a -> String
+    renderPart []   a = render a
+    renderPart args a = "(" ++ unwords (render a : args) ++ ")"
+
+instance Render dom => Render (AST dom)
+  where
+    renderPart args (Symbol a) = renderPart args a
+    renderPart args (f :$: a)  = renderPart (render a : args) f
+
+instance Render dom => Show (AST dom a)
+  where
+    show = render
+
+instance (Render expr1, Render expr2) => Render (expr1 :+: expr2)
+  where
+    renderPart args (InjectL a) = renderPart args a
+    renderPart args (InjectR a) = renderPart args a
+
+instance (Render expr1, Render expr2) => Show ((expr1 :+: expr2) a)
+  where
+    show = render
+
+-- | Print an expression
+printExpr :: Render expr => expr a -> IO ()
+printExpr = putStrLn . render
+
+
+
+class Render expr => ToTree expr
+  where
+    -- | Convert a partially applied constructor to a syntax tree given a list
+    -- of rendered missing arguments
+    toTreePart :: [Tree String] -> expr a -> Tree String
+    toTreePart args a = Node (render a) args
+
+instance ToTree dom => ToTree (AST dom)
+  where
+    toTreePart args (Symbol a) = toTreePart args a
+    toTreePart args (f :$: a)  = toTreePart (toTree a : args) f
+
+instance (ToTree expr1, ToTree expr2) => ToTree (expr1 :+: expr2)
+  where
+    toTreePart args (InjectL a) = toTreePart args a
+    toTreePart args (InjectR a) = toTreePart args a
+
+-- | Convert an expression to a syntax tree
+toTree :: ToTree expr => expr a -> Tree String
+toTree = toTreePart []
+
+-- | Show syntax tree using ASCII art
+showAST :: ToTree dom => AST dom a -> String
+showAST = drawTree . toTree
+
+-- | Print syntax tree using ASCII art
+drawAST :: ToTree dom => AST dom a -> IO ()
+drawAST = putStrLn . showAST
+
diff --git a/Language/Syntactic/Sharing/ReifyHO.hs b/Language/Syntactic/Sharing/ReifyHO.hs
--- a/Language/Syntactic/Sharing/ReifyHO.hs
+++ b/Language/Syntactic/Sharing/ReifyHO.hs
@@ -10,7 +10,6 @@
 -- This module is based on /Type-Safe Observable Sharing in Haskell/ (Andy Gill,
 -- /Haskell Symposium/, 2009).
 
-
 module Language.Syntactic.Sharing.ReifyHO
     ( reifyGraphTop
     , reifyGraph
diff --git a/Language/Syntactic/Syntax.hs b/Language/Syntactic/Syntax.hs
--- a/Language/Syntactic/Syntax.hs
+++ b/Language/Syntactic/Syntax.hs
@@ -70,6 +70,7 @@
     , listHList
     , listHListM
     , mapHList
+    , mapHListM
     , appHList
     , ($:)
     , AST (..)
@@ -84,19 +85,32 @@
       -- * AST processing
     , queryNodeI
     , queryNode
+    , transformNodeC
     , transformNode
       -- * Restricted syntax trees
     , Sat (..)
+    , Witness (PolyWit, SimpleWit)
+        -- TODO A warning reports that these are already exported by 'Sat (..)',
+        --      but that is actually not the case. This seems to have been fixed
+        --      recently:
+        --
+        --        http://hackage.haskell.org/trac/ghc/ticket/2436#comment:12
+        --
+        --      I don't know if the fix just removes the warning, or if it means
+        --      that 'Sat (..)' is enough.
     , Witness' (..)
     , witness'
     , WitnessSat (..)
     , withContext
     , Poly
     , poly
+    , SimpleCtx
+    , simpleCtx
     ) where
 
 
 
+import Control.Monad.Identity
 import Data.Typeable
 
 import Data.Proxy
@@ -146,6 +160,7 @@
     listHList'  :: (forall a . c (Full a) -> b) -> HList c a -> [b]
     listHListM' :: Monad m => (forall a . c (Full a) -> m b) -> HList c a -> m [b]
     mapHList'   :: (forall a . c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a
+    mapHListM'  :: Monad m => (forall a . c1 (Full a) -> m (c2 (Full a))) -> HList c1 a -> m (HList c2 a)
     appHList'   :: AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a)
 
 
@@ -159,7 +174,8 @@
     listHList'  f Nil = []
     listHListM' f Nil = return []
     mapHList'   f Nil = Nil
-    appHList' a Nil   = a
+    mapHListM'  f Nil = return Nil
+    appHList'   a Nil = a
 
 instance ConsType' b => ConsType' (a :-> b)
   where
@@ -171,7 +187,8 @@
     listHList'  f (a :*: as) = f a : listHList' f as
     listHListM' f (a :*: as) = sequence (f a : listHList' f as)
     mapHList'   f (a :*: as) = f a :*: mapHList' f as
-    appHList' c (a :*: as)   = appHList' (c :$: a) as
+    mapHListM'  f (a :*: as) = liftM2 (:*:) (f a) (mapHListM' f as)
+    appHList'   c (a :*: as) = appHList' (c :$: a) as
 
 -- | Fully or partially applied constructor
 --
@@ -226,6 +243,12 @@
     (forall a . c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a
 mapHList = mapHList'
 
+-- | Change the container of each element in a heterogeneous list, monadic
+-- version
+mapHListM :: (Monad m, ConsType a) =>
+    (forall a . c1 (Full a) -> m (c2 (Full a))) -> HList c1 a -> m (HList c2 a)
+mapHListM = mapHListM'
+
 -- | Apply the syntax tree to listed arguments
 appHList :: ConsType a =>
     AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a)
@@ -316,7 +339,7 @@
 --
 -- > eval a == eval (desugar $ (id :: A -> A) $ sugar a)
 --
--- (using 'Language.Syntactic.Analysis.Evaluation.eval')
+-- (using 'Language.Syntactic.Interpretation.Evaluation.eval')
 class Typeable (Internal a) => Syntactic a dom | a -> dom
     -- Note: using a functional dependency rather than an associated type,
     -- because this makes it possible to make a class alias constraining dom.
@@ -379,6 +402,9 @@
 -- * AST processing
 --------------------------------------------------------------------------------
 
+newtype Wrap a b = Wrap {unWrap :: a}
+  -- Only used in the definition of 'queryNode'
+
 -- | Like 'queryNode' but with the result indexed by the constructor's result
 -- type
 queryNodeI :: forall dom a b
@@ -390,9 +416,6 @@
     query (Symbol a) args = f a args
     query (c :$: a)  args = query c (a :*: args)
 
-newtype Wrap a b = Wrap {unWrap :: a}
-  -- Only used in the definition of 'queryNode'
-
 -- | Query an 'AST' using a function that gets direct access to the top-most
 -- constructor and its sub-trees
 --
@@ -431,10 +454,23 @@
 queryNode :: forall dom a b
     .  (forall a . ConsType a => dom a -> HList (AST dom) a -> b)
     -> ASTF dom a -> b
-queryNode f a = unWrap $ queryNodeI (\c args -> Wrap $ f c args) a
+queryNode f a = unWrap $ queryNodeI (\c -> Wrap . f c) a
 
 
 
+-- | Like 'transformNode' but with the result wrapped in a type constructor @c@
+transformNodeC :: forall dom dom' c a
+    .  (  forall a . ConsType a
+       => dom a -> HList (AST dom) a -> c (ASTF dom' (EvalResult a))
+       )
+    -> ASTF dom a
+    -> c (ASTF dom' a)
+transformNodeC f a = transform a Nil
+  where
+    transform :: AST dom b -> HList (AST dom) b -> c (ASTF dom' (EvalResult b))
+    transform (Symbol a) args = f a args
+    transform (c :$: a)  args = transform c (a :*: args)
+
 -- | Transform an 'AST' using a function that gets direct access to the top-most
 -- constructor and its sub-trees. This function is similar to 'queryNode', but
 -- returns a transformed 'AST' rather than abstract interpretation.
@@ -442,12 +478,9 @@
     .  (  forall a . ConsType a
        => dom a -> HList (AST dom) a -> ASTF dom' (EvalResult a)
        )
-    -> ASTF dom a -> ASTF dom' a
-transformNode f a = transform a Nil
-  where
-    transform :: AST dom b -> HList (AST dom) b -> ASTF dom' (EvalResult b)
-    transform (Symbol a) args = f a args
-    transform (c :$: a)  args = transform c (a :*: args)
+    -> ASTF dom a
+    -> ASTF dom' a
+transformNode f a = runIdentity $ transformNodeC (\c -> Identity . f c) a
 
 
 
@@ -510,4 +543,16 @@
 
 poly :: Proxy Poly
 poly = Proxy
+
+-- | Representation of \"simple\" types: types satisfying
+-- @(`Eq` a, `Show` a, `Typeable` a)@
+data SimpleCtx
+
+instance (Eq a, Show a, Typeable a) => Sat SimpleCtx a
+  where
+    data Witness SimpleCtx a = (Eq a, Show a, Typeable a) => SimpleWit
+    witness = SimpleWit
+
+simpleCtx :: Proxy SimpleCtx
+simpleCtx = Proxy
 
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        0.5
+Version:        0.6
 Synopsis:       Generic abstract syntax, and utilities for embedded languages
 Description:    This library provides:
                 .
@@ -38,6 +38,7 @@
 Extra-source-files:
   Examples/ALaCarte.hs
   Examples/NanoFeldspar/Core.hs
+  Examples/NanoFeldspar/Extra.hs
   Examples/NanoFeldspar/Vector.hs
   Examples/NanoFeldspar/Test.hs
 
@@ -49,17 +50,19 @@
   Exposed-modules:
     Language.Syntactic
     Language.Syntactic.Syntax
-    Language.Syntactic.Analysis.Equality
-    Language.Syntactic.Analysis.Render
-    Language.Syntactic.Analysis.Evaluation
+    Language.Syntactic.Interpretation.Equality
+    Language.Syntactic.Interpretation.Render
+    Language.Syntactic.Interpretation.Evaluation
     Language.Syntactic.Features.Annotate
     Language.Syntactic.Features.Symbol
     Language.Syntactic.Features.Literal
     Language.Syntactic.Features.Condition
     Language.Syntactic.Features.Tuple
     Language.Syntactic.Features.TupleSyntacticPoly
+    Language.Syntactic.Features.TupleSyntacticSimple
     Language.Syntactic.Features.Binding
     Language.Syntactic.Features.Binding.HigherOrder
+    Language.Syntactic.Features.Binding.PartialEval
     Language.Syntactic.Sharing.Utils
     Language.Syntactic.Sharing.Graph
     Language.Syntactic.Sharing.StableName