diff --git a/benchmarks/JoiningTypes.hs b/benchmarks/JoiningTypes.hs
--- a/benchmarks/JoiningTypes.hs
+++ b/benchmarks/JoiningTypes.hs
@@ -3,8 +3,7 @@
 module JoiningTypes (main) where
 
 import Criterion.Main
-import Criterion.Config
-import Data.Monoid
+import Criterion.Types
 import Data.Syntactic
 import Data.Syntactic.Functional
 
@@ -50,11 +49,11 @@
   evalSym EIf     = \c a b -> if c then a else b
 
 instance EvalEnv Expr1 env where
-  compileSym p (EI n) = compileSymDefault p (EI n)
-  compileSym p (EB b) = compileSymDefault p (EB b)
-  compileSym p EAdd   = compileSymDefault p EAdd
-  compileSym p EEq    = compileSymDefault p EEq
-  compileSym p EIf    = compileSymDefault p EIf
+  compileSym p (EI n) = compileSymDefault signature p (EI n)
+  compileSym p (EB b) = compileSymDefault signature p (EB b)
+  compileSym p EAdd   = compileSymDefault signature p EAdd
+  compileSym p EEq    = compileSymDefault signature p EEq
+  compileSym p EIf    = compileSymDefault signature p EIf
 
 -- Joined types
 data ExprI t where
@@ -105,13 +104,13 @@
   evalSym EIfJ    = \c a b -> if c then a else b
 
 instance EvalEnv ExprI env where
-  compileSym p (EIJ n) = compileSymDefault p (EIJ n)
-  compileSym p EAddJ   = compileSymDefault p EAddJ
+  compileSym p (EIJ n) = compileSymDefault signature p (EIJ n)
+  compileSym p EAddJ   = compileSymDefault signature p EAddJ
 
 instance EvalEnv ExprB env where
-  compileSym p (EBJ b) = compileSymDefault p (EBJ b)
-  compileSym p EEqJ    = compileSymDefault p EEqJ
-  compileSym p EIfJ    = compileSymDefault p EIfJ
+  compileSym p (EBJ b) = compileSymDefault signature p (EBJ b)
+  compileSym p EEqJ    = compileSymDefault signature p EEqJ
+  compileSym p EIfJ    = compileSymDefault signature p EIfJ
 
 -- Joined types (4 joins)
 
@@ -181,19 +180,19 @@
   evalSym E4JIf     = \c a b -> if c then a else b
 
 instance EvalEnv Expr4J1 env where
-  compileSym p (E4JI n)  = compileSymDefault p (E4JI n)
+  compileSym p (E4JI n)  = compileSymDefault signature p (E4JI n)
 
 instance EvalEnv Expr4J2 env where
-  compileSym p (E4JB b)  = compileSymDefault p (E4JB b)
+  compileSym p (E4JB b)  = compileSymDefault signature p (E4JB b)
 
 instance EvalEnv Expr4J3 env where
-  compileSym p E4JAdd    = compileSymDefault p E4JAdd
+  compileSym p E4JAdd    = compileSymDefault signature p E4JAdd
 
 instance EvalEnv Expr4J4 env where
-  compileSym p E4JEq     = compileSymDefault p E4JEq
+  compileSym p E4JEq     = compileSymDefault signature p E4JEq
 
 instance EvalEnv Expr4J5 env where
-  compileSym p E4JIf     = compileSymDefault p E4JIf
+  compileSym p E4JIf     = compileSymDefault signature p E4JIf
 
 -- Expressions
 syntacticExpr :: Int -> Expr1' Int
@@ -209,7 +208,7 @@
 syntacticExpr4J n = (add4 (syntacticExpr4J (n-1)) (syntacticExpr4J (n-1)))
 
 main :: IO ()
-main = defaultMainWith (defaultConfig {cfgSummaryFile = Last $ Just "bench-results/joiningTypes.csv"}) (return ())
+main = defaultMainWith (defaultConfig {csvFile = Just "bench-results/joiningTypes.csv"})
          [ bgroup "eval 10" [ bench "syntactic 0 joins" $ nf evalDen (syntacticExpr 10)
                             , bench "syntactic 1 join"  $ nf evalDen (syntacticExprJ 10)
                             , bench "syntactic 4 joins" $ nf evalDen (syntacticExpr4J 10)]
diff --git a/benchmarks/Normal.hs b/benchmarks/Normal.hs
--- a/benchmarks/Normal.hs
+++ b/benchmarks/Normal.hs
@@ -3,13 +3,12 @@
 module Normal (main) where
 
 import Criterion.Main
-import Criterion.Config
-import Data.Monoid
+import Criterion.Types
 import Data.Syntactic
 import Data.Syntactic.Functional
 
 main :: IO ()
-main = defaultMainWith (defaultConfig {cfgSummaryFile = Last $ Just "bench-results/normal.csv"}) (return ())
+main = defaultMainWith (defaultConfig {csvFile = Just "bench-results/normal.csv"})
          [ bgroup "Eval Tree 10"   [ bench "gadt"      $ nf evl (gadtExpr 10)
                                    , bench "syntactic" $ nf evalDen (syntacticExpr 10)]
          , bgroup "Eval Tree 15"   [ bench "gadt"      $ nf evl (gadtExpr 15)
@@ -121,9 +120,9 @@
   evalSym EIf    = \c a b -> if c then a else b
 
 instance EvalEnv ExprS env where
-  compileSym p (EI n) = compileSymDefault p (EI n)
-  compileSym p (EB b) = compileSymDefault p (EB b)
-  compileSym p EAdd   = compileSymDefault p EAdd
-  compileSym p EEq    = compileSymDefault p EEq
-  compileSym p EIf    = compileSymDefault p EIf
+  compileSym p (EI n) = compileSymDefault signature p (EI n)
+  compileSym p (EB b) = compileSymDefault signature p (EB b)
+  compileSym p EAdd   = compileSymDefault signature p EAdd
+  compileSym p EEq    = compileSymDefault signature p EEq
+  compileSym p EIf    = compileSymDefault signature p EIf
 
diff --git a/benchmarks/WithArity.hs b/benchmarks/WithArity.hs
--- a/benchmarks/WithArity.hs
+++ b/benchmarks/WithArity.hs
@@ -3,13 +3,12 @@
 module WithArity (main) where
 
 import Criterion.Main
-import Criterion.Config
-import Data.Monoid
+import Criterion.Types
 import Data.Syntactic hiding (E)
 import Data.Syntactic.Functional
 
 main :: IO ()
-main = defaultMainWith (defaultConfig {cfgSummaryFile = Last $ Just "bench-results/withArity.csv"}) (return ())
+main = defaultMainWith (defaultConfig {csvFile = Just "bench-results/withArity.csv"})
          [ bgroup "eval 5"  [ bench "gadt"      $ nf evl (gExpr 5)
                             , bench "Syntactic" $ nf evalDen (sExpr 5) ]
          , bgroup "eval 6"  [ bench "gadt"      $ nf evl (gExpr 6)
@@ -118,10 +117,10 @@
 
 instance EvalEnv T env
   where
-    compileSym p (T0 a) = compileSymDefault p (T0 a)
-    compileSym p T1     = compileSymDefault p T1
-    compileSym p T2     = compileSymDefault p T2
-    compileSym p T3     = compileSymDefault p T3
-    compileSym p T5     = compileSymDefault p T5
-    compileSym p T10    = compileSymDefault p T10
+    compileSym p (T0 a) = compileSymDefault signature p (T0 a)
+    compileSym p T1     = compileSymDefault signature p T1
+    compileSym p T2     = compileSymDefault signature p T2
+    compileSym p T3     = compileSymDefault signature p T3
+    compileSym p T5     = compileSymDefault signature p T5
+    compileSym p T10    = compileSymDefault signature p T10
 
diff --git a/examples/Monad.hs b/examples/Monad.hs
--- a/examples/Monad.hs
+++ b/examples/Monad.hs
@@ -19,7 +19,7 @@
 
 import Data.Syntactic
 import Data.Syntactic.Functional
-import Data.Syntactic.Sugar.MonadT
+import Data.Syntactic.Sugar.MonadT ()
 
 import NanoFeldspar (Type, Arithmetic (..))
 
diff --git a/examples/NanoFeldspar.hs b/examples/NanoFeldspar.hs
--- a/examples/NanoFeldspar.hs
+++ b/examples/NanoFeldspar.hs
@@ -26,7 +26,7 @@
 import Data.Syntactic hiding (fold, printExpr, showAST, drawAST, writeHtmlAST)
 import qualified Data.Syntactic as Syntactic
 import Data.Syntactic.Functional
-import Data.Syntactic.Sugar.BindingT
+import Data.Syntactic.Sugar.BindingT ()
 
 
 
@@ -47,12 +47,18 @@
 -- * Abstract syntax
 --------------------------------------------------------------------------------
 
-data Arithmetic a
+data Arithmetic sig
   where
     Add :: (Type a, Num a) => Arithmetic (a :-> a :-> Full a)
     Sub :: (Type a, Num a) => Arithmetic (a :-> a :-> Full a)
     Mul :: (Type a, Num a) => Arithmetic (a :-> a :-> Full a)
 
+instance Symbol Arithmetic
+  where
+    symSig Add = signature
+    symSig Sub = signature
+    symSig Mul = signature
+
 instance Render Arithmetic
   where
     renderSym Add = "(+)"
@@ -69,17 +75,15 @@
     evalSym Mul = (*)
 
 instance EvalEnv Arithmetic env
-  where
-    compileSym p Add = compileSymDefault p Add
-    compileSym p Sub = compileSymDefault p Sub
-    compileSym p Mul = compileSymDefault p Mul
-      -- Pattern matching on the individual constructors is needed in order to fulfill the
-      -- 'Signature' constraint required by the right-hand side.
 
-data Let a
+data Let sig
   where
     Let :: Let (a :-> (a -> b) :-> Full b)
 
+instance Symbol Let
+  where
+    symSig Let = signature
+
 instance Equality Let
   where
     equal = equalDefault
@@ -100,13 +104,15 @@
     evalSym Let = flip ($)
 
 instance EvalEnv Let env
-  where
-    compileSym p Let = compileSymDefault p Let
 
-data Parallel a
+data Parallel sig
   where
     Parallel :: Type a => Parallel (Length :-> (Index -> a) :-> Full [a])
 
+instance Symbol Parallel
+  where
+    symSig Parallel = signature
+
 instance Render Parallel
   where
     renderSym Parallel = "parallel"
@@ -118,13 +124,15 @@
     evalSym Parallel = \len ixf -> Prelude.map ixf [0 .. len-1]
 
 instance EvalEnv Parallel env
-  where
-    compileSym p Parallel = compileSymDefault p Parallel
 
-data ForLoop a
+data ForLoop sig
   where
     ForLoop :: Type st => ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)
 
+instance Symbol ForLoop
+  where
+    symSig ForLoop = signature
+
 instance Render ForLoop
   where
     renderSym ForLoop = "forLoop"
@@ -136,8 +144,6 @@
     evalSym ForLoop = \len init body -> foldl (flip body) init [0 .. len-1]
 
 instance EvalEnv ForLoop env
-  where
-    compileSym p ForLoop = compileSymDefault p ForLoop
 
 type FeldDomain
     =   Arithmetic
diff --git a/examples/WellScoped.hs b/examples/WellScoped.hs
--- a/examples/WellScoped.hs
+++ b/examples/WellScoped.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 
 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
@@ -15,12 +16,10 @@
 
 
 
-import Data.Proxy
-
 import Data.Syntactic
 import Data.Syntactic.Functional
 
-import NanoFeldspar (Arithmetic (..), Let (..))
+import NanoFeldspar (Let (..))
 
 
 
@@ -28,9 +27,9 @@
 
 instance (Num a, Show a) => Num (Exp e a)
   where
-    fromInteger i = smartWS $ Construct (show i') i'
+    fromInteger i = smartWS (Construct (show i') i' :: Construct (Full a))
       where i' = fromInteger i
-    (+) = smartWS $ Construct "(+)" (+)
+    (+) = smartWS (Construct "(+)" (+) :: Construct (a :-> a :-> Full a))
 
 share :: forall e a b .
     Exp e a -> ((forall e' . Ext e' (a,e) => Exp e' a) -> Exp (a,e) b) -> Exp e b
diff --git a/extras/TypeUniverseClosed.hs b/extras/TypeUniverseClosed.hs
deleted file mode 100644
--- a/extras/TypeUniverseClosed.hs
+++ /dev/null
@@ -1,93 +0,0 @@
--- | Typed type reification, type-level reasoning and dynamic types
---
--- This module is meant as a reference for understanding the "Data.Syntactic.TypeUniverse" module.
-
-module TypeUniverseClosed where
-
-
-
-import Data.Constraint
-
-
-
--- | Typed representation of types (reification of type @a@)
-data TypeRep a
-  where
-    BoolType  :: TypeRep Bool
-    IntType   :: TypeRep Int
-    FloatType :: TypeRep Float
-    ListType  :: TypeRep a -> TypeRep [a]
-
--- | Type reification
-class Typeable a
-  where
-    -- | Reifies type @a@
-    typeRep :: TypeRep a
-
-instance Typeable Bool              where typeRep = BoolType
-instance Typeable Int               where typeRep = IntType
-instance Typeable Float             where typeRep = FloatType
-instance Typeable a => Typeable [a] where typeRep = ListType typeRep
-
-typeEq :: TypeRep a -> TypeRep b -> Maybe (Dict (a ~ b))
-typeEq BoolType      BoolType      = Just Dict
-typeEq IntType       IntType       = Just Dict
-typeEq FloatType     FloatType     = Just Dict
-typeEq (ListType t1) (ListType t2) = do Dict <- typeEq t1 t2; return Dict
-typeEq _ _ = Nothing
-
-hasTypeable :: TypeRep a -> Dict (Typeable a)
-hasTypeable BoolType  = Dict
-hasTypeable IntType   = Dict
-hasTypeable FloatType = Dict
-hasTypeable (ListType t) | Dict <- hasTypeable t = Dict
-
-hasEq :: TypeRep a -> Dict (Eq a)
-hasEq BoolType  = Dict
-hasEq IntType   = Dict
-hasEq FloatType = Dict
-hasEq (ListType t) | Dict <- hasEq t = Dict
-
-hasShow :: TypeRep a -> Dict (Show a)
-hasShow BoolType  = Dict
-hasShow IntType   = Dict
-hasShow FloatType = Dict
-hasShow (ListType t) | Dict <- hasShow t = Dict
-
-hasNum :: TypeRep a -> Maybe (Dict (Num a))
-hasNum BoolType     = Nothing
-hasNum IntType      = Just Dict
-hasNum FloatType    = Just Dict
-hasNum (ListType t) = Nothing
-
--- | Safe cast (does not use @unsafeCoerce@ underneath)
-cast :: forall a b . (Typeable a, Typeable b) => a -> Maybe b
-cast a = do
-    Dict <- typeEq (typeRep :: TypeRep a) (typeRep :: TypeRep b)
-    return a
-
-typeOf :: Typeable a => a -> TypeRep a
-typeOf _ = typeRep
-
-data Dynamic
-  where
-    Dyn :: TypeRep a -> a -> Dynamic
-
-toDyn :: Typeable a => a -> Dynamic
-toDyn = Dyn typeRep
-
-fromDyn :: Typeable a => Dynamic -> Maybe a
-fromDyn (Dyn t a) | Dict <- hasTypeable t = cast a
-
-instance Eq Dynamic
-  where
-    Dyn ta a == Dyn tb b
-        | Just Dict <- typeEq ta tb
-        , Dict      <- hasEq ta
-        = a == b
-    _ == _ = False
-
-instance Show Dynamic
-  where
-    show (Dyn t a) | Dict <- hasShow t = show a
-
diff --git a/src/Data/Syntactic/Decoration.hs b/src/Data/Syntactic/Decoration.hs
--- a/src/Data/Syntactic/Decoration.hs
+++ b/src/Data/Syntactic/Decoration.hs
@@ -32,6 +32,11 @@
            }
         -> (expr :&: info) sig
 
+instance Symbol sym => Symbol (sym :&: info)
+  where
+    rnfSym = rnfSym . decorExpr
+    symSig = symSig . decorExpr
+
 instance Project sub sup => Project sub (sup :&: info)
   where
     prj = prj . decorExpr
diff --git a/src/Data/Syntactic/Functional.hs b/src/Data/Syntactic/Functional.hs
--- a/src/Data/Syntactic/Functional.hs
+++ b/src/Data/Syntactic/Functional.hs
@@ -1,6 +1,16 @@
-{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE UndecidableInstances #-}
 
+#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
+
 -- | Basics for implementing functional EDSLs
 
 module Data.Syntactic.Functional
@@ -51,15 +61,16 @@
 
 
 
-import Control.Applicative
+import Control.Applicative  -- Needed by GHC < 7.10
+import Control.DeepSeq
 import Control.Monad.Cont
 import Control.Monad.Reader
 import Data.Dynamic
 import Data.List (genericIndex)
+import Data.Proxy  -- Needed by GHC < 7.8
 import Data.Tree
 
 import Data.Hash (hashInt)
-import Data.Proxy
 import Safe
 
 import Data.Syntactic
@@ -74,10 +85,15 @@
 --
 -- 'Construct' gives a quick way to introduce a syntactic construct by giving its name and semantic
 -- function.
-data Construct a
+data Construct sig
   where
     Construct :: Signature sig => String -> Denotation sig -> Construct sig
 
+instance Symbol Construct
+  where
+    rnfSym (Construct name den) = rnf name `seq` den `seq` ()
+    symSig (Construct _ _)      = signature
+
 instance Render Construct
   where
     renderSym (Construct name _) = name
@@ -92,18 +108,25 @@
 
 -- | Variable name
 newtype Name = Name Integer
-  deriving (Eq, Ord, Num, Enum, Real, Integral)
+  deriving (Eq, Ord, Num, Enum, Real, Integral, NFData)
 
 instance Show Name
   where
     show (Name n) = show n
 
 -- | Variables and binders
-data Binding a
+data Binding sig
   where
     Var :: Name -> Binding (Full a)
     Lam :: Name -> Binding (b :-> Full (a -> b))
 
+instance Symbol Binding
+  where
+    rnfSym (Var v) = rnf v
+    rnfSym (Lam v) = rnf v
+    symSig (Var _) = signature
+    symSig (Lam _) = signature
+
 -- | 'equal' does strict identifier comparison; i.e. no alpha equivalence.
 --
 -- 'hash' assigns the same hash to all variables and binders. This is a valid over-approximation
@@ -177,11 +200,18 @@
     go vs a = gmapT (go vs) a
 
 -- | Typed variables and binders
-data BindingT a
+data BindingT sig
   where
     VarT :: Typeable a => Name -> BindingT (Full a)
     LamT :: Typeable a => Name -> BindingT (b :-> Full (a -> b))
 
+instance Symbol BindingT
+  where
+    rnfSym (VarT v) = rnf v
+    rnfSym (LamT v) = rnf v
+    symSig (VarT _) = signature
+    symSig (LamT _) = signature
+
 -- | 'equal' does strict identifier comparison; i.e. no alpha equivalence.
 --
 -- 'hash' assigns the same hash to all variables and binders. This is a valid over-approximation
@@ -247,40 +277,41 @@
   -- `(Project Binding s, Project BindingT s)`. However, the problem is that one then has to
   -- specify the type `t` through a `Proxy`. The `BindingDomain` class gets around this problem.
 
-instance (BindingDomain sym1, BindingDomain sym2) => BindingDomain (sym1 :+: sym2)
+instance {-# OVERLAPPING #-}
+         (BindingDomain sym1, BindingDomain sym2) => BindingDomain (sym1 :+: sym2)
   where
     prVar (InjL s) = prVar s
     prVar (InjR s) = prVar s
     prLam (InjL s) = prLam s
     prLam (InjR s) = prLam s
 
-instance BindingDomain sym => BindingDomain (sym :&: i)
+instance {-# OVERLAPPING #-} BindingDomain sym => BindingDomain (sym :&: i)
   where
     prVar = prVar . decorExpr
     prLam = prLam . decorExpr
 
-instance BindingDomain sym => BindingDomain (AST sym)
+instance {-# OVERLAPPING #-} BindingDomain sym => BindingDomain (AST sym)
   where
     prVar (Sym s) = prVar s
     prVar _       = Nothing
     prLam (Sym s) = prLam s
     prLam _       = Nothing
 
-instance BindingDomain Binding
+instance {-# OVERLAPPING #-} BindingDomain Binding
   where
     prVar (Var v) = Just v
     prVar _       = Nothing
     prLam (Lam v) = Just v
     prLam _       = Nothing
 
-instance BindingDomain BindingT
+instance {-# OVERLAPPING #-} BindingDomain BindingT
   where
     prVar (VarT v) = Just v
     prVar _        = Nothing
     prLam (LamT v) = Just v
     prLam _        = Nothing
 
-instance BindingDomain sym
+instance {-# OVERLAPPING #-} BindingDomain sym
   where
     prVar _ = Nothing
     prLam _ = Nothing
@@ -294,6 +325,11 @@
     Return :: MONAD m (a :-> Full (m a))
     Bind   :: MONAD m (m a :-> (a -> m b) :-> Full (m b))
 
+instance Symbol (MONAD m)
+  where
+    symSig Return = signature
+    symSig Bind   = signature
+
 instance Render (MONAD m)
   where
     renderSym Return = "return"
@@ -348,9 +384,12 @@
 alphaEq' env var1 var2
     | Just v1 <- prVar var1
     , Just v2 <- prVar var2
-    = case lookup v1 env of
-        Nothing  -> v1==v2   -- Free variables
-        Just v2' -> v2==v2'
+    = case (lookup v1 env, lookup v2 env') of
+        (Nothing, Nothing)   -> v1==v2  -- Free variables
+        (Just v2', Just v1') -> v1==v1' && v2==v2'
+        _                    -> False
+  where
+    env' = [(v2,v1) | (v1,v2) <- env]
 alphaEq' env (lam1 :$ body1) (lam2 :$ body2)
     | Just v1 <- prLam lam1
     , Just v2 <- prLam lam2
@@ -436,12 +475,10 @@
 type instance DenotationM m (a :-> sig) = m a -> DenotationM m sig
 
 -- | Lift a 'Denotation' to 'DenotationM'
-liftDenotationM :: forall m sig proxy1 proxy2 . (Monad m, Signature sig) =>
-    proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig
-liftDenotationM _ _ = help2 sig . help1 sig
+liftDenotationM :: forall m sig proxy1 proxy2 . Monad m =>
+    SigRep sig -> proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig
+liftDenotationM sig _ _ = help2 sig . help1 sig
   where
-    sig = signature :: SigRep sig
-
     help1 :: Monad m =>
         SigRep sig' -> Denotation sig' -> Args (WrapFull m) sig' -> m (DenResult sig')
     help1 SigFull f _ = return f
@@ -460,8 +497,17 @@
 -- | Evaluation
 class EvalEnv sym env
   where
+    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'
+compileSymDefault :: forall proxy env sym sig . Eval sym =>
+    SigRep sig -> proxy env -> sym sig -> DenotationM (Reader env) sig
+compileSymDefault sig p s = liftDenotationM sig (Proxy :: Proxy (Reader env)) s (evalSym s)
+
 instance (EvalEnv sym1 env, EvalEnv sym2 env) => EvalEnv (sym1 :+: sym2) env
   where
     compileSym p (InjL s) = compileSym p s
@@ -477,16 +523,11 @@
 
 instance EvalEnv Construct env
   where
-    compileSym _ s@(Construct _ d :: Construct sig) = liftDenotationM p s d
+    compileSym _ s@(Construct _ d) = liftDenotationM signature p s d
       where
         p = Proxy :: Proxy (Reader env)
 
 instance Monad m => EvalEnv (MONAD m) env
-  where
-    compileSym p Return = compileSymDefault p Return
-    compileSym p Bind   = compileSymDefault p Bind
-      -- Pattern matching on the individual constructors is needed in order to fulfill the
-      -- 'Signature' constraint required by the right-hand side.
 
 instance EvalEnv BindingT RunEnv
   where
@@ -497,11 +538,6 @@
         msgType  = "compileSym: type error"  -- TODO Print types
     compileSym _ (LamT v) = \body -> reader $ \env a -> runReader body ((v, toDyn a) : env)
 
--- | Simple implementation of `compileSym` from a 'Denotation'
-compileSymDefault :: forall proxy env sym sig . (Eval sym, Signature sig) =>
-    proxy env -> sym sig -> DenotationM (Reader env) sig
-compileSymDefault p s = liftDenotationM (Proxy :: Proxy (Reader env)) s (evalSym s)
-
 -- | \"Compile\" a term to a Haskell function
 compile :: EvalEnv sym env => proxy env -> AST sym sig -> DenotationM (Reader env) sig
 compile p (Sym s)  = compileSym p s
@@ -533,19 +569,19 @@
     -- | Return the amount by which an environment has been extended
     diff :: Num a => Proxy ext -> Proxy orig -> a
 
-instance Ext env env
+instance {-# OVERLAPPING #-} Ext env env
   where
     unext = id
     diff _ _ = 0
 
-instance (Ext env e, ext ~ (a,env)) => Ext ext e
+instance {-# OVERLAPPING #-} (Ext env e, ext ~ (a,env)) => Ext ext e
   where
     unext = unext . snd
     diff m n = diff (fmap snd m) n + 1
 
 -- | Lookup in an extended environment
 lookEnv :: forall env a e . Ext env (a,e) => Proxy e -> Reader env a
-lookEnv _ = reader $ \env -> let (a, e :: e) = unext env in a
+lookEnv _ = reader $ \env -> let (a, _ :: e) = unext env in a
 
 -- | Well-scoped variable binding
 --
@@ -556,11 +592,18 @@
 -- \"Typing Dynamic Typing\" starts from an untyped term, and thus needs (safe) dynamic type casting
 -- during compilation. In contrast, the denotational semantics of 'BindingWS' (the 'Eval' instance)
 -- uses no type casting.
-data BindingWS a
+data BindingWS sig
   where
     VarWS :: Ext env (a,e) => Proxy e -> BindingWS (Full (Reader env a))
     LamWS :: BindingWS (Reader (a,e) b :-> Full (Reader e (a -> b)))
 
+instance Symbol BindingWS
+  where
+    rnfSym (VarWS Proxy) = ()
+    rnfSym LamWS         = ()
+    symSig (VarWS _)     = signature
+    symSig LamWS         = signature
+
 instance Eval BindingWS
   where
     evalSym (VarWS p) = lookEnv p
@@ -609,7 +652,7 @@
 type instance LowerReader (a :-> sig) = UnReader a :-> LowerReader sig
 
 -- | Wrap a symbol to give it a 'LiftReader' signature
-data ReaderSym sym a
+data ReaderSym sym sig
   where
     ReaderSym
         :: ( Signature sig
@@ -622,7 +665,7 @@
 
 instance Eval sym => Eval (ReaderSym sym)
   where
-    evalSym (ReaderSym (_ :: Proxy env) s) = liftDenotationM p s $ evalSym s
+    evalSym (ReaderSym (_ :: Proxy env) s) = liftDenotationM signature p s $ evalSym s
       where
         p = Proxy :: Proxy (Reader env)
 
diff --git a/src/Data/Syntactic/Sugar.hs b/src/Data/Syntactic/Sugar.hs
--- a/src/Data/Syntactic/Sugar.hs
+++ b/src/Data/Syntactic/Sugar.hs
@@ -1,6 +1,16 @@
-{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE UndecidableInstances #-}
 
+#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
+
 -- | \"Syntactic sugar\"
 --
 -- For details, see "Combining Deep and Shallow Embedding for EDSL"
@@ -60,12 +70,13 @@
     desugarN :: f -> internal
     sugarN   :: internal -> f
 
-instance (Syntactic f, Domain f ~ sym, fi ~ AST sym (Full (Internal f))) => SyntacticN f fi
+instance {-# OVERLAPPING #-}
+         (Syntactic f, Domain f ~ sym, fi ~ AST sym (Full (Internal f))) => SyntacticN f fi
   where
     desugarN = desugar
     sugarN   = sugar
 
-instance
+instance {-# OVERLAPPING #-}
     ( Syntactic a
     , Domain a ~ sym
     , ia ~ Internal a
diff --git a/src/Data/Syntactic/Syntax.hs b/src/Data/Syntactic/Syntax.hs
--- a/src/Data/Syntactic/Syntax.hs
+++ b/src/Data/Syntactic/Syntax.hs
@@ -1,6 +1,16 @@
-{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE UndecidableInstances #-}
 
+#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
+
 -- | Generic representation of typed syntax trees
 --
 -- For details, see: A Generic Abstract Syntax Model for Embedded Languages
@@ -12,11 +22,12 @@
     , ASTF
     , Full (..)
     , (:->) (..)
-    , size
-    , DenResult
-      -- Smart constructors
     , SigRep (..)
     , Signature (..)
+    , DenResult
+    , Symbol (..)
+    , size
+      -- Smart constructors
     , SmartFun
     , SmartSig
     , SmartSym
@@ -41,11 +52,12 @@
 
 
 
-import Data.Foldable (Foldable)
-import Data.Traversable (Traversable)
+import Control.DeepSeq
 import Data.Typeable
+import Data.Foldable (Foldable)        -- Needed by GHC < 7.10
+import Data.Proxy                      -- Needed by GHC < 7.8
+import Data.Traversable (Traversable)  -- Needed by GHC < 7.10
 
-import Data.Proxy
 
 
 
@@ -83,29 +95,13 @@
 
 infixr :->
 
--- | Count the number of symbols in an 'AST'
-size :: AST sym sig -> Int
-size (Sym _)  = 1
-size (s :$ a) = size s + size a
-
--- | The result type of a symbol with the given signature
-type family   DenResult sig
-type instance DenResult (Full a)    = a
-type instance DenResult (a :-> sig) = DenResult sig
-
-
-
---------------------------------------------------------------------------------
--- * Smart constructors
---------------------------------------------------------------------------------
-
 -- | Witness of the arity of a symbol signature
 data SigRep sig
   where
     SigFull :: SigRep (Full a)
     SigMore :: SigRep sig -> SigRep (a :-> sig)
 
--- | Symbol signatures
+-- | Valid symbol signatures
 class Signature sig
   where
     signature :: SigRep sig
@@ -118,6 +114,37 @@
   where
     signature = SigMore signature
 
+-- | The result type of a symbol with the given signature
+type family   DenResult sig
+type instance DenResult (Full a)    = a
+type instance DenResult (a :-> sig) = DenResult sig
+
+-- | Valid symbols to use in an 'AST'
+class Symbol sym
+  where
+    -- | Force a symbol to normal form
+    rnfSym :: sym sig -> ()
+    rnfSym s = s `seq` ()
+
+    -- | Reify the signature of a symbol
+    symSig :: sym sig -> SigRep sig
+
+instance Symbol sym => NFData (AST sym sig)
+  where
+    rnf (Sym s)  = rnfSym s
+    rnf (s :$ a) = rnf s `seq` rnf a
+
+-- | Count the number of symbols in an 'AST'
+size :: AST sym sig -> Int
+size (Sym _)  = 1
+size (s :$ a) = size s + size a
+
+
+
+--------------------------------------------------------------------------------
+-- * Smart constructors
+--------------------------------------------------------------------------------
+
 -- | Maps a symbol signature to the type of the corresponding smart constructor:
 --
 -- > SmartFun sym (a :-> b :-> ... :-> Full x) = ASTF sym a -> ASTF sym b -> ... -> ASTF sym x
@@ -162,7 +189,7 @@
 --------------------------------------------------------------------------------
 
 -- | Direct sum of two symbol domains
-data (sym1 :+: sym2) a
+data (sym1 :+: sym2) sig
   where
     InjL :: sym1 a -> (sym1 :+: sym2) a
     InjR :: sym2 a -> (sym1 :+: sym2) a
@@ -170,6 +197,13 @@
 
 infixr :+:
 
+instance (Symbol sym1, Symbol sym2) => Symbol (sym1 :+: sym2)
+  where
+    rnfSym (InjL s) = rnfSym s
+    rnfSym (InjR s) = rnfSym s
+    symSig (InjL s) = symSig s
+    symSig (InjR s) = symSig s
+
 -- | Symbol projection
 --
 -- The class is defined for /all pairs of types/, but 'prj' can only succeed if @sup@ is of the form
@@ -179,21 +213,21 @@
     -- | Partial projection from @sup@ to @sub@
     prj :: sup a -> Maybe (sub a)
 
-instance Project sub sup => Project sub (AST sup)
+instance {-# OVERLAPPING #-} Project sub sup => Project sub (AST sup)
   where
     prj (Sym s) = prj s
     prj _       = Nothing
 
-instance Project sym sym
+instance {-# OVERLAPPING #-} Project sym sym
   where
     prj = Just
 
-instance Project sym1 (sym1 :+: sym2)
+instance {-# OVERLAPPING #-} Project sym1 (sym1 :+: sym2)
   where
     prj (InjL a) = Just a
     prj _        = Nothing
 
-instance Project sym1 sym3 => Project sym1 (sym2 :+: sym3)
+instance {-# OVERLAPPING #-} Project sym1 sym3 => Project sym1 (sym2 :+: sym3)
   where
     prj (InjR a) = prj a
     prj _        = Nothing
@@ -211,19 +245,19 @@
     -- | Injection from @sub@ to @sup@
     inj :: sub a -> sup a
 
-instance (sub :<: sup) => (sub :<: AST sup)
+instance {-# OVERLAPPING #-} (sub :<: sup) => (sub :<: AST sup)
   where
     inj = Sym . inj
 
-instance (sym :<: sym)
+instance {-# OVERLAPPING #-} (sym :<: sym)
   where
     inj = id
 
-instance (sym1 :<: (sym1 :+: sym2))
+instance {-# OVERLAPPING #-} (sym1 :<: (sym1 :+: sym2))
   where
     inj = InjL
 
-instance (sym1 :<: sym3) => (sym1 :<: (sym2 :+: sym3))
+instance {-# OVERLAPPING #-} (sym1 :<: sym3) => (sym1 :<: (sym2 :+: sym3))
   where
     inj = InjR . inj
 
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        2.0
+Version:        2.1
 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
@@ -15,7 +15,7 @@
                   * Slides:
                     <http://www.cse.chalmers.se/~emax/documents/axelsson2012generic-slides.pdf>
                 .
-                Example EDSL can be found in the @examples@ folder.
+                Example EDSLs can be found in the @examples@ folder.
                 .
                 \[1\] W. Swierstra. Data Types à la Carte.
                 /Journal of Functional Programming/, 18(4):423-436, 2008,
@@ -31,14 +31,12 @@
 Category:       Language
 Build-type:     Simple
 Cabal-version:  >=1.16
-Tested-with:    GHC==7.6.2, GHC==7.8.2
 
 extra-source-files:
   CONTRIBUTORS
   examples/*.hs
   tests/*.hs
   tests/gold/*.txt
-  extras/*.hs
   benchmarks/*.hs
 
 source-repository head
@@ -64,6 +62,7 @@
     containers,
     constraints,
     data-hash,
+    deepseq,
     mtl >= 2 && < 3,
     safe,
     tagged,
@@ -75,6 +74,7 @@
   default-language: Haskell2010
 
   default-extensions:
+    DefaultSignatures
     DeriveDataTypeable
     DeriveFunctor
     DeriveFoldable
@@ -137,7 +137,8 @@
 
   build-depends:
     base,
-    criterion,
+    criterion >= 1,
+    deepseq,
     syntactic
 
   default-language: Haskell2010
diff --git a/tests/MonadTests.hs b/tests/MonadTests.hs
--- a/tests/MonadTests.hs
+++ b/tests/MonadTests.hs
@@ -12,7 +12,6 @@
 import Data.ByteString.Lazy.UTF8 (fromString)
 
 import Data.Syntactic
-import Data.Syntactic.Functional
 import qualified Monad