diff --git a/examples/Monad.hs b/examples/Monad.hs
--- a/examples/Monad.hs
+++ b/examples/Monad.hs
@@ -3,7 +3,8 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeOperators #-}
 
-{-# OPTIONS_GHC -fno-warn-missing-methods #-}
+{-# OPTIONS_GHC -Wno-missing-methods #-}
+{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
 
 -- | This module demonstrates monad reification.
 -- See \"Generic Monadic Constructs for Embedded Languages\" (Persson et al., IFL 2011
diff --git a/examples/NanoFeldsparComp.hs b/examples/NanoFeldsparComp.hs
--- a/examples/NanoFeldsparComp.hs
+++ b/examples/NanoFeldsparComp.hs
@@ -99,7 +99,7 @@
 
 compileExp :: ASTF Dom a -> CodeGen Exp
 compileExp var
-    | Just (Var v) <- prj var = return (varNameE v)
+    | Just (VarT v) <- prj var = return (varNameE v)
 compileExp (lett :$ a :$ (lam :$ body))
     | Just (Let _)  <- prj lett
     , Just (LamT v) <- prj lam
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
@@ -51,9 +51,9 @@
 
 instance (NFData1 sym, NFData1 info) => NFData1 (sym :&: info)
   where
-    liftRnf r (s :&: i) = liftRnf r s `seq` liftRnf (`seq` ()) i
+    rnf1 (s :&: i) = rnf1 s `seq` rnf1 i `seq` ()
 
-instance {-# OVERLAPPING #-} Project sub sup => Project sub (sup :&: info)
+instance 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
@@ -68,7 +68,7 @@
 #else
 import Control.Applicative
 #endif
-import Control.DeepSeq
+import Control.DeepSeq (NFData (..))
 import Control.Monad.Cont
 import Control.Monad.Reader
 import Control.Monad.State
@@ -87,9 +87,9 @@
 
 
 
---------------------------------------------------------------------------------
+----------------------------------------------------------------------------------------------------
 -- * Syntactic constructs
---------------------------------------------------------------------------------
+----------------------------------------------------------------------------------------------------
 
 -- | Literal
 data Literal sig
@@ -155,8 +155,8 @@
 
 instance NFData1 Binding
   where
-    liftRnf _ (Var v) = rnf v
-    liftRnf _ (Lam v) = rnf v
+    rnf1 (Var v) = rnf v
+    rnf1 (Lam v) = rnf v
 
 -- | 'equal' does strict identifier comparison; i.e. no alpha equivalence.
 --
@@ -255,8 +255,8 @@
 
 instance NFData1 BindingT
   where
-    liftRnf _ (VarT v) = rnf v
-    liftRnf _ (LamT v) = rnf v
+    rnf1 (VarT v) = rnf v
+    rnf1 (LamT v) = rnf v
 
 -- | 'equal' does strict identifier comparison; i.e. no alpha equivalence.
 --
@@ -390,11 +390,15 @@
     renameBind re (VarT v) = VarT $ re v
     renameBind re (LamT v) = LamT $ re v
 
-instance {-# OVERLAPPING #-} BindingDomain sym
+instance {-# OVERLAPPABLE #-} BindingDomain sym
   where
     prVar _ = Nothing
     prLam _ = Nothing
     renameBind _ a = a
+  -- This instance seems to overlap all others on GHC 8.2.2. This leads to
+  -- failures in the test suite. Removing the instance and declaring one
+  -- instance per type solves the problem. Earlier and later GHC versions don't
+  -- have this problem, so I assume it's a bug in 8.2.
 
 -- | A symbol for let bindings
 --
@@ -546,9 +550,11 @@
 
 freshVar :: MonadState [Name] m => m Name
 freshVar = do
-    v:vs <- get
-    put vs
-    return v
+    vs <- get
+    case vs of
+      v:vs' -> do
+        put vs'
+        return v
 
 -- | Rename the bound variables in a term
 --
@@ -585,9 +591,9 @@
 
 
 
---------------------------------------------------------------------------------
+----------------------------------------------------------------------------------------------------
 -- * Alpha-equivalence
---------------------------------------------------------------------------------
+----------------------------------------------------------------------------------------------------
 
 -- | Environment used by 'alphaEq''
 type AlphaEnv = [(Name,Name)]
@@ -632,9 +638,9 @@
 
 
 
---------------------------------------------------------------------------------
+----------------------------------------------------------------------------------------------------
 -- * Evaluation
---------------------------------------------------------------------------------
+----------------------------------------------------------------------------------------------------
 
 -- | Semantic function type of the given symbol signature
 type family   Denotation sig
diff --git a/src/Language/Syntactic/Functional/WellScoped.hs b/src/Language/Syntactic/Functional/WellScoped.hs
--- a/src/Language/Syntactic/Functional/WellScoped.hs
+++ b/src/Language/Syntactic/Functional/WellScoped.hs
@@ -33,12 +33,12 @@
     -- | Return the amount by which an environment has been extended
     diff :: Num a => Proxy ext -> Proxy orig -> a
 
-instance {-# OVERLAPPING #-} Ext env env
+instance {-# OVERLAPS #-} Ext env env
   where
     unext = id
     diff _ _ = 0
 
-instance {-# OVERLAPPING #-} (Ext env e, ext ~ (a,env)) => Ext ext e
+instance {-# OVERLAPS #-} (Ext env e, ext ~ (a,env)) => Ext ext e
   where
     unext = unext . snd
     diff m n = diff (fmap snd m) n + 1
@@ -68,8 +68,8 @@
 
 instance NFData1 BindingWS
   where
-    liftRnf _ (VarWS Proxy) = ()
-    liftRnf _ LamWS         = ()
+    rnf1 (VarWS Proxy) = ()
+    rnf1 LamWS         = ()
 
 instance Eval BindingWS
   where
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
@@ -79,13 +79,13 @@
     desugarN :: f -> internal
     sugarN   :: internal -> f
 
-instance {-# OVERLAPPING #-}
+instance {-# OVERLAPS #-}
          (Syntactic f, Domain f ~ sym, fi ~ AST sym (Full (Internal f))) => SyntacticN f fi
   where
     desugarN = desugar
     sugarN   = sugar
 
-instance {-# OVERLAPPING #-}
+instance {-# OVERLAPS #-}
     ( Syntactic a
     , Domain a ~ sym
     , ia ~ Internal a
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
@@ -59,7 +59,7 @@
 
 
 
-import Control.DeepSeq
+import Control.DeepSeq (NFData (..))
 import Data.Typeable
 #if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0)
 #else
@@ -142,7 +142,7 @@
 
 instance NFData1 sym => NFData (AST sym sig)
   where
-    rnf (Sym s)  = liftRnf (`seq` ()) s
+    rnf (Sym s)  = rnf1 s
     rnf (s :$ a) = rnf s `seq` rnf a
 
 -- | Count the number of symbols in an 'AST'
@@ -215,8 +215,8 @@
 
 instance (NFData1 sym1, NFData1 sym2) => NFData1 (sym1 :+: sym2)
   where
-    liftRnf r (InjL s) = liftRnf r s
-    liftRnf r (InjR s) = liftRnf r s
+    rnf1 (InjL s) = rnf1 s
+    rnf1 (InjR s) = rnf1 s
 
 -- | Symbol projection
 --
@@ -227,29 +227,25 @@
     -- | Partial projection from @sup@ to @sub@
     prj :: sup a -> Maybe (sub a)
 
-instance {-# OVERLAPPING #-} Project sub sup => Project sub (AST sup)
+instance Project sub sup => Project sub (AST sup)
   where
     prj (Sym s) = prj s
     prj _       = Nothing
 
-instance {-# OVERLAPPING #-} Project sym sym
+instance {-# OVERLAPS #-} Project sym sym
   where
     prj = Just
 
-instance {-# OVERLAPPING #-} Project sym1 (sym1 :+: sym2)
+instance {-# OVERLAPS #-} Project sym1 (sym1 :+: sym2)
   where
     prj (InjL a) = Just a
     prj _        = Nothing
 
-instance {-# OVERLAPPING #-} Project sym1 sym3 => Project sym1 (sym2 :+: sym3)
+instance {-# OVERLAPS #-} Project sym1 sym3 => Project sym1 (sym2 :+: sym3)
   where
     prj (InjR a) = prj a
     prj _        = Nothing
 
--- | If @sub@ is not in @sup@, 'prj' always returns 'Nothing'.
-instance Project sub sup
-  where
-    prj _ = Nothing
 
 -- | Symbol injection
 --
@@ -259,19 +255,19 @@
     -- | Injection from @sub@ to @sup@
     inj :: sub a -> sup a
 
-instance {-# OVERLAPPING #-} (sub :<: sup) => (sub :<: AST sup)
+instance {-# OVERLAPS #-} (sub :<: sup) => (sub :<: AST sup)
   where
     inj = Sym . inj
 
-instance {-# OVERLAPPING #-} (sym :<: sym)
+instance {-# OVERLAPS #-} (sym :<: sym)
   where
     inj = id
 
-instance {-# OVERLAPPING #-} (sym1 :<: (sym1 :+: sym2))
+instance {-# OVERLAPS #-} (sym1 :<: (sym1 :+: sym2))
   where
     inj = InjL
 
-instance {-# OVERLAPPING #-} (sym1 :<: sym3) => (sym1 :<: (sym2 :+: sym3))
+instance {-# OVERLAPS #-} (sym1 :<: sym3) => (sym1 :<: (sym2 :+: sym3))
   where
     inj = InjR . inj
 
@@ -359,7 +355,7 @@
   where
     Typed :: Typeable (DenResult sig) => sym sig -> Typed sym sig
 
-instance {-# OVERLAPPING #-} Project sub sup => Project sub (Typed sup)
+instance Project sub sup => Project sub (Typed sup)
   where
     prj (Typed s) = prj s
 
@@ -397,6 +393,13 @@
 --------------------------------------------------------------------------------
 -- * Misc.
 --------------------------------------------------------------------------------
+
+-- | Higher-kinded version of 'NFData'
+class NFData1 c
+  where
+    -- | Force a symbol to normal form
+    rnf1 :: c a -> ()
+    rnf1 s = s `seq` ()
 
 -- | Constrain a symbol to a specific type
 symType :: Proxy sym -> sym sig -> sym sig
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,10 +1,13 @@
 Name:           syntactic
-Version:        3.7.1
+Version:        3.8
 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
                 trees based on the technique in Data Types à la Carte [1].
                 .
+                This package does not work on GHC version 8.2, but works on many
+                earlier and later versions.
+                .
                 (Note that the difference between version 2.x and 3.0 is not that big. The bump to
                 3.0 was done because the modules changed namespace.)
                 .
@@ -77,15 +80,21 @@
       Language.Syntactic.Sugar.TupleTyped
 
   build-depends:
-    base >= 4.6 && < 5,
-    constraints,
-    containers,
-    data-hash,
-    deepseq >= 1.4.3.0,
-    mtl >= 2 && < 3,
-    syb,
-    tree-view >= 0.5
+    base >= 4.6 && < 4.13,
+    constraints < 0.11,
+    containers < 0.7,
+    data-hash < 0.3,
+    deepseq < 1.5,
+    mtl >= 2 && < 2.3,
+    syb < 0.8,
+    tree-view >= 0.5 && < 0.6
 
+  if impl(ghc == 8.2.*)
+    build-depends: base<0
+    -- See the note to the catch-all instance of `BindingDomain`. Since this can
+    -- lead to subtle errors and non-termination in user code, we prefer not to
+    -- support GHC 8.2.
+
   if impl(ghc < 7.10)
     build-depends: base-orphans
 
@@ -127,6 +136,17 @@
 
   main-is: Tests.hs
 
+  other-modules: AlgorithmTests
+                 Monad
+                 MonadTests
+                 NanoFeldspar
+                 NanoFeldsparComp
+                 NanoFeldsparTests
+                 SyntaxTests
+                 TH
+                 WellScoped
+                 WellScopedTests
+
   default-language: Haskell2010
 
   build-depends:
@@ -137,6 +157,7 @@
     QuickCheck,
     tagged,
     tasty,
+    tasty-hunit,
     tasty-golden,
     tasty-quickcheck,
     tasty-th,
@@ -148,6 +169,10 @@
   hs-source-dirs: benchmarks
 
   main-is: MainBenchmark.hs
+
+  other-modules: JoiningTypes
+                 Normal
+                 WithArity
 
   build-depends:
     base,
diff --git a/tests/SyntaxTests.hs b/tests/SyntaxTests.hs
new file mode 100644
--- /dev/null
+++ b/tests/SyntaxTests.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+module SyntaxTests where
+
+import Data.Maybe
+import Language.Syntactic
+import Language.Syntactic.TH
+import Test.Tasty
+import Test.Tasty.HUnit
+
+data A sig
+  where
+    A1 :: Int -> A (Full Int)
+    A2 :: A (Int :-> Full Int)
+
+deriving instance Eq (A sig)
+deriving instance Show (A sig)
+
+data B sig
+  where
+    B1 :: Char -> B (Full Char)
+
+deriving instance Eq (B sig)
+deriving instance Show (B sig)
+
+data C sig
+  where
+    C1 :: C (Full ())
+    C2 :: C (Int :-> Int :-> Full Int)
+
+deriving instance Eq (C sig)
+deriving instance Show (C sig)
+
+type Dom = A :+: B :+: C
+
+type Exp a = ASTF Dom a
+
+a1 :: Int -> Exp Int
+a1 = inj . A1
+
+a2 :: Exp Int -> Exp Int
+a2 a = inj A2 :$ a
+
+b1 :: Char -> Exp Char
+b1 = inj . B1
+
+c1 :: Exp ()
+c1 = inj $ C1
+
+c2 :: Exp Int -> Exp Int -> Exp Int
+c2 a b = inj C2 :$ a :$ b
+
+tests = testGroup "SyntaxTests"
+  [
+    testCase "project first domain entry 1" $ prj (a1 5)      @?= Just (A1 5)
+  , testCase "project first domain entry 2" $ prj (a2 (a1 1)) @?= (Nothing :: Maybe (A (Full Int)))
+  , testCase "project second domain entry"  $ prj (b1 'b')    @?= Just (B1 'b')
+  , testCase "project third domain entry 1" $ prj (c1)        @?= Just C1
+  , testCase "project third domain entry 2" $ prj (c2 (a1 3) (a2 (a1 9))) @?= (Nothing :: Maybe (C (Full Int)))
+  ]
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -4,10 +4,12 @@
 import qualified NanoFeldsparTests
 import qualified WellScopedTests
 import qualified MonadTests
+import qualified SyntaxTests
 import qualified TH
 
 tests = testGroup "AllTests"
-    [ AlgorithmTests.tests
+    [ SyntaxTests.tests
+    , AlgorithmTests.tests
     , NanoFeldsparTests.tests
     , WellScopedTests.tests
     , MonadTests.tests