diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,29 @@
 `th-desugar` release notes
 ==========================
 
+Version 1.8
+-----------
+* Support GHC 8.4.
+
+* `substTy` now properly substitutes into kind signatures.
+
+* Expose `fvDType`, which computes the free variables of a `DType`.
+
+* Incorporate a `DDeclaredInfix` field into `DNormalC` to indicate if it is
+  a constructor that was declared infix.
+
+* Implement `lookupValueNameWithLocals`, `lookupTypeNameWithLocals`,
+  `mkDataNameWithLocals`, and `mkTypeNameWithLocals`, counterparts to
+  `lookupValueName`, `lookupTypeName`, `mkDataName`, and `mkTypeName` which
+  have access to local Template Haskell declarations.
+
+* Implement `reifyNameSpace` to determine a `Name`'s `NameSpace`.
+
+* Export `reifyFixityWithLocals` from `Language.Haskell.TH.Desugar`.
+
+* Export `matchTy` (among other goodies) from new module `Language.Haskell.TH.Subst`.
+  This function matches a type template against a target.
+
 Version 1.7
 -----------
 * Support for TH's support for `TypeApplications`, thanks to @RyanGlScott.
diff --git a/Language/Haskell/TH/Desugar.hs b/Language/Haskell/TH/Desugar.hs
--- a/Language/Haskell/TH/Desugar.hs
+++ b/Language/Haskell/TH/Desugar.hs
@@ -28,7 +28,7 @@
   DDerivClause(..), DerivStrategy(..), DPatSynDir(..), DPatSynType,
   Overlap(..), PatSynArgs(..), NewOrData(..),
   DTypeFamilyHead(..), DFamilyResultSig(..), InjectivityAnn(..),
-  DCon(..), DConFields(..), DBangType, DVarBangType,
+  DCon(..), DConFields(..), DDeclaredInfix, DBangType, DVarBangType,
   Bang(..), SourceUnpackedness(..), SourceStrictness(..),
   DForeign(..),
   DPragma(..), DRuleBndr(..), DTySynEqn(..), DInfo(..), DInstanceDec,
@@ -65,12 +65,19 @@
 
   -- | The following definitions allow you to register a list of
   -- @Dec@s to be used in reification queries.
-  withLocalDeclarations, dsReify, reifyWithLocals_maybe, reifyWithLocals,
+  withLocalDeclarations, dsReify,
+  reifyWithLocals_maybe, reifyWithLocals, reifyFixityWithLocals,
+  lookupValueNameWithLocals, lookupTypeNameWithLocals,
+  mkDataNameWithLocals, mkTypeNameWithLocals,
+  reifyNameSpace,
   DsMonad(..), DsM,
 
   -- * Nested pattern flattening
   scExp, scLetDec,
 
+  -- * Capture-avoiding substitution and utilities
+  module Language.Haskell.TH.Desugar.Subst,
+
   -- * Utility functions
   applyDExp, applyDType,
   dPatToDExp, removeWilds,
@@ -78,7 +85,7 @@
   nameOccursIn, allNamesIn, flattenDValD, getRecordSelectors,
   mkTypeName, mkDataName, newUniqueName,
   mkTupleDExp, mkTupleDPat, maybeDLetE, maybeDCaseE,
-  substTy,
+  fvDType,
   tupleDegree_maybe, tupleNameDegree_maybe,
   unboxedSumDegree_maybe, unboxedSumNameDegree_maybe,
   unboxedTupleDegree_maybe, unboxedTupleNameDegree_maybe,
@@ -95,8 +102,10 @@
 import Language.Haskell.TH.Desugar.Reify
 import Language.Haskell.TH.Desugar.Expand
 import Language.Haskell.TH.Desugar.Match
+import Language.Haskell.TH.Desugar.Subst
 
 import qualified Data.Map as M
+import Data.Monoid
 import qualified Data.Set as S
 #if __GLASGOW_HASKELL__ < 709
 import Data.Foldable ( foldMap )
@@ -172,17 +181,29 @@
 flattenDValD other_dec = return [other_dec]
 
 fvDType :: DType -> S.Set Name
-fvDType = go
+fvDType = go_ty
   where
-    go (DForallT tvbs _cxt ty) = go ty `S.difference` (foldMap dtvbName tvbs)
-    go (DAppT ty1 ty2)         = go ty1 `S.union` go ty2
-    go (DSigT ty ki)           = go ty `S.union` fvDType ki
-    go (DVarT n)               = S.singleton n
-    go (DConT _)               = S.empty
-    go DArrowT                 = S.empty
-    go (DLitT {})              = S.empty
-    go DWildCardT              = S.empty
-    go DStarT                  = S.empty
+    go_ty :: DType -> S.Set Name
+    go_ty (DForallT tvbs cxt ty) = (foldMap go_tvb tvbs <> go_ty ty <> foldMap go_pred cxt)
+                                   S.\\ foldMap dtvbName tvbs
+    go_ty (DAppT t1 t2)          = go_ty t1 <> go_ty t2
+    go_ty (DSigT ty ki)          = go_ty ty <> go_ty ki
+    go_ty (DVarT n)              = S.singleton n
+    go_ty (DConT {})             = S.empty
+    go_ty DArrowT                = S.empty
+    go_ty (DLitT {})             = S.empty
+    go_ty DWildCardT             = S.empty
+    go_ty DStarT                 = S.empty
+
+    go_pred :: DPred -> S.Set Name
+    go_pred (DAppPr pr ty) = go_pred pr <> go_ty ty
+    go_pred (DSigPr pr ki) = go_pred pr <> go_ty ki
+    go_pred (DVarPr n)     = S.singleton n
+    go_pred _              = S.empty
+
+    go_tvb :: DTyVarBndr -> S.Set Name
+    go_tvb (DPlainTV{})    = S.empty
+    go_tvb (DKindedTV _ k) = go_ty k
 
 dtvbName :: DTyVarBndr -> S.Set Name
 dtvbName (DPlainTV n)    = S.singleton n
diff --git a/Language/Haskell/TH/Desugar/Core.hs b/Language/Haskell/TH/Desugar/Core.hs
--- a/Language/Haskell/TH/Desugar/Core.hs
+++ b/Language/Haskell/TH/Desugar/Core.hs
@@ -27,8 +27,15 @@
 import Data.Foldable hiding (notElem)
 import Data.Traversable
 import Data.Data hiding (Fixity)
+#if __GLASGOW_HASKELL__ > 710
+import Data.Maybe (isJust)
+#endif
 import GHC.Generics hiding (Fixity)
 
+#if __GLASGOW_HASKELL__ >= 803
+import GHC.OverloadedLabels ( fromLabel )
+#endif
+
 import qualified Data.Set as S
 import GHC.Exts
 
@@ -177,10 +184,54 @@
 
 -- | A list of fields either for a standard data constructor or a record
 -- data constructor.
-data DConFields = DNormalC [DBangType]
+data DConFields = DNormalC DDeclaredInfix [DBangType]
                 | DRecC [DVarBangType]
                 deriving (Show, Typeable, Data, Generic)
 
+-- | 'True' if a constructor is declared infix. For normal ADTs, this means
+-- that is was written in infix style. For example, both of the constructors
+-- below are declared infix.
+--
+-- @
+-- data Infix = Int `Infix` Int | Int :*: Int
+-- @
+--
+-- Whereas neither of these constructors are declared infix:
+--
+-- @
+-- data Prefix = Prefix Int Int | (:+:) Int Int
+-- @
+--
+-- For GADTs, detecting whether a constructor is declared infix is a bit
+-- trickier, as one cannot write a GADT constructor "infix-style" like one
+-- can for normal ADT constructors. GHC considers a GADT constructor to be
+-- declared infix if it meets the following three criteria:
+--
+-- 1. Its name uses operator syntax (e.g., @(:*:)@).
+-- 2. It has exactly two fields (without record syntax).
+-- 3. It has a programmer-specified fixity declaration.
+--
+-- For example, in the following GADT:
+--
+-- @
+-- infixl 5 :**:, :&&:, :^^:, `ActuallyPrefix`
+-- data InfixGADT a where
+--   (:**:) :: Int -> b -> InfixGADT (Maybe b) -- Only this one is infix
+--   ActuallyPrefix :: Char -> Bool -> InfixGADT Double
+--   (:&&:) :: { infixGADT1 :: b, infixGADT2 :: Int } -> InfixGADT [b]
+--   (:^^:) :: Int -> Int -> Int -> InfixGADT Int
+--   (:!!:) :: Char -> Char -> InfixGADT Char
+-- @
+--
+-- Only the @(:**:)@ constructor is declared infix. The other constructors
+-- are not declared infix, because:
+--
+-- * @ActuallyPrefix@ does not use operator syntax (criterion 1).
+-- * @(:&&:)@ uses record syntax (criterion 2).
+-- * @(:^^:)@ does not have exactly two fields (criterion 2).
+-- * @(:!!:)@ does not have a programmer-specified fixity declaration (criterion 3).
+type DDeclaredInfix = Bool
+
 -- | Corresponds to TH's @BangType@ type.
 type DBangType = (Bang, DType)
 
@@ -331,12 +382,35 @@
 dsExp (SigE exp ty) = DSigE <$> dsExp exp <*> dsType ty
 dsExp (RecConE con_name field_exps) = do
   con <- dataConNameToCon con_name
-  reordered <- case con of
-                 RecC _name fields -> reorderFields fields field_exps
-                                                    (repeat $ DVarE 'undefined)
-                 _ -> impossible $ "Record syntax used with non-record constructor "
-                                   ++ (show con_name) ++ "."
+  reordered <- reorder con
   return $ foldl DAppE (DConE con_name) reordered
+  where
+    reorder con = case con of
+                    NormalC _name fields -> non_record fields
+                    InfixC field1 _name field2 -> non_record [field1, field2]
+                    RecC _name fields -> reorder_fields fields
+                    ForallC _ _ c -> reorder c
+#if __GLASGOW_HASKELL__ >= 800
+                    GadtC _names fields _ret_ty -> non_record fields
+                    RecGadtC _names fields _ret_ty -> reorder_fields fields
+#endif
+
+    reorder_fields fields = reorderFields fields field_exps
+                                          (repeat $ DVarE 'undefined)
+
+    non_record fields | null field_exps
+                        -- Special case: record construction is allowed for any
+                        -- constructor, regardless of whether the constructor
+                        -- actually was declared with records, provided that no
+                        -- records are given in the expression itself. (See #59).
+                        --
+                        -- Con{} desugars down to Con undefined ... undefined.
+                      = return $ replicate (length fields) $ DVarE 'undefined
+
+                      | otherwise =
+                          impossible $ "Record syntax used with non-record constructor "
+                                       ++ (show con_name) ++ "."
+
 dsExp (RecUpdE exp field_exps) = do
   -- here, we need to use one of the field names to find the tycon, somewhat dodgily
   first_name <- case field_exps of
@@ -375,19 +449,33 @@
     filter_cons_with_names cons field_names =
       filter has_names cons
       where
-        has_names (RecC _con_name args) =
+        args_contain_names args =
           let con_field_names = map fst_of_3 args in
           all (`elem` con_field_names) field_names
+
+        has_names (RecC _con_name args) =
+          args_contain_names args
+#if __GLASGOW_HASKELL__ >= 800
+        has_names (RecGadtC _con_name args _ret_ty) =
+          args_contain_names args
+#endif
         has_names (ForallC _ _ c) = has_names c
         has_names _               = False
 
-    con_to_dmatch :: DsMonad q => Con -> q DMatch
-    con_to_dmatch (RecC con_name args) = do
+    rec_con_to_dmatch con_name args = do
       let con_field_names = map fst_of_3 args
       field_var_names <- mapM (newUniqueName . nameBase) con_field_names
       DMatch (DConPa con_name (map DVarPa field_var_names)) <$>
              (foldl DAppE (DConE con_name) <$>
                     (reorderFields args field_exps (map DVarE field_var_names)))
+
+    con_to_dmatch :: DsMonad q => Con -> q DMatch
+    con_to_dmatch (RecC con_name args) = rec_con_to_dmatch con_name args
+#if __GLASGOW_HASKELL__ >= 800
+    -- We're assuming the GADT constructor has only one Name here, but since
+    -- this constructor was reified, this assumption should always hold true.
+    con_to_dmatch (RecGadtC [con_name] args _ret_ty) = rec_con_to_dmatch con_name args
+#endif
     con_to_dmatch (ForallC _ _ c) = con_to_dmatch c
     con_to_dmatch _ = impossible "Internal error within th-desugar."
 
@@ -406,6 +494,9 @@
 dsExp (UnboxedSumE exp alt arity) =
   DAppE (DConE $ unboxedSumDataName alt arity) <$> dsExp exp
 #endif
+#if __GLASGOW_HASKELL__ >= 803
+dsExp (LabelE str) = return $ DVarE 'fromLabel `DAppTypeE` DLitT (StrTyLit str)
+#endif
 
 -- | Desugar a lambda expression, where the body has already been desugared
 dsLam :: DsMonad q => [Pat] -> DExp -> q DExp
@@ -611,11 +702,33 @@
 dsPat WildP = return DWildPa
 dsPat (RecP con_name field_pats) = do
   con <- lift $ dataConNameToCon con_name
-  reordered <- case con of
-    RecC _name fields -> reorderFieldsPat fields field_pats
-    _ -> lift $ impossible $ "Record syntax used with non-record constructor "
-                             ++ (show con_name) ++ "."
+  reordered <- reorder con
   return $ DConPa con_name reordered
+  where
+    reorder con = case con of
+                     NormalC _name fields -> non_record fields
+                     InfixC field1 _name field2 -> non_record [field1, field2]
+                     RecC _name fields -> reorder_fields_pat fields
+                     ForallC _ _ c -> reorder c
+#if __GLASGOW_HASKELL__ >= 800
+                     GadtC _names fields _ret_ty -> non_record fields
+                     RecGadtC _names fields _ret_ty -> reorder_fields_pat fields
+#endif
+
+    reorder_fields_pat fields = reorderFieldsPat fields field_pats
+
+    non_record fields | null field_pats
+                        -- Special case: record patterns are allowed for any
+                        -- constructor, regardless of whether the constructor
+                        -- actually was declared with records, provided that
+                        -- no records are given in the pattern itself. (See #59).
+                        --
+                        -- Con{} desugars down to Con _ ... _.
+                      = return $ replicate (length fields) DWildPa
+                      | otherwise = lift $ impossible
+                                         $ "Record syntax used with non-record constructor "
+                                           ++ (show con_name) ++ "."
+
 dsPat (ListP pats) = go pats
   where go [] = return $ DConPa '[] []
         go (h : t) = do
@@ -950,13 +1063,13 @@
 dsCon :: DsMonad q
       => Con -> q [DCon]
 dsCon (NormalC n stys) =
-  (:[]) <$> (DCon [] [] n <$> (DNormalC <$> mapM dsBangType stys) <*> pure Nothing)
+  (:[]) <$> (DCon [] [] n <$> (DNormalC False <$> mapM dsBangType stys) <*> pure Nothing)
 dsCon (RecC n vstys) =
   (:[]) <$> (DCon [] [] n <$> (DRecC <$> mapM dsVarBangType vstys) <*> pure Nothing)
 dsCon (InfixC sty1 n sty2) = do
   dty1 <- dsBangType sty1
   dty2 <- dsBangType sty2
-  return $ [DCon [] [] n (DNormalC [dty1, dty2]) Nothing]
+  return $ [DCon [] [] n (DNormalC True [dty1, dty2]) Nothing]
 dsCon (ForallC tvbs cxt con) = do
   dtvbs <- mapM dsTvb tvbs
   dcxt <- dsCxt cxt
@@ -967,8 +1080,16 @@
 dsCon (GadtC nms btys rty) = do
   dbtys <- mapM dsBangType btys
   drty  <- dsType rty
-  return $ flip map nms $ \nm ->
-    DCon [] [] nm (DNormalC dbtys) (Just drty)
+  sequence $ flip map nms $ \nm -> do
+    mbFi <- reifyFixityWithLocals nm
+    -- A GADT data constructor is declared infix when these three
+    -- properties hold:
+    let decInfix = isInfixDataCon (nameBase nm) -- 1. Its name uses operator syntax
+                                                --    (e.g., (:*:))
+                || length dbtys == 2            -- 2. It has exactly two fields
+                || isJust mbFi                  -- 3. It has a programmer-specified
+                                                --    fixity declaration
+    return $ DCon [] [] nm (DNormalC decInfix dbtys) (Just drty)
 dsCon (RecGadtC nms vbtys rty) = do
   dvbtys <- mapM dsVarBangType vbtys
   drty   <- dsType rty
@@ -1272,3 +1393,15 @@
 strictToBang :: Bang -> Bang
 strictToBang = id
 #endif
+
+-- | Convert a 'DType' to a 'DPred'
+dTypeToDPred :: Monad q => DType -> q DPred
+dTypeToDPred (DForallT _ _ _) = impossible "Forall-type used as constraint"
+dTypeToDPred (DAppT t1 t2)   = liftM2 DAppPr (dTypeToDPred t1) (return t2)
+dTypeToDPred (DSigT ty ki)   = liftM2 DSigPr (dTypeToDPred ty) (return ki)
+dTypeToDPred (DVarT n)       = return $ DVarPr n
+dTypeToDPred (DConT n)       = return $ DConPr n
+dTypeToDPred DArrowT         = impossible "Arrow used as head of constraint"
+dTypeToDPred (DLitT _)       = impossible "Type literal used as head of constraint"
+dTypeToDPred DWildCardT      = return DWildCardPr
+dTypeToDPred DStarT          = impossible "Star used as head of constraint"
diff --git a/Language/Haskell/TH/Desugar/Expand.hs b/Language/Haskell/TH/Desugar/Expand.hs
--- a/Language/Haskell/TH/Desugar/Expand.hs
+++ b/Language/Haskell/TH/Desugar/Expand.hs
@@ -26,14 +26,10 @@
   expand, expandType,
 
   -- * Expand synonyms potentially unsoundly
-  expandUnsoundly,
-
-  -- * Capture-avoiding substitution
-  substTy
+  expandUnsoundly
   ) where
 
 import qualified Data.Map as M
-import qualified Data.Set as S
 import Control.Monad
 #if __GLASGOW_HASKELL__ < 709
 import Control.Applicative
@@ -42,16 +38,13 @@
 import Language.Haskell.TH.Syntax ( Quasi(..) )
 import Data.Data
 import Data.Generics
-import Data.List
 import qualified Data.Traversable as T
 
 import Language.Haskell.TH.Desugar.Core
 import Language.Haskell.TH.Desugar.Util
 import Language.Haskell.TH.Desugar.Sweeten
 import Language.Haskell.TH.Desugar.Reify
-
--- | Ignore kind annotations?
-data IgnoreKinds = YesIgnore | NoIgnore
+import Language.Haskell.TH.Desugar.Subst
 
 -- | Expands all type synonyms in a desugared type. Also expands open type family
 -- applications. (In GHCs before 7.10, this part does not work if there are any
@@ -118,14 +111,17 @@
 #endif
       -> do
         let (syn_args, rest_args) = splitAtList tvbs args
-        -- need to get the correct instance
-        insts <- qReifyInstances n (map typeToTH syn_args)
+        -- We need to get the correct instance. If we fail to reify anything
+        -- (e.g., if a type family is quasiquoted), then fall back by
+        -- pretending that there are no instances in scope.
+        insts <- qRecover (return []) $
+                 qReifyInstances n (map typeToTH syn_args)
         dinsts <- dsDecs insts
         case dinsts of
           [DTySynInstD _n (DTySynEqn lhs rhs)] -> do
             subst <-
               expectJustM "Impossible: reification returned a bogus instance" $
-              merge_maps $ zipWith build_subst lhs syn_args
+              unionMaybeSubsts $ zipWith (matchTy ign) lhs syn_args
             ty <- substTy subst rhs
             ty' <- expand_type ign ty
             return $ foldl DAppT ty' rest_args
@@ -148,7 +144,7 @@
          -- returns the substed rhs
         check_eqn :: DsMonad q => [DType] -> DTySynEqn -> q (Maybe DType)
         check_eqn arg_tys (DTySynEqn lhs rhs) = do
-          let m_subst = merge_maps $ zipWith build_subst lhs arg_tys
+          let m_subst = unionMaybeSubsts $ zipWith (matchTy ign) lhs arg_tys
           T.mapM (flip substTy rhs) m_subst
 
     _ -> return $ foldl DAppT (DConT n) args
@@ -169,102 +165,13 @@
         _                                        -> True
     no_tyvar_tyfam t = gmapQl (liftM2 (&&)) (return True) no_tyvars_tyfams t
 
-    build_subst :: DType -> DType -> Maybe (M.Map Name DType)
-    build_subst (DVarT var_name) arg = Just $ M.singleton var_name arg
-      -- if a pattern has a kind signature, it's really easy to get
-      -- this wrong.
-    build_subst (DSigT ty _ki) arg = case ign of
-      YesIgnore -> build_subst ty arg
-      NoIgnore  -> Nothing
-      -- but we can safely ignore kind signatures on the target
-    build_subst pat (DSigT ty _ki) = build_subst pat ty
-    build_subst (DForallT {}) _ =
-      error "Impossible: forall-quantified pattern to type family"
-      -- reifyInstances should fail if an argument is forall-quantified.
-    build_subst _ (DForallT {}) =
-      error "Impossible: forall-quantified argument to type family"
-    build_subst (DAppT pat1 pat2) (DAppT arg1 arg2) =
-      merge_maps [build_subst pat1 arg1, build_subst pat2 arg2]
-    build_subst (DConT pat_con) (DConT arg_con)
-      | pat_con == arg_con = Just M.empty
-    build_subst DArrowT DArrowT = Just M.empty
-    build_subst (DLitT pat_lit) (DLitT arg_lit)
-      | pat_lit == arg_lit = Just M.empty
-    build_subst _ _ = Nothing
-
-    merge_maps :: [Maybe (M.Map Name DType)] -> Maybe (M.Map Name DType)
-    merge_maps = foldl' merge_map1 (Just M.empty)
-
-    merge_map1 :: Maybe (M.Map Name DType) -> Maybe (M.Map Name DType)
-               -> Maybe (M.Map Name DType)
-    merge_map1 ma mb = do
-      a <- ma
-      b <- mb
-      let shared_key_set = M.keysSet a `S.intersection` M.keysSet b
-          matches_up     = S.foldr (\name -> ((a M.! name) `geq` (b M.! name) &&))
-                                   True shared_key_set
-      if matches_up then return (a `M.union` b) else Nothing
-
     allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
     allM f = foldM (\b x -> (b &&) `liftM` f x) True
 
--- | Capture-avoiding substitution on types
-substTy :: DsMonad q => M.Map Name DType -> DType -> q DType
-substTy vars (DForallT tvbs cxt ty) =
-  substTyVarBndrs vars tvbs $ \vars' tvbs' -> do
-    cxt' <- mapM (substPred vars') cxt
-    ty' <- substTy vars' ty
-    return $ DForallT tvbs' cxt' ty'
-substTy vars (DAppT t1 t2) =
-  DAppT <$> substTy vars t1 <*> substTy vars t2
-substTy vars (DSigT ty ki) =
-  DSigT <$> substTy vars ty <*> pure ki
-substTy vars (DVarT n)
-  | Just ty <- M.lookup n vars
-  = return ty
-  | otherwise
-  = return $ DVarT n
-substTy _ ty = return ty
-
-substTyVarBndrs :: DsMonad q => M.Map Name DType -> [DTyVarBndr]
-                -> (M.Map Name DType -> [DTyVarBndr] -> q DType)
-                -> q DType
-substTyVarBndrs vars tvbs thing = do
-  new_names <- mapM (const (qNewName "local")) tvbs
-  let new_vars = M.fromList (zip (map extractDTvbName tvbs) (map DVarT new_names))
-  -- this is very inefficient. Oh well.
-  thing (M.union vars new_vars) (zipWith substTvb tvbs new_names)
-
-substTvb :: DTyVarBndr -> Name -> DTyVarBndr
-substTvb (DPlainTV _) n = DPlainTV n
-substTvb (DKindedTV _ k) n = DKindedTV n k
-
 -- | Extract the name from a @TyVarBndr@
 extractDTvbName :: DTyVarBndr -> Name
 extractDTvbName (DPlainTV n) = n
 extractDTvbName (DKindedTV n _) = n
-
-substPred :: DsMonad q => M.Map Name DType -> DPred -> q DPred
-substPred vars (DAppPr p t) = DAppPr <$> substPred vars p <*> substTy vars t
-substPred vars (DSigPr p k) = DSigPr <$> substPred vars p <*> pure k
-substPred vars (DVarPr n)
-  | Just ty <- M.lookup n vars
-  = dTypeToDPred ty
-  | otherwise
-  = return $ DVarPr n
-substPred _ p = return p
-
--- | Convert a 'DType' to a 'DPred'
-dTypeToDPred :: DsMonad q => DType -> q DPred
-dTypeToDPred (DForallT _ _ _) = impossible "Forall-type used as constraint"
-dTypeToDPred (DAppT t1 t2)   = DAppPr <$> dTypeToDPred t1 <*> pure t2
-dTypeToDPred (DSigT ty ki)   = DSigPr <$> dTypeToDPred ty <*> pure ki
-dTypeToDPred (DVarT n)       = return $ DVarPr n
-dTypeToDPred (DConT n)       = return $ DConPr n
-dTypeToDPred DArrowT         = impossible "Arrow used as head of constraint"
-dTypeToDPred (DLitT _)       = impossible "Type literal used as head of constraint"
-dTypeToDPred DWildCardT      = return DWildCardPr
-dTypeToDPred DStarT          = impossible "Star used as head of constraint"
 
 -- | Expand all type synonyms and type families in the desugared abstract
 -- syntax tree provided, where type family simplification is on a "best effort"
diff --git a/Language/Haskell/TH/Desugar/Reify.hs b/Language/Haskell/TH/Desugar/Reify.hs
--- a/Language/Haskell/TH/Desugar/Reify.hs
+++ b/Language/Haskell/TH/Desugar/Reify.hs
@@ -19,6 +19,11 @@
   -- * Datatype lookup
   getDataD, dataConNameToCon, dataConNameToDataName,
 
+  -- * Value and type lookup
+  lookupValueNameWithLocals, lookupTypeNameWithLocals,
+  mkDataNameWithLocals, mkTypeNameWithLocals,
+  reifyNameSpace,
+
   -- * Monad support
   DsMonad(..), DsM, withLocalDeclarations
   ) where
@@ -167,6 +172,9 @@
 #if __GLASGOW_HASKELL__ >= 800
            , Fail.MonadFail
 #endif
+#if __GLASGOW_HASKELL__ >= 803
+           , MonadIO
+#endif
            )
 
 instance Quasi q => DsMonad (DsM q) where
@@ -197,7 +205,7 @@
 
 -- | Look through a list of declarations and possibly return a relevant 'Info'
 reifyInDecs :: Name -> [Dec] -> Maybe Info
-reifyInDecs n decs = firstMatch (reifyInDec n decs) decs
+reifyInDecs n decs = snd `fmap` firstMatch (reifyInDec n decs) decs
 
 -- | Look through a list of declarations and possibly return a fixity.
 reifyFixityInDecs :: Name -> [Dec] -> Maybe Fixity
@@ -206,43 +214,45 @@
     match_fixity (InfixD fixity n') | n `nameMatches` n' = Just fixity
     match_fixity _                                       = Nothing
 
+-- | A reified thing along with the name of that thing.
+type Named a = (Name, a)
 
-reifyInDec :: Name -> [Dec] -> Dec -> Maybe Info
-reifyInDec n decs (FunD n' _) | n `nameMatches` n' = Just $ mkVarI n decs
+reifyInDec :: Name -> [Dec] -> Dec -> Maybe (Named Info)
+reifyInDec n decs (FunD n' _) | n `nameMatches` n' = Just (n', mkVarI n decs)
 reifyInDec n decs (ValD pat _ _)
-  | any (nameMatches n) (S.elems (extractBoundNamesPat pat)) = Just $ mkVarI n decs
+  | Just n' <- find (nameMatches n) (S.elems (extractBoundNamesPat pat)) = Just (n', mkVarI n decs)
 #if __GLASGOW_HASKELL__ > 710
-reifyInDec n _    dec@(DataD    _ n' _ _ _ _) | n `nameMatches` n' = Just $ TyConI dec
-reifyInDec n _    dec@(NewtypeD _ n' _ _ _ _) | n `nameMatches` n' = Just $ TyConI dec
+reifyInDec n _    dec@(DataD    _ n' _ _ _ _) | n `nameMatches` n' = Just (n', TyConI dec)
+reifyInDec n _    dec@(NewtypeD _ n' _ _ _ _) | n `nameMatches` n' = Just (n', TyConI dec)
 #else
-reifyInDec n _    dec@(DataD    _ n' _ _ _) | n `nameMatches` n' = Just $ TyConI dec
-reifyInDec n _    dec@(NewtypeD _ n' _ _ _) | n `nameMatches` n' = Just $ TyConI dec
+reifyInDec n _    dec@(DataD    _ n' _ _ _) | n `nameMatches` n' = Just (n', TyConI dec)
+reifyInDec n _    dec@(NewtypeD _ n' _ _ _) | n `nameMatches` n' = Just (n', TyConI dec)
 #endif
-reifyInDec n _    dec@(TySynD n' _ _)       | n `nameMatches` n' = Just $ TyConI dec
+reifyInDec n _    dec@(TySynD n' _ _)       | n `nameMatches` n' = Just (n', TyConI dec)
 reifyInDec n decs dec@(ClassD _ n' _ _ _)   | n `nameMatches` n'
-  = Just $ ClassI (stripClassDec dec) (findInstances n decs)
+  = Just (n', ClassI (stripClassDec dec) (findInstances n decs))
 reifyInDec n decs (ForeignD (ImportF _ _ _ n' ty)) | n `nameMatches` n'
-  = Just $ mkVarITy n decs ty
+  = Just (n', mkVarITy n decs ty)
 reifyInDec n decs (ForeignD (ExportF _ _ n' ty)) | n `nameMatches` n'
-  = Just $ mkVarITy n decs ty
+  = Just (n', mkVarITy n decs ty)
 #if __GLASGOW_HASKELL__ > 710
 reifyInDec n decs dec@(OpenTypeFamilyD (TypeFamilyHead n' _ _ _)) | n `nameMatches` n'
-  = Just $ FamilyI (handleBug8884 dec) (findInstances n decs)
+  = Just (n', FamilyI (handleBug8884 dec) (findInstances n decs))
 reifyInDec n decs dec@(DataFamilyD n' _ _) | n `nameMatches` n'
-  = Just $ FamilyI (handleBug8884 dec) (findInstances n decs)
+  = Just (n', FamilyI (handleBug8884 dec) (findInstances n decs))
 reifyInDec n _    dec@(ClosedTypeFamilyD (TypeFamilyHead n' _ _ _) _) | n `nameMatches` n'
-  = Just $ FamilyI dec []
+  = Just (n', FamilyI dec [])
 #else
 reifyInDec n decs dec@(FamilyD _ n' _ _) | n `nameMatches` n'
-  = Just $ FamilyI (handleBug8884 dec) (findInstances n decs)
+  = Just (n', FamilyI (handleBug8884 dec) (findInstances n decs))
 #if __GLASGOW_HASKELL__ >= 707
 reifyInDec n _    dec@(ClosedTypeFamilyD n' _ _ _) | n `nameMatches` n'
-  = Just $ FamilyI dec []
+  = Just (n', FamilyI dec [])
 #endif
 #endif
 #if __GLASGOW_HASKELL__ >= 801
 reifyInDec n decs (PatSynD n' _ _ _) | n `nameMatches` n'
-  = Just $ mkPatSynI n decs
+  = Just (n', mkPatSynI n decs)
 #endif
 
 #if __GLASGOW_HASKELL__ > 710
@@ -262,14 +272,14 @@
 #endif
 #if __GLASGOW_HASKELL__ > 710
 reifyInDec n _decs (ClassD _ ty_name tvbs _ sub_decs)
-  | Just ty <- findType n sub_decs
-  = Just $ ClassOpI n (addClassCxt ty_name tvbs ty) ty_name
+  | Just (n', ty) <- findType n sub_decs
+  = Just (n', ClassOpI n (addClassCxt ty_name tvbs ty) ty_name)
 #else
 reifyInDec n decs (ClassD _ ty_name tvbs _ sub_decs)
-  | Just ty <- findType n sub_decs
-  = Just $ ClassOpI n (addClassCxt ty_name tvbs ty)
-                    ty_name (fromMaybe defaultFixity $
-                             reifyFixityInDecs n $ sub_decs ++ decs)
+  | Just (n', ty) <- findType n sub_decs
+  = Just (n', ClassOpI n (addClassCxt ty_name tvbs ty)
+                       ty_name (fromMaybe defaultFixity $
+                                reifyFixityInDecs n $ sub_decs ++ decs))
 #endif
 reifyInDec n decs (ClassD _ _ _ _ sub_decs)
   | Just info <- firstMatch (reifyInDec n (sub_decs ++ decs)) sub_decs
@@ -303,24 +313,24 @@
 
 reifyInDec _ _ _ = Nothing
 
-maybeReifyCon :: Name -> [Dec] -> Name -> [Type] -> [Con] -> Maybe Info
+maybeReifyCon :: Name -> [Dec] -> Name -> [Type] -> [Con] -> Maybe (Named Info)
 #if __GLASGOW_HASKELL__ > 710
 maybeReifyCon n _decs ty_name ty_args cons
-  | Just con <- findCon n cons
-  = Just $ DataConI n (maybeForallT tvbs [] $ con_to_type con) ty_name
+  | Just (n', con) <- findCon n cons
+  = Just (n', DataConI n (maybeForallT tvbs [] $ con_to_type con) ty_name)
 #else
 maybeReifyCon n decs ty_name ty_args cons
-  | Just con <- findCon n cons
-  = Just $ DataConI n (maybeForallT tvbs [] $ con_to_type con)
-                    ty_name fixity
+  | Just (n', con) <- findCon n cons
+  = Just (n', DataConI n (maybeForallT tvbs [] $ con_to_type con)
+                         ty_name fixity)
 #endif
 
-  | Just ty <- findRecSelector n cons
+  | Just (n', ty) <- findRecSelector n cons
       -- we don't try to ferret out naughty record selectors.
 #if __GLASGOW_HASKELL__ > 710
-  = Just $ VarI n (maybeForallT tvbs [] $ mkArrows [result_ty] ty) Nothing
+  = Just (n', VarI n (maybeForallT tvbs [] $ mkArrows [result_ty] ty) Nothing)
 #else
-  = Just $ VarI n (maybeForallT tvbs [] $ mkArrows [result_ty] ty) Nothing fixity
+  = Just (n', VarI n (maybeForallT tvbs [] $ mkArrows [result_ty] ty) Nothing fixity)
 #endif
   where
     result_ty = foldl AppT (ConT ty_name) ty_args
@@ -340,7 +350,7 @@
 maybeReifyCon _ _ _ _ _ = Nothing
 
 mkVarI :: Name -> [Dec] -> Info
-mkVarI n decs = mkVarITy n decs (fromMaybe (no_type n) $ findType n decs)
+mkVarI n decs = mkVarITy n decs (maybe (no_type n) snd $ findType n decs)
 
 mkVarITy :: Name -> [Dec] -> Type -> Info
 #if __GLASGOW_HASKELL__ > 710
@@ -350,11 +360,11 @@
                                         reifyFixityInDecs n decs)
 #endif
 
-findType :: Name -> [Dec] -> Maybe Type
+findType :: Name -> [Dec] -> Maybe (Named Type)
 findType n = firstMatch match_type
   where
-    match_type (SigD n' ty) | n `nameMatches` n' = Just ty
-    match_type _                             = Nothing
+    match_type (SigD n' ty) | n `nameMatches` n' = Just (n', ty)
+    match_type _                                 = Nothing
 
 #if __GLASGOW_HASKELL__ >= 801
 mkPatSynI :: Name -> [Dec] -> Info
@@ -447,27 +457,43 @@
   | ForallT tvbs2 cxt2 ty2 <- ty = ForallT (tvbs ++ tvbs2) (cxt ++ cxt2) ty2
   | otherwise                    = ForallT tvbs cxt ty
 
-findCon :: Name -> [Con] -> Maybe Con
-findCon n = find match_con
+findCon :: Name -> [Con] -> Maybe (Named Con)
+findCon n = firstMatch match_con
   where
-    match_con (NormalC n' _)  = n `nameMatches` n'
-    match_con (RecC n' _)     = n `nameMatches` n'
-    match_con (InfixC _ n' _) = n `nameMatches` n'
-    match_con (ForallC _ _ c) = match_con c
+    match_con :: Con -> Maybe (Named Con)
+    match_con con =
+      case con of
+        NormalC n' _  | n `nameMatches` n' -> Just (n', con)
+        RecC n' _     | n `nameMatches` n' -> Just (n', con)
+        InfixC _ n' _ | n `nameMatches` n' -> Just (n', con)
+        ForallC _ _ c -> case match_con c of
+                           Just (n', _) -> Just (n', con)
+                           Nothing      -> Nothing
 #if __GLASGOW_HASKELL__ > 710
-    match_con (GadtC nms _ _)    = any (n `nameMatches`) nms
-    match_con (RecGadtC nms _ _) = any (n `nameMatches`) nms
+        GadtC nms _ _    -> gadt_case con nms
+        RecGadtC nms _ _ -> gadt_case con nms
 #endif
+        _                -> Nothing
 
-findRecSelector :: Name -> [Con] -> Maybe Type
+#if __GLASGOW_HASKELL__ > 710
+    gadt_case :: Con -> [Name] -> Maybe (Named Con)
+    gadt_case con nms = case find (n `nameMatches`) nms of
+                          Just n' -> Just (n', con)
+                          Nothing -> Nothing
+#endif
+
+findRecSelector :: Name -> [Con] -> Maybe (Named Type)
 findRecSelector n = firstMatch match_con
   where
-    match_con (RecC _ vstys)  = firstMatch match_rec_sel vstys
-    match_con (ForallC _ _ c) = match_con c
-    match_con _               = Nothing
+    match_con (RecC _ vstys)       = firstMatch match_rec_sel vstys
+#if __GLASGOW_HASKELL__ >= 800
+    match_con (RecGadtC _ vstys _) = firstMatch match_rec_sel vstys
+#endif
+    match_con (ForallC _ _ c)      = match_con c
+    match_con _                    = Nothing
 
-    match_rec_sel (n', _, ty) | n `nameMatches` n' = Just ty
-    match_rec_sel _                     = Nothing
+    match_rec_sel (n', _, ty) | n `nameMatches` n' = Just (n', ty)
+    match_rec_sel _                                = Nothing
 
 handleBug8884 :: Dec -> Dec
 #if __GLASGOW_HASKELL__ >= 707
@@ -521,3 +547,108 @@
 reifyFixityWithLocals name = qRecover
   (return . reifyFixityInDecs name =<< localDeclarations)
   (qReifyFixity name)
+
+--------------------------------------
+-- Lookuping name value and type names
+--------------------------------------
+
+-- | Like 'lookupValueName' from Template Haskell, but looks also in 'Names' of
+-- not-yet-typechecked declarations. To establish this list of not-yet-typechecked
+-- declarations, use 'withLocalDeclarations'. Returns 'Nothing' if no value
+-- with the same name can be found.
+lookupValueNameWithLocals :: DsMonad q => String -> q (Maybe Name)
+lookupValueNameWithLocals = lookupNameWithLocals False
+
+-- | Like 'lookupTypeName' from Template Haskell, but looks also in 'Names' of
+-- not-yet-typechecked declarations. To establish this list of not-yet-typechecked
+-- declarations, use 'withLocalDeclarations'. Returns 'Nothing' if no type
+-- with the same name can be found.
+lookupTypeNameWithLocals :: DsMonad q => String -> q (Maybe Name)
+lookupTypeNameWithLocals = lookupNameWithLocals True
+
+lookupNameWithLocals :: DsMonad q => Bool -> String -> q (Maybe Name)
+lookupNameWithLocals ns s = do
+    mb_name <- qLookupName ns s
+    case mb_name of
+      j_name@(Just{}) -> return j_name
+      Nothing         -> consult_locals
+  where
+    built_name = mkName s
+
+    consult_locals = do
+      decs <- localDeclarations
+      let mb_infos = map (reifyInDec built_name decs) decs
+          infos = catMaybes mb_infos
+      return $ firstMatch (if ns then find_type_name
+                                 else find_value_name) infos
+
+    -- These functions work over Named Infos so we can avoid performing
+    -- tiresome pattern-matching to retrieve the name associated with each Info.
+    find_type_name, find_value_name :: Named Info -> Maybe Name
+    find_type_name (n, info) =
+      case infoNameSpace info of
+        TcClsName -> Just n
+        VarName   -> Nothing
+        DataName  -> Nothing
+
+    find_value_name (n, info) =
+      case infoNameSpace info of
+        VarName   -> Just n
+        DataName  -> Just n
+        TcClsName -> Nothing
+
+-- | Like TH's @lookupValueName@, but if this name is not bound, then we assume
+-- it is declared in the current module.
+--
+-- Unlike 'mkDataName', this also consults the local declarations in scope when
+-- determining if the name is currently bound.
+mkDataNameWithLocals :: DsMonad q => String -> q Name
+mkDataNameWithLocals = mkNameWith lookupValueNameWithLocals mkNameG_d
+
+-- | Like TH's @lookupTypeName@, but if this name is not bound, then we assume
+-- it is declared in the current module.
+--
+-- Unlike 'mkTypeName', this also consults the local declarations in scope when
+-- determining if the name is currently bound.
+mkTypeNameWithLocals :: DsMonad q => String -> q Name
+mkTypeNameWithLocals = mkNameWith lookupTypeNameWithLocals mkNameG_tc
+
+-- | Determines a `Name`'s 'NameSpace'. If the 'NameSpace' is attached to
+-- the 'Name' itself (i.e., it is unambiguous), then that 'NameSpace' is
+-- immediately returned. Otherwise, reification is used to lookup up the
+-- 'NameSpace' (consulting local declarations if necessary).
+--
+-- Note that if a 'Name' lives in two different 'NameSpaces' (which can
+-- genuinely happen--for instance, @'mkName' \"==\"@, where @==@ is both
+-- a function and a type family), then this function will simply return
+-- whichever 'NameSpace' is discovered first via reification. If you wish
+-- to find a 'Name' in a particular 'NameSpace', use the
+-- 'lookupValueNameWithLocals' or 'lookupTypeNameWithLocals' functions.
+reifyNameSpace :: DsMonad q => Name -> q (Maybe NameSpace)
+reifyNameSpace n@(Name _ nf) =
+  case nf of
+    -- NameGs are simple, as they have a NameSpace attached.
+    NameG ns _ _ -> pure $ Just ns
+
+    -- For other names, we must use reification to determine what NameSpace
+    -- it lives in (if any).
+    _ -> do mb_info <- reifyWithLocals_maybe n
+            pure $ fmap infoNameSpace mb_info
+
+-- | Determine a name's 'NameSpace' from its 'Info'.
+infoNameSpace :: Info -> NameSpace
+infoNameSpace info =
+  case info of
+    ClassI{}     -> TcClsName
+    TyConI{}     -> TcClsName
+    FamilyI{}    -> TcClsName
+    PrimTyConI{} -> TcClsName
+    TyVarI{}     -> TcClsName
+
+    ClassOpI{}   -> VarName
+    VarI{}       -> VarName
+
+    DataConI{}   -> DataName
+#if __GLASGOW_HASKELL__ >= 801
+    PatSynI{}    -> DataName
+#endif
diff --git a/Language/Haskell/TH/Desugar/Subst.hs b/Language/Haskell/TH/Desugar/Subst.hs
new file mode 100644
--- /dev/null
+++ b/Language/Haskell/TH/Desugar/Subst.hs
@@ -0,0 +1,146 @@
+{-# LANGUAGE CPP #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Language.Haskell.TH.Desugar.Subst
+-- Copyright   :  (C) 2018 Richard Eisenberg
+-- License     :  BSD-style (see LICENSE)
+-- Maintainer  :  Richard Eisenberg (rae@cs.brynmawr.edu)
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Capture-avoiding substitutions on 'DType's
+--
+----------------------------------------------------------------------------
+
+module Language.Haskell.TH.Desugar.Subst (
+  DSubst,
+
+  -- * Capture-avoiding substitution
+  substTy, unionSubsts, unionMaybeSubsts,
+
+  -- * Matching a type template against a type
+  IgnoreKinds(..), matchTy
+  ) where
+
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+import Data.Generics
+import Data.List
+
+import Language.Haskell.TH.Desugar.Core
+import Language.Haskell.TH.Syntax
+import Language.Haskell.TH.Desugar.Util
+
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+
+-- | A substitution is just a map from names to types
+type DSubst = M.Map Name DType
+
+-- | Capture-avoiding substitution on types
+substTy :: Quasi q => DSubst -> DType -> q DType
+substTy vars (DForallT tvbs cxt ty) =
+  substTyVarBndrs vars tvbs $ \vars' tvbs' -> do
+    cxt' <- mapM (substPred vars') cxt
+    ty' <- substTy vars' ty
+    return $ DForallT tvbs' cxt' ty'
+substTy vars (DAppT t1 t2) =
+  DAppT <$> substTy vars t1 <*> substTy vars t2
+substTy vars (DSigT ty ki) =
+  DSigT <$> substTy vars ty <*> substTy vars ki
+substTy vars (DVarT n)
+  | Just ty <- M.lookup n vars
+  = return ty
+  | otherwise
+  = return $ DVarT n
+substTy _ ty = return ty
+
+substTyVarBndrs :: Quasi q => DSubst -> [DTyVarBndr]
+                -> (DSubst -> [DTyVarBndr] -> q DType)
+                -> q DType
+substTyVarBndrs vars tvbs thing = do
+  (vars', tvbs') <- mapAccumLM substTvb vars tvbs
+  thing vars' tvbs'
+
+substTvb :: Quasi q => DSubst -> DTyVarBndr
+         -> q (DSubst, DTyVarBndr)
+substTvb vars (DPlainTV n) = do
+  new_n <- qNewName (nameBase n)
+  return (M.insert n (DVarT new_n) vars, DPlainTV new_n)
+substTvb vars (DKindedTV n k) = do
+  new_n <- qNewName (nameBase n)
+  k' <- substTy vars k
+  return (M.insert n (DVarT new_n) vars, DKindedTV new_n k')
+
+substPred :: Quasi q => DSubst -> DPred -> q DPred
+substPred vars (DAppPr p t) = DAppPr <$> substPred vars p <*> substTy vars t
+substPred vars (DSigPr p k) = DSigPr <$> substPred vars p <*> substTy vars k
+substPred vars (DVarPr n)
+  | Just ty <- M.lookup n vars
+  = dTypeToDPred ty
+  | otherwise
+  = return $ DVarPr n
+substPred _ p = return p
+
+-- | Computes the union of two substitutions. Fails if both subsitutions map
+-- the same variable to different types.
+unionSubsts :: DSubst -> DSubst -> Maybe DSubst
+unionSubsts a b =
+  let shared_key_set = M.keysSet a `S.intersection` M.keysSet b
+      matches_up     = S.foldr (\name -> ((a M.! name) `geq` (b M.! name) &&))
+                               True shared_key_set
+  in
+  if matches_up then return (a `M.union` b) else Nothing
+
+---------------------------
+-- Matching
+
+-- | Ignore kind annotations in @matchTy@?
+data IgnoreKinds = YesIgnore | NoIgnore
+
+-- | @matchTy ign tmpl targ@ matches a type template @tmpl@ against a type
+-- target @targ@. This returns a Map from names of type variables in the
+-- type template to types if the types indeed match up, or @Nothing@ otherwise.
+-- In the @Just@ case, it is guaranteed that every type variable mentioned
+-- in the template is mapped by the returned substitution.
+--
+-- The first argument @ign@ tells @matchTy@ whether to ignore kind signatures
+-- in the template. A kind signature in the template might mean that a type
+-- variable has a more restrictive kind than otherwise possible, and that
+-- mapping that type variable to a type of a different kind could be disastrous.
+-- So, if we don't ignore kind signatures, this function returns @Nothing@ if
+-- the template has a signature anywhere. If we do ignore kind signatures, it's
+-- possible the returned map will be ill-kinded. Use at your own risk.
+matchTy :: IgnoreKinds -> DType -> DType -> Maybe DSubst
+matchTy _   (DVarT var_name) arg = Just $ M.singleton var_name arg
+  -- if a pattern has a kind signature, it's really easy to get
+  -- this wrong.
+matchTy ign (DSigT ty _ki) arg = case ign of
+  YesIgnore -> matchTy ign ty arg
+  NoIgnore  -> Nothing
+  -- but we can safely ignore kind signatures on the target
+matchTy ign pat (DSigT ty _ki) = matchTy ign pat ty
+matchTy _   (DForallT {}) _ =
+  error "Cannot match a forall in a pattern"
+matchTy _   _ (DForallT {}) =
+  error "Cannot match a forall in a target"
+matchTy ign (DAppT pat1 pat2) (DAppT arg1 arg2) =
+  unionMaybeSubsts [matchTy ign pat1 arg1, matchTy ign pat2 arg2]
+matchTy _   (DConT pat_con) (DConT arg_con)
+  | pat_con == arg_con = Just M.empty
+matchTy _   DArrowT DArrowT = Just M.empty
+matchTy _   (DLitT pat_lit) (DLitT arg_lit)
+  | pat_lit == arg_lit = Just M.empty
+matchTy _ _ _ = Nothing
+
+unionMaybeSubsts :: [Maybe DSubst] -> Maybe DSubst
+unionMaybeSubsts = foldl' union_subst1 (Just M.empty)
+  where
+    union_subst1 :: Maybe DSubst -> Maybe DSubst -> Maybe DSubst
+    union_subst1 ma mb = do
+      a <- ma
+      b <- mb
+      unionSubsts a b
diff --git a/Language/Haskell/TH/Desugar/Sweeten.hs b/Language/Haskell/TH/Desugar/Sweeten.hs
--- a/Language/Haskell/TH/Desugar/Sweeten.hs
+++ b/Language/Haskell/TH/Desugar/Sweeten.hs
@@ -217,12 +217,21 @@
 
 conToTH :: DCon -> Con
 #if __GLASGOW_HASKELL__ > 710
-conToTH (DCon [] [] n (DNormalC stys) (Just rty)) =
+conToTH (DCon [] [] n (DNormalC _ stys) (Just rty)) =
   GadtC [n] (map (second typeToTH) stys) (typeToTH rty)
 conToTH (DCon [] [] n (DRecC vstys) (Just rty)) =
   RecGadtC [n] (map (thirdOf3 typeToTH) vstys) (typeToTH rty)
 #endif
-conToTH (DCon [] [] n (DNormalC stys) _) =
+conToTH (DCon [] [] n (DNormalC True [sty1, sty2]) _) =
+#if __GLASGOW_HASKELL__ > 710
+  InfixC (second typeToTH sty1) n (second typeToTH sty2)
+#else
+  InfixC ((bangToStrict *** typeToTH) sty1) n ((bangToStrict *** typeToTH) sty2)
+#endif
+-- Note: it's possible that someone could pass in a DNormalC value that
+-- erroneously claims that it's declared infix (e.g., if has more than two
+-- fields), but we will fall back on NormalC in such a scenario.
+conToTH (DCon [] [] n (DNormalC _ stys) _) =
 #if __GLASGOW_HASKELL__ > 710
   NormalC n (map (second typeToTH) stys)
 #else
diff --git a/Language/Haskell/TH/Desugar/Util.hs b/Language/Haskell/TH/Desugar/Util.hs
--- a/Language/Haskell/TH/Desugar/Util.hs
+++ b/Language/Haskell/TH/Desugar/Util.hs
@@ -11,9 +11,9 @@
 module Language.Haskell.TH.Desugar.Util (
   newUniqueName,
   impossible,
-  nameOccursIn, allNamesIn, mkTypeName, mkDataName, isDataName,
+  nameOccursIn, allNamesIn, mkTypeName, mkDataName, mkNameWith, isDataName,
   stripVarP_maybe, extractBoundNamesStmt,
-  concatMapM, mapMaybeM, expectJustM,
+  concatMapM, mapAccumLM, mapMaybeM, expectJustM,
   stripPlainTV_maybe,
   thirdOf3, splitAtList, extractBoundNamesDec,
   extractBoundNamesPat,
@@ -21,7 +21,7 @@
   unboxedSumDegree_maybe, unboxedSumNameDegree_maybe,
   tupleDegree_maybe, tupleNameDegree_maybe, unboxedTupleDegree_maybe,
   unboxedTupleNameDegree_maybe, splitTuple_maybe,
-  topEverywhereM
+  topEverywhereM, isInfixDataCon
   ) where
 
 import Prelude hiding (mapM, foldl, concatMap, any)
@@ -34,7 +34,10 @@
 import Data.Generics hiding ( Fixity )
 import Data.Traversable
 import Data.Maybe
+
+#if __GLASGOW_HASKELL__ < 804
 import Data.Monoid
+#endif
 
 ----------------------------------------
 -- TH manipulations
@@ -48,27 +51,31 @@
   n <- qNewName str
   qNewName $ show n
 
--- | Like TH's @lookupTypeName@, but if this name is not bound, then we assume
--- it is declared in the current module.
-mkTypeName :: Quasi q => String -> q Name
-mkTypeName str = do
-  m_name <- qLookupName True str
+-- | @mkNameWith lookup_fun mkName_fun str@ looks up the exact 'Name' of @str@
+-- using the function @lookup_fun@. If it finds 'Just' the 'Name', meaning
+-- that it is bound in the current scope, then it is returned. If it finds
+-- 'Nothing', it assumes that @str@ is declared in the current module, and
+-- uses @mkName_fun@ to construct the appropriate 'Name' to return.
+mkNameWith :: Quasi q => (String -> q (Maybe Name))
+                      -> (String -> String -> String -> Name)
+                      -> String -> q Name
+mkNameWith lookup_fun mkName_fun str = do
+  m_name <- lookup_fun str
   case m_name of
     Just name -> return name
     Nothing -> do
       Loc { loc_package = pkg, loc_module = modu } <- qLocation
-      return $ mkNameG_tc pkg modu str
+      return $ mkName_fun pkg modu str
 
+-- | Like TH's @lookupTypeName@, but if this name is not bound, then we assume
+-- it is declared in the current module.
+mkTypeName :: Quasi q => String -> q Name
+mkTypeName = mkNameWith (qLookupName True) mkNameG_tc
+
 -- | Like TH's @lookupDataName@, but if this name is not bound, then we assume
 -- it is declared in the current module.
 mkDataName :: Quasi q => String -> q Name
-mkDataName str = do
-  m_name <- qLookupName False str
-  case m_name of
-    Just name -> return name
-    Nothing -> do
-      Loc { loc_package = pkg, loc_module = modu } <- qLocation
-      return $ mkNameG_d pkg modu str
+mkDataName = mkNameWith (qLookupName False) mkNameG_d
 
 -- | Is this name a data constructor name? A 'False' answer means "unsure".
 isDataName :: Name -> Bool
@@ -220,12 +227,12 @@
 #endif
 
 freeNamesOfTypes :: [Type] -> S.Set Name
-freeNamesOfTypes = mconcat . map go
+freeNamesOfTypes = foldMap go
   where
-    go (ForallT tvbs cxt ty) = (go ty <> mconcat (map go_pred cxt))
+    go (ForallT tvbs cxt ty) = (foldMap go_tvb tvbs <> go ty <> foldMap go_pred cxt)
                                S.\\ S.fromList (map tvbName tvbs)
     go (AppT t1 t2)          = go t1 <> go t2
-    go (SigT ty _)           = go ty
+    go (SigT ty ki)          = go ty <> go ki
     go (VarT n)              = S.singleton n
     go _                     = S.empty
 
@@ -236,6 +243,9 @@
     go_pred (EqualP t1 t2) = go t1 <> go t2
 #endif
 
+    go_tvb (PlainTV{})    = S.empty
+    go_tvb (KindedTV _ k) = go k
+
 ----------------------------------------
 -- General utility
 ----------------------------------------
@@ -264,6 +274,19 @@
   return $ fold bss
 
 -- like GHC's
+-- | Monadic version of mapAccumL
+mapAccumLM :: Monad m
+            => (acc -> x -> m (acc, y)) -- ^ combining function
+            -> acc                      -- ^ initial state
+            -> [x]                      -- ^ inputs
+            -> m (acc, [y])             -- ^ final state, outputs
+mapAccumLM _ s []     = return (s, [])
+mapAccumLM f s (x:xs) = do
+    (s1, x')  <- f s x
+    (s2, xs') <- mapAccumLM f s1 xs
+    return    (s2, x' : xs')
+
+-- like GHC's
 mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
 mapMaybeM _ [] = return []
 mapMaybeM f (x:xs) = do
@@ -290,3 +313,9 @@
 topEverywhereM :: (Typeable a, Data b, Monad m) => (a -> m a) -> b -> m b
 topEverywhereM handler =
   gmapM (topEverywhereM handler) `extM` handler
+
+-- Checks if a String names a valid Haskell infix data constructor
+-- (i.e., does it begin with a colon?).
+isInfixDataCon :: String -> Bool
+isInfixDataCon (':':_) = True
+isInfixDataCon _ = False
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,7 +1,8 @@
 `th-desugar` Package
 ====================
 
-[![Build Status](https://travis-ci.org/goldfirere/th-desugar.png?branch=master)](https://travis-ci.org/goldfirere/th-desugar)
+[![Hackage](https://img.shields.io/hackage/v/th-desugar.svg)](http://hackage.haskell.org/package/th-desugar)
+[![Build Status](https://travis-ci.org/goldfirere/th-desugar.svg?branch=master)](https://travis-ci.org/goldfirere/th-desugar)
 
 This package provides the `Language.Haskell.TH.Desugar` module, which desugars
 Template Haskell's rich encoding of Haskell syntax into a simpler encoding.
diff --git a/Test/Dec.hs b/Test/Dec.hs
--- a/Test/Dec.hs
+++ b/Test/Dec.hs
@@ -39,6 +39,11 @@
 #endif
 $(S.dectest12)
 $(S.dectest13)
+$(S.dectest14)
+
+#if __GLASGOW_HASKELL__ >= 710
+$(S.dectest15)
+#endif
 
 $(fmap unqualify S.instance_test)
 
diff --git a/Test/DsDec.hs b/Test/DsDec.hs
--- a/Test/DsDec.hs
+++ b/Test/DsDec.hs
@@ -68,7 +68,12 @@
 
 $(dsDecSplice S.dectest12)
 $(dsDecSplice S.dectest13)
+$(dsDecSplice S.dectest14)
 
+#if __GLASGOW_HASKELL__ >= 710
+$(dsDecSplice S.dectest15)
+#endif
+
 $(do decs <- S.rec_sel_test
      [DDataD nd [] name [DPlainTV tvbName] cons []] <- dsDecs decs
      let arg_ty = (DConT name) `DAppT` (DVarT tvbName)
@@ -83,6 +88,6 @@
            let (_names, stricts, types) = unzip3 fields
                fields' = zip stricts types
            in
-           DCon tvbs cxt con_name (DNormalC fields') rty
+           DCon tvbs cxt con_name (DNormalC False fields') rty
          plaindata = [DDataD nd [] name [DPlainTV tvbName] (map unrecord cons) []]
      return (decsToTH plaindata ++ mapMaybe letDecToTH recsels))
diff --git a/Test/Run.hs b/Test/Run.hs
--- a/Test/Run.hs
+++ b/Test/Run.hs
@@ -5,13 +5,14 @@
 -}
 
 {-# LANGUAGE TemplateHaskell, UnboxedTuples, ParallelListComp, CPP,
-             RankNTypes, ImpredicativeTypes, TypeFamilies,
+             RankNTypes, TypeFamilies,
              DataKinds, ConstraintKinds, PolyKinds, MultiParamTypeClasses,
              FlexibleInstances, ExistentialQuantification,
              ScopedTypeVariables, GADTs, ViewPatterns #-}
 {-# OPTIONS -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns
             -fno-warn-unused-matches -fno-warn-type-defaults
-            -fno-warn-missing-signatures -fno-warn-unused-do-bind #-}
+            -fno-warn-missing-signatures -fno-warn-unused-do-bind
+            -fno-warn-missing-fields #-}
 
 #if __GLASGOW_HASKELL__ >= 711
 {-# LANGUAGE PartialTypeSignatures #-}
@@ -43,6 +44,10 @@
 import Control.Applicative
 #endif
 
+import Data.Generics ( geq )
+import Data.Function ( on )
+import qualified Data.Map as M
+import qualified Data.Set as S
 #if __GLASGOW_HASKELL__ >= 707
 import Data.Proxy
 #endif
@@ -117,6 +122,12 @@
              , "scoped_tvs" ~: $test42_scoped_tvs @=? $(dsSplice test42_scoped_tvs)
              , "ubx_sums"   ~: $test43_ubx_sums   @=? $(dsSplice test43_ubx_sums)
 #endif
+             , "let_pragma" ~: $test44_let_pragma @=? $(dsSplice test44_let_pragma)
+--             , "empty_rec"  ~: $test45_empty_record_con @=? $(dsSplice test45_empty_record_con)
+        -- This one can't be tested by this means, because it contains an "undefined"
+#if __GLASGOW_HASKELL__ >= 803
+             , "over_label" ~: $test46_overloaded_label @=? $(dsSplice test46_overloaded_label)
+#endif
              ]
 
 test35a = $test35_expand
@@ -228,6 +239,62 @@
 test_deriving_strategies = True
 #endif
 
+test_local_tyfam_expansion :: Bool
+test_local_tyfam_expansion =
+  $(do fam_name <- newName "Fam"
+       let orig_ty = DConT fam_name
+       exp_ty <- withLocalDeclarations
+                   (decsToTH [ DOpenTypeFamilyD (DTypeFamilyHead fam_name [] DNoSig Nothing)
+                             , DTySynInstD fam_name (DTySynEqn [] (DConT ''Int)) ])
+                   (expandType orig_ty)
+       orig_ty `eqTHSplice` exp_ty)
+
+test_kind_substitution :: [Bool]
+test_kind_substitution =
+  $(do a <- newName "a"
+       b <- newName "b"
+       c <- newName "c"
+       let subst = M.singleton a (DVarT b)
+
+                 -- (Nothing :: Maybe a)
+           ty1 = DSigT (DConT 'Nothing) (DConT ''Maybe `DAppT` DVarT a)
+                 -- forall (c :: a). c
+           ty2 = DForallT [DKindedTV c (DVarT a)] [] (DVarT c)
+                 -- forall a (c :: a). c
+           ty3 = DForallT [DPlainTV a, DKindedTV c (DVarT a)] [] (DVarT c)
+
+       substTy1 <- substTy subst ty1
+       substTy2 <- substTy subst ty2
+       substTy3 <- substTy subst ty3
+
+       let freeVars1 = fvDType substTy1
+           freeVars2 = fvDType substTy2
+           freeVars3 = fvDType substTy3
+
+           b1 = freeVars1 `eqTH` S.singleton b
+           b2 = freeVars2 `eqTH` S.singleton b
+           b3 = freeVars3 `eqTH` S.empty
+       [| [b1, b2, b3] |])
+
+test_lookup_value_type_names :: [Bool]
+test_lookup_value_type_names =
+  $(do let nameStr = "***"
+       valName  <- newName nameStr
+       typeName <- newName nameStr
+       let tyDec = DTySynD typeName [] (DConT ''Bool)
+           decs  = decsToTH [ DLetDec (DSigD valName (DConT ''Bool))
+                            , DLetDec (DValD (DVarPa valName) (DConE 'False))
+                            , tyDec ]
+           lookupReify lookup_fun = withLocalDeclarations decs $ do
+                                      Just n <- lookup_fun nameStr
+                                      Just i <- dsReify n
+                                      return i
+       reifiedVal  <- lookupReify lookupValueNameWithLocals
+       reifiedType <- lookupReify lookupTypeNameWithLocals
+       let b1 = reifiedVal  `eqTH` DVarI valName (DConT ''Bool) Nothing
+       let b2 = reifiedType `eqTH` DTyConI tyDec Nothing
+       [| [b1, b2] |])
+
 local_reifications :: [String]
 local_reifications = $(do decs <- reifyDecs
                           m_infos <- withLocalDeclarations decs $
@@ -267,6 +334,35 @@
                        let bools = zipWith eqTH ds_exprs2 ds_exprs3
                        Syn.lift bools )
 
+test_matchTy :: [Bool]
+test_matchTy =
+  [ matchTy NoIgnore (DVarT a) (DConT ''Bool) `eq` Just (M.singleton a (DConT ''Bool))
+  , matchTy NoIgnore (DVarT a) (DVarT a) `eq` Just (M.singleton a (DVarT a))
+  , matchTy NoIgnore (DVarT a) (DVarT b) `eq` Just (M.singleton a (DVarT b))
+  , matchTy NoIgnore (DConT ''Either `DAppT` DVarT a `DAppT` DVarT b)
+                     (DConT ''Either `DAppT` DConT ''Int `DAppT` DConT ''Bool)
+    `eq` Just (M.fromList [(a, DConT ''Int), (b, DConT ''Bool)])
+  , matchTy NoIgnore (DConT ''Either `DAppT` DVarT a `DAppT` DVarT a)
+                     (DConT ''Either `DAppT` DConT ''Int `DAppT` DConT ''Int)
+    `eq` Just (M.singleton a (DConT ''Int))
+  , matchTy NoIgnore (DConT ''Either `DAppT` DVarT a `DAppT` DVarT a)
+                     (DConT ''Either `DAppT` DConT ''Int `DAppT` DConT ''Bool)
+    `eq` Nothing
+  , matchTy NoIgnore (DConT ''Int) (DConT ''Bool) `eq` Nothing
+  , matchTy NoIgnore (DConT ''Int) (DConT ''Int) `eq` Just M.empty
+  , matchTy NoIgnore (DConT ''Int) (DVarT a) `eq` Nothing
+  , matchTy NoIgnore (DVarT a `DSigT` DConT ''Bool) (DConT ''Int) `eq` Nothing
+  , matchTy YesIgnore (DVarT a `DSigT` DConT ''Bool) (DConT ''Int)
+    `eq` Just (M.singleton a (DConT ''Int))
+  ]
+  where
+    a = mkName "a"
+    b = mkName "b"
+
+     -- GHC 7.6 uses containers-0.5.0.0 which doesn't have a good Data instance
+     -- for Map. So we have to convert to lists before comparing.
+    eq = geq `on` fmap M.toList
+
 main :: IO ()
 main = hspec $ do
   describe "th-desugar library" $ do
@@ -295,8 +391,10 @@
 
     it "works with standalone deriving" $ test_standalone_deriving
 
-    it "workds with deriving strategies" $ test_deriving_strategies
+    it "works with deriving strategies" $ test_deriving_strategies
 
+    it "doesn't expand local type families" $ test_local_tyfam_expansion
+
     -- Remove map pprints here after switch to th-orphans
     zipWithM (\t t' -> it ("can do Type->DType->Type of " ++ t) $ t == t')
              $(sequence round_trip_types >>= Syn.lift . map pprint)
@@ -310,5 +408,14 @@
     zipWithM (\b n -> it ("works on simplCase test " ++ show n) b) simplCase [1..]
 
     zipWithM (\b n -> it ("round-trip successfully on case " ++ show n) b) test_roundtrip [1..]
+
+    zipWithM (\b n -> it ("lookups up local value and type names " ++ show n) b)
+      test_lookup_value_type_names [1..]
+
+    zipWithM (\b n -> it ("substitutes tyvar binder kinds " ++ show n) b)
+      test_kind_substitution [1..]
+
+    zipWithM (\b n -> it ("matches types " ++ show n) b)
+      test_matchTy [1..]
 
     fromHUnitTest tests
diff --git a/Test/Splices.hs b/Test/Splices.hs
--- a/Test/Splices.hs
+++ b/Test/Splices.hs
@@ -21,6 +21,11 @@
 {-# LANGUAGE UnboxedSums #-}
 #endif
 
+#if __GLASGOW_HASKELL__ >= 803
+{-# LANGUAGE OverloadedLabels #-}
+{-# OPTIONS_GHC -Wno-orphans #-}  -- IsLabel is an orphan
+#endif
+
 {-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-type-defaults
                 -fno-warn-name-shadowing #-}
 
@@ -35,6 +40,10 @@
 import Language.Haskell.TH.Desugar
 import Data.Generics
 
+#if __GLASGOW_HASKELL__ >= 803
+import GHC.OverloadedLabels ( IsLabel(..) )
+#endif
+
 #if __GLASGOW_HASKELL__ < 707
 data Proxy a = Proxy
 #endif
@@ -243,7 +252,30 @@
                            {-# INLINE x #-}
                        in x |]
 
+test45_empty_record_con = [| let j :: Maybe Int
+                                 j = Just{}
+                             in case j of
+                                Nothing -> j
+                                Just{}  -> j |]
 
+#if __GLASGOW_HASKELL__ >= 803
+data Label (l :: Symbol) = Get
+
+class Has a l b | a l -> b where
+  from :: a -> Label l -> b
+
+data Point = Point Int Int deriving Show
+
+instance Has Point "x" Int where from (Point x _) _ = x
+instance Has Point "y" Int where from (Point _ y) _ = y
+
+instance Has a l b => IsLabel l (a -> b) where
+  fromLabel x = from x (Get :: Label l)
+
+test46_overloaded_label = [| let p = Point 3 4 in
+                             #x p - #y p |]
+#endif
+
 type family TFExpand x
 type instance TFExpand Int = Bool
 type instance TFExpand (Maybe a) = [a]
@@ -321,6 +353,10 @@
 dectest7 = [d| type family Dec7 a (b :: *) (c :: Bool) :: * -> * |]
 dectest8 = [d| type family Dec8 a |]
 dectest9 = [d| data family Dec9 a (b :: * -> *) :: * -> * |]
+  -- NB: dectest9 inexplicably fails when you don't recompile everything from
+  -- scratch. I (Richard) haven't explored why. The failure is benign (replacing the
+  -- decl above with one with three variables) so I'm not terribly bothered.
+
 #if __GLASGOW_HASKELL__ < 707
 ds_dectest10 = DClosedTypeFamilyD
                  (DTypeFamilyHead
@@ -365,6 +401,16 @@
                   MkDec13 :: c a => a -> Dec13 c
               |]
 
+dectest14 = [d| data InfixADT = Int `InfixADT` Int |]
+
+dectest15 = [d| infixl 5 :**:, :&&:, :^^:, `ActuallyPrefix`
+                data InfixGADT a where
+                  (:**:) :: Int -> b -> InfixGADT (Maybe b) -- Only this one is infix
+                  (:&&:) :: { infixGADT1 :: b, infixGADT2 :: Int } -> InfixGADT [b]
+                  ActuallyPrefix :: Char -> Bool -> InfixGADT Double
+                  (:^^:) :: Int -> Int -> Int -> InfixGADT Int
+                  (:!!:) :: Char -> Char -> InfixGADT Char |]
+
 instance_test = [d| instance (Show a, Show b) => Show (a -> b) where
                        show _ = "function" |]
 
@@ -584,4 +630,8 @@
              , test43_ubx_sums
 #endif
              , test44_let_pragma
+             , test45_empty_record_con
+#if __GLASGOW_HASKELL__ >= 803
+             , test46_overloaded_label
+#endif
              ]
diff --git a/th-desugar.cabal b/th-desugar.cabal
--- a/th-desugar.cabal
+++ b/th-desugar.cabal
@@ -1,5 +1,5 @@
 name:           th-desugar
-version:        1.7
+version:        1.8
 cabal-version:  >= 1.10
 synopsis:       Functions to desugar Template Haskell
 homepage:       https://github.com/goldfirere/th-desugar
@@ -12,6 +12,9 @@
 license:        BSD3
 license-file:   LICENSE
 build-type:     Simple
+tested-with:    GHC == 7.6.3, GHC == 7.8.2, GHC == 7.8.3, GHC == 7.8.4,
+                GHC == 7.10.1, GHC == 7.10.2, GHC == 7.10.3, GHC == 8.0.1,
+                GHC == 8.0.2, GHC == 8.2.1, GHC == 8.2.2, GHC == 8.4.1
 description:
     This package provides the Language.Haskell.TH.Desugar module, which desugars
     Template Haskell's rich encoding of Haskell syntax into a simpler encoding.
@@ -26,7 +29,7 @@
 source-repository this
   type:     git
   location: https://github.com/goldfirere/th-desugar.git
-  tag:      v1.7
+  tag:      v1.8
 
 library
   build-depends:
@@ -42,7 +45,8 @@
   exposed-modules:    Language.Haskell.TH.Desugar,
                       Language.Haskell.TH.Desugar.Sweeten,
                       Language.Haskell.TH.Desugar.Lift,
-                      Language.Haskell.TH.Desugar.Expand
+                      Language.Haskell.TH.Desugar.Expand,
+                      Language.Haskell.TH.Desugar.Subst
   other-modules:      Language.Haskell.TH.Desugar.Core,
                       Language.Haskell.TH.Desugar.Match,
                       Language.Haskell.TH.Desugar.Util,