diff --git a/ivory.cabal b/ivory.cabal
--- a/ivory.cabal
+++ b/ivory.cabal
@@ -2,7 +2,7 @@
 --  see http://haskell.org/cabal/users-guide/
 
 name:                ivory
-version:             0.1.0.6
+version:             0.1.0.7
 author:              Galois, Inc.
 maintainer:          trevor@galois.com, leepike@galois.com
 category:            Language
@@ -87,7 +87,8 @@
                         pretty >= 1.1,
                         containers >= 0.5,
                         monadLib >= 3.7,
-                        template-haskell >= 2.8,
+                        template-haskell >= 2.8 && <2.13,
+                        th-abstraction >=0.2.5 && <0.3,
                         filepath,
                         text,
                         dlist >= 0.5,
diff --git a/src/Ivory/Language/Proxy.hs b/src/Ivory/Language/Proxy.hs
--- a/src/Ivory/Language/Proxy.hs
+++ b/src/Ivory/Language/Proxy.hs
@@ -1,19 +1,32 @@
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE ConstraintKinds #-}
-
-module Ivory.Language.Proxy where
+{-# LANGUAGE PolyKinds #-}
 
-import GHC.TypeLits (natVal, symbolVal, Symbol, Nat, KnownNat, KnownSymbol)
+module Ivory.Language.Proxy
+  (
+  -- * Proxy
+    Proxy(..)
+  , SProxy
+  -- * Nat
+  , ANat
+  , NatType
+  , aNat
+  , fromTypeNat
+  -- * Symbol
+  , ASymbol
+  , SymbolType
+  , aSymbol
+  , fromTypeSym
+  ) where
 
-data Proxy (a :: k) = Proxy
+import Data.Proxy   (Proxy (..))
+import GHC.TypeLits (KnownNat, KnownSymbol, Nat, Symbol, natVal, symbolVal)
 
 -- | Type proxies for * types.
 type SProxy a = Proxy (a :: *)
 
-type ANat    n = (KnownNat n)
+type ANat    n = KnownNat n
 type NatType n = Proxy n
 aNat :: KnownNat n => Proxy n
 aNat = Proxy
diff --git a/src/Ivory/Language/Syntax/Concrete/QQ/BitDataQQ.hs b/src/Ivory/Language/Syntax/Concrete/QQ/BitDataQQ.hs
--- a/src/Ivory/Language/Syntax/Concrete/QQ/BitDataQQ.hs
+++ b/src/Ivory/Language/Syntax/Concrete/QQ/BitDataQQ.hs
@@ -25,6 +25,7 @@
 
 import           Language.Haskell.TH                      hiding (Exp, Type)
 import qualified Language.Haskell.TH                      as TH
+import           Language.Haskell.TH.Datatype
 
 import qualified Ivory.Language.Bits                      as I
 import qualified Ivory.Language.Cast                      as I
@@ -37,9 +38,7 @@
 import qualified Ivory.Language.BitData.Array             as B
 import qualified Ivory.Language.BitData.BitData           as B
 import qualified Ivory.Language.BitData.Bits              as B
-#if __GLASGOW_HASKELL__ >= 709
 import           Ivory.Language.Syntax.Concrete.QQ.Common
-#endif
 import           Ivory.Language.Syntax.Concrete.Location
 import           Ivory.Language.Syntax.Concrete.QQ.TypeQQ
 
@@ -325,33 +324,23 @@
     , concatMap (mkConstr def) (thDefConstrs def)
     , mkArraySizeTypeInsts def
     ]
-#if __GLASGOW_HASKELL__ >= 709
   ln <- lnPragma (bdLoc d)
   return (ln ++ defs)
-#else
-  return defs
-#endif
 
 -- | Generate a newtype definition for a bit data definition.
 mkDefNewtype :: THDef -> [DecQ]
 mkDefNewtype def =
-#if __GLASGOW_HASKELL__ >= 800
-  [newtypeD (cxt []) name []
-   Nothing
-   (normalC name
-    [bangType (bang noSourceUnpackedness noSourceStrictness) (return ty)])
-   (mapM conT
+  [newtypeDCompat (cxt []) name [] (normalC name [field])
     [ ''I.IvoryType, ''I.IvoryVar, ''I.IvoryExpr , ''I.IvoryEq
-    , ''I.IvoryInit, ''I.IvoryStore, ''I.IvoryZeroVal ])]
-#else
-  [newtypeD (cxt []) name []
-   (normalC name [strictType notStrict (return ty)])
-   [ ''I.IvoryType, ''I.IvoryVar, ''I.IvoryExpr , ''I.IvoryEq
-   , ''I.IvoryInit, ''I.IvoryStore, ''I.IvoryZeroVal ]]
-#endif
+    , ''I.IvoryInit, ''I.IvoryStore, ''I.IvoryZeroVal ]]
   where
     name = thDefName def
     ty   = thDefType def
+#if __GLASGOW_HASKELL__ >= 800
+    field = bangType (bang noSourceUnpackedness noSourceStrictness) (return ty)
+#else
+    field = strictType notStrict (return ty)
+#endif
 
 -- | Generate an instance of the "BitData" type class for a bit data
 -- definition.
@@ -362,11 +351,7 @@
     baseTy  = thDefType def
     instTy  = [t| B.BitData $(conT (thDefName def)) |]
     body    = [tyDef, toFun, fromFun]
-#if __GLASGOW_HASKELL__ >= 708
-    tyDef   = return (TySynInstD ''B.BitType (TySynEqn [ConT name] baseTy))
-#else
-    tyDef   = return (TySynInstD ''B.BitType [ConT name] baseTy)
-#endif
+    tyDef   = tySynInstDCompat ''B.BitType [conT name] (return baseTy)
     x       = mkName "x"
     toFun   = funD 'B.toBits [clause [conP name [varP x]]
                               (normalB (varE x)) []]
@@ -393,11 +378,7 @@
 -- result type is the same.
 mkArraySizeTypeInst :: Integer -> TH.Type -> [DecQ]
 mkArraySizeTypeInst n ty =
-#if __GLASGOW_HASKELL__ >= 708
-  [tySynInstD ''B.ArraySize (tySynEqn args size)]
-#else
-  [tySynInstD ''B.ArraySize args size]
-#endif
+  [tySynInstDCompat ''B.ArraySize args size]
   where
     size = tyBits ty >>= litT . numTyLit . fromIntegral . (* n)
     args = [litT (numTyLit (fromIntegral n)), return ty]
diff --git a/src/Ivory/Language/Syntax/Concrete/QQ/Common.hs b/src/Ivory/Language/Syntax/Concrete/QQ/Common.hs
--- a/src/Ivory/Language/Syntax/Concrete/QQ/Common.hs
+++ b/src/Ivory/Language/Syntax/Concrete/QQ/Common.hs
@@ -41,6 +41,7 @@
 import Prelude.Compat hiding (exp)
 
 import           Language.Haskell.TH       hiding (Stmt, Exp, Type)
+import           Language.Haskell.TH.Datatype (pragLineDCompat)
 import qualified Language.Haskell.TH as T
 
 import           Data.List  (nub)
@@ -193,13 +194,11 @@
 
 --------------------------------------------------------------------------------
 
-#if __GLASGOW_HASKELL__ >= 709
 lnPragma :: SrcLoc -> Q [Dec]
 lnPragma srcloc =
   case srcLoclinePragma srcloc of
     Nothing         -> return []
-    Just (ln, file) -> (:[]) `fmap` pragLineD ln file
-#else
-lnPragma :: SrcLoc -> Q [Dec]
-lnPragma _srcloc = return []
-#endif
+    Just (ln, file) ->
+      case pragLineDCompat ln file of
+        Nothing -> return []
+        Just p  -> (:[]) `fmap` p
