diff --git a/.hlint.yaml b/.hlint.yaml
new file mode 100644
--- /dev/null
+++ b/.hlint.yaml
@@ -0,0 +1,4 @@
+- arguments: [--cpp-define=HLINT, --cpp-ansi]
+
+- ignore: {name: Use camelCase}
+- ignore: {name: Eta reduce}
diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
--- a/.travis.yml
+++ /dev/null
@@ -1,1 +0,0 @@
-language: haskell
diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,112 @@
+0.8.10 [2025.12.07]
+-------------------
+* Deprecate `Data.Proxy.TH.{pr,pr1}`, as their functionality has been subsumed
+  by using `Proxy` with `TypeApplications` syntax. For instance, uses of
+  `[pr|T|]` should be migrated to `Proxy @T`. `Data.Proxy.TH` will be removed
+  in the next `tagged` release.
+* Allow disabling the `template-haskell` dependency by disabling a `cabal` flag
+  of the same name.
+* Support building with MicroHs.
+
+0.8.9 [2024.12.03]
+------------------
+* Allow building with GHC 9.12.
+* Drop support for GHC 7.10 and earlier.
+
+0.8.8 [2023.08.08]
+------------------
+* Allow building with GHC 9.8.
+
+0.8.7 [2023.02.18]
+------------------
+* Define `Foldable1` and `Bifoldable1` instances for `Tagged`. These instances
+  were originally defined in the `semigroupoids` library, and they have now
+  been migrated to `tagged` as a side effect of adapting to
+  [this Core Libraries Proposal](https://github.com/haskell/core-libraries-committee/issues/9),
+  which adds `Foldable1` and `Bifoldable1` to `base`.
+
+0.8.6.1 [2020.12.28]
+--------------------
+* Mark all modules as explicitly Safe or Trustworthy.
+
+0.8.6 [2018.07.02]
+------------------
+* Make the `Read(1)` instances for `Proxy` ignore the precedence argument,
+  mirroring similar changes to `base`
+  [here](http://git.haskell.org/ghc.git/commitdiff/8fd959998e900dffdb7f752fcd42df7aaedeae6e).
+* Fix a bug in the `Floating` instance for `Tagged` in which `logBase` was
+  defined in terms of `(**)`.
+* Avoid incurring some dependencies when using recent GHCs.
+
+0.8.5
+-----
+* Support `Data.Bifoldable`/`Data.Bitraversable` in `base` for GHC 8.1+.
+* Backport the `Eq1`, `Ord1`, `Read1`, and `Show1` instances for `Proxy` from `base-4.9`
+* Add `Eq1`/`2`, `Ord1`/`2`, `Read1`/`2`, and `Show1`/`2` instances for `Tagged`
+
+0.8.4
+-----
+* Backport the `Alternative`, `MonadPlus`, and `MonadZip` instances for `Proxy` from `base-4.9`
+* Add `Bits`, `FiniteBits`, `IsString`, and `Storable` instances for `Tagged`
+
+0.8.3
+-----
+* Manual `Generic1` support to work around a bug in GHC 7.6
+* Invert the dependency to supply the `Semigroup` instance ourselves when building on GHC 8
+
+0.8.2
+-------
+* `deepseq` support.
+* Widened `template-haskell` dependency bounds.
+
+0.8.1
+-----
+* Add `KProxy` to the backwards compatibility `Data.Proxy` module.
+* Add a `Generic` instance to `Proxy`.
+
+0.8.0.1
+-------
+* Fix builds on GHC 7.4.
+
+0.8
+---
+* Added `Data.Proxy.TH`, based on the code from `Frames` by Anthony Cowley.
+* Removed `reproxy` from `Data.Proxy`. This is a bad API decision, but it isn't present in GHC's `Data.Proxy`, and this makes the API more stable.
+
+0.7.3
+---
+* Support `Data.Bifunctor` in `base` for GHC 7.9+.
+
+0.7.2
+-----
+* Fixed warning on GHC 7.8
+
+0.7.1
+-----
+* Added `tagWith`.
+
+0.7
+---
+* `Data.Proxy` has moved into base as of GHC 7.7 for use in the new `Data.Typeable`. We no longer export
+  it for GHC >= 7.7. The most notable change in the module from the migration into base is the loss of
+  the `reproxy` function.
+
+0.6.2
+-----
+* Allowed polymorphic arguments where possible.
+
+0.6.1
+-----
+* Needlessly claim that this entirely pure package is `Trustworthy`!
+
+0.6
+---
+* On GHC 7.7, we now still export the instances we used to for `Data.Proxy.Proxy` as orphans if need be.
+
+0.5
+---
+* On GHC 7.7 we now simply export `Data.Typeable.Proxy` rather than make our own type. We still re-export it.
+
 0.4.5
 -----
 * Added `witness`
diff --git a/Data/Proxy.hs b/Data/Proxy.hs
deleted file mode 100644
--- a/Data/Proxy.hs
+++ /dev/null
@@ -1,189 +0,0 @@
-{-# LANGUAGE CPP #-}
-#ifdef LANGUAGE_DeriveDataTypeable
-{-# LANGUAGE DeriveDataTypeable #-}
-#endif
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 706
-{-# LANGUAGE PolyKinds #-}
-#endif
-----------------------------------------------------------------------------
--- |
--- Module     : Data.Proxy
--- Copyright  : 2009-2012 Edward Kmett
--- License    : BSD3
---
--- Maintainer  : Edward Kmett <ekmett@gmail.com>
--- Stability   : experimental
--- Portability : portable
---
--------------------------------------------------------------------------------
-module Data.Proxy
-    (
-    -- * Tagged values
-      Proxy(..)
-    , reproxy
-    , asProxyTypeOf
-    -- * Conversion
-    , proxy
-    , unproxy
-    ) where
-
-import Control.Applicative (Applicative(..))
-import Data.Traversable (Traversable(..))
-import Data.Foldable (Foldable(..))
-import Data.Ix (Ix(..))
-import Data.Tagged
-import Data.Monoid
-#ifdef __GLASGOW_HASKELL__
-import GHC.Arr (unsafeIndex, unsafeRangeSize)
-import Data.Data
-#endif
-
-data Proxy s = Proxy
-
-instance Eq (Proxy s) where
-  _ == _ = True
-
-instance Ord (Proxy s) where
-  compare _ _ = EQ
-
-instance Show (Proxy s) where
-  showsPrec _ _ = showString "Proxy"
-
-instance Read (Proxy s) where
-  readsPrec d = readParen (d > 10) (\r -> [(Proxy, s) | ("Proxy",s) <- lex r ])
-
-#ifdef __GLASGOW_HASKELL__
-
-instance Typeable1 Proxy where
-  typeOf1 _ = mkTyConApp proxyTyCon []
-
-proxyTyCon :: TyCon
-#if __GLASGOW_HASKELL__ < 704
-proxyTyCon = mkTyCon "Data.Proxy.Proxy"
-#else
-proxyTyCon = mkTyCon3 "tagged" "Data.Proxy" "Proxy"
-#endif
-{-# NOINLINE proxyTyCon #-}
-
-instance Data s => Data (Proxy s) where
-  gfoldl _ z _ = z Proxy
-  toConstr _ = proxyConstr
-  gunfold _ z c = case constrIndex c of
-    1 -> z Proxy
-    _ -> error "gunfold"
-  dataTypeOf _ = proxyDataType
-  dataCast1 f = gcast1 f
-
-proxyConstr :: Constr
-proxyConstr = mkConstr proxyDataType "Proxy" [] Prefix
-{-# NOINLINE proxyConstr #-}
-
-proxyDataType :: DataType
-proxyDataType = mkDataType "Data.Proxy.Proxy" [proxyConstr]
-{-# NOINLINE proxyDataType #-}
-#endif
-
-instance Enum (Proxy s) where
-    succ _ = error "Proxy.succ"
-    pred _ = error "Proxy.pred"
-    fromEnum _ = 0
-    toEnum 0 = Proxy
-    toEnum _ = error "Proxy.toEnum: 0 expected"
-    enumFrom _ = [Proxy]
-    enumFromThen _ _ = [Proxy]
-    enumFromThenTo _ _ _ = [Proxy]
-    enumFromTo _ _ = [Proxy]
-
-instance Ix (Proxy s) where
-    range _ = [Proxy]
-    index _ _ = 0
-    inRange _ _ = True
-    rangeSize _ = 1
-#ifdef __GLASGOW_HASKELL__
-    unsafeIndex _ _ = 0
-    unsafeRangeSize _ = 1
-#endif
-
-instance Bounded (Proxy s) where
-    minBound = Proxy
-    maxBound = Proxy
-
-instance Functor Proxy where
-    fmap _ _ = Proxy
-    {-# INLINE fmap #-}
-
-instance Applicative Proxy where
-    pure _ = Proxy
-    {-# INLINE pure #-}
-    _ <*> _ = Proxy
-    {-# INLINE (<*>) #-}
-
-instance Monoid (Proxy s) where
-    mempty = Proxy
-    {-# INLINE mempty #-}
-    mappend _ _ = Proxy
-    {-# INLINE mappend #-}
-    mconcat _ = Proxy
-    {-# INLINE mconcat #-}
-
-instance Monad Proxy where
-    return _ = Proxy
-    {-# INLINE return #-}
-    _ >>= _ = Proxy
-    {-# INLINE (>>=) #-}
-
-instance Foldable Proxy where
-    foldMap _ _ = mempty
-    {-# INLINE foldMap #-}
-    fold _ = mempty
-    {-# INLINE fold #-}
-    foldr _ z _ = z
-    {-# INLINE foldr #-}
-    foldl _ z _ = z
-    {-# INLINE foldl #-}
-    foldl1 _ _ = error "foldl1: Proxy"
-    {-# INLINE foldl1 #-}
-    foldr1 _ _ = error "foldr1: Proxy"
-    {-# INLINE foldr1 #-}
-
-instance Traversable Proxy where
-    traverse _ _ = pure Proxy
-    {-# INLINE traverse #-}
-    sequenceA _ = pure Proxy
-    {-# INLINE sequenceA #-}
-    mapM _ _ = return Proxy
-    {-# INLINE mapM #-}
-    sequence _ = return Proxy
-    {-# INLINE sequence #-}
-
--- | Some times you need to change the proxy you have lying around.
--- Idiomatic usage is to make a new combinator for the relationship
--- between the proxies that you want to enforce, and define that
--- combinator using 'reproxy'.
---
--- > data Succ n
--- > reproxySucc :: Proxy n -> Proxy (Succ n)
--- > reproxySucc = reproxy
-reproxy :: Proxy s -> Proxy t
-reproxy _ = Proxy
-{-# INLINE reproxy #-}
-
--- | Convert from a 'Tagged' representation to a representation
--- based on a 'Proxy'.
-proxy :: Tagged s a -> Proxy s -> a
-proxy (Tagged x) _ = x
-{-# INLINE proxy #-}
-
--- | Convert from a representation based on a 'Proxy' to a 'Tagged'
--- representation.
-unproxy :: (Proxy s -> a) -> Tagged s a
-unproxy f = Tagged (f Proxy)
-{-# INLINE unproxy #-}
-
--- | 'asProxyTypeOf' is a type-restricted version of 'const'.
--- It is usually used as an infix operator, and its typing forces its first
--- argument (which is usually overloaded) to have the same type as the tag
--- of the second.
-asProxyTypeOf :: a -> Proxy a -> a
-asProxyTypeOf = const
-{-# INLINE asProxyTypeOf #-}
diff --git a/Data/Tagged.hs b/Data/Tagged.hs
deleted file mode 100644
--- a/Data/Tagged.hs
+++ /dev/null
@@ -1,255 +0,0 @@
-{-# LANGUAGE CPP #-}
-#ifdef LANGUAGE_DeriveDataTypeable
-{-# LANGUAGE DeriveDataTypeable #-}
-#endif
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 706
-{-# LANGUAGE PolyKinds #-}
-#endif
-----------------------------------------------------------------------------
--- |
--- Module     : Data.Tagged
--- Copyright  : 2009-2012 Edward Kmett
--- License    : BSD3
---
--- Maintainer  : Edward Kmett <ekmett@gmail.com>
--- Stability   : experimental
--- Portability : portable
---
--------------------------------------------------------------------------------
-
-module Data.Tagged
-    (
-    -- * Tagged values
-      Tagged(..)
-    , retag
-    , untag
-    , tagSelf
-    , untagSelf
-    , asTaggedTypeOf
-    , witness
-    ) where
-
-import Control.Applicative ((<$>), liftA2, Applicative(..))
-import Control.Monad (liftM)
-import Data.Traversable (Traversable(..))
-import Data.Foldable (Foldable(..))
-#ifdef __GLASGOW_HASKELL__
-import Data.Data
-#endif
-import Data.Ix (Ix(..))
-import Data.Monoid
-
--- | A @'Tagged' s b@ value is a value @b@ with an attached phantom type @s@.
--- This can be used in place of the more traditional but less safe idiom of
--- passing in an undefined value with the type, because unlike an @(s -> b)@,
--- a @'Tagged' s b@ can't try to use the argument @s@ as a real value.
---
--- Moreover, you don't have to rely on the compiler to inline away the extra
--- argument, because the newtype is \"free\"
-newtype Tagged s b = Tagged { unTagged :: b } deriving
-  ( Eq, Ord, Ix, Bounded
-  )
-
-#ifdef __GLASGOW_HASKELL__
-instance Typeable2 Tagged where
-  typeOf2 _ = mkTyConApp taggedTyCon []
-
-taggedTyCon :: TyCon
-#if __GLASGOW_HASKELL__ < 704
-taggedTyCon = mkTyCon "Data.Tagged.Tagged"
-#else
-taggedTyCon = mkTyCon3 "tagged" "Data.Tagged" "Tagged"
-#endif
-
-instance (Data s, Data b) => Data (Tagged s b) where
-  gfoldl f z (Tagged b) = z Tagged `f` b
-  toConstr _ = taggedConstr
-  gunfold k z c = case constrIndex c of
-    1 -> k (z Tagged)
-    _ -> error "gunfold"
-  dataTypeOf _ = taggedDataType
-  dataCast1 f = gcast1 f
-  dataCast2 f = gcast2 f
-
-taggedConstr :: Constr
-taggedConstr = mkConstr taggedDataType "Tagged" [] Prefix
-{-# INLINE taggedConstr #-}
-
-taggedDataType :: DataType
-taggedDataType = mkDataType "Data.Tagged.Tagged" [taggedConstr]
-{-# INLINE taggedDataType #-}
-#endif
-
-instance Show b => Show (Tagged s b) where
-    showsPrec n (Tagged b) = showParen (n > 10) $
-        showString "Tagged " .
-        showsPrec 11 b
-
-instance Read b => Read (Tagged s b) where
-    readsPrec d = readParen (d > 10) $ \r ->
-        [(Tagged a, t) | ("Tagged", s) <- lex r, (a, t) <- readsPrec 11 s]
-
-instance Monoid a => Monoid (Tagged s a) where
-    mempty = Tagged mempty
-    mappend (Tagged a) (Tagged b) = Tagged (mappend a b)
-
-instance Functor (Tagged s) where
-    fmap f (Tagged x) = Tagged (f x)
-    {-# INLINE fmap #-}
-
-instance Applicative (Tagged s) where
-    pure = Tagged
-    {-# INLINE pure #-}
-    Tagged f <*> Tagged x = Tagged (f x)
-    {-# INLINE (<*>) #-}
-
-instance Monad (Tagged s) where
-    return = Tagged
-    {-# INLINE return #-}
-    Tagged m >>= k = k m
-    {-# INLINE (>>=) #-}
-    _ >> n = n
-    {-# INLINE (>>) #-}
-
-instance Foldable (Tagged s) where
-    foldMap f (Tagged x) = f x
-    {-# INLINE foldMap #-}
-    fold (Tagged x) = x
-    {-# INLINE fold #-}
-    foldr f z (Tagged x) = f x z
-    {-# INLINE foldr #-}
-    foldl f z (Tagged x) = f z x
-    {-# INLINE foldl #-}
-    foldl1 _ (Tagged x) = x
-    {-# INLINE foldl1 #-}
-    foldr1 _ (Tagged x) = x
-    {-# INLINE foldr1 #-}
-
-instance Traversable (Tagged s) where
-    traverse f (Tagged x) = Tagged <$> f x
-    {-# INLINE traverse #-}
-    sequenceA (Tagged x) = Tagged <$> x
-    {-# INLINE sequenceA #-}
-    mapM f (Tagged x) = liftM Tagged (f x)
-    {-# INLINE mapM #-}
-    sequence (Tagged x) = liftM Tagged x
-    {-# INLINE sequence #-}
-
-instance Enum a => Enum (Tagged s a) where
-    succ = fmap succ
-    pred = fmap pred
-    toEnum = Tagged . toEnum
-    fromEnum (Tagged x) = fromEnum x
-    enumFrom (Tagged x) = map Tagged (enumFrom x)
-    enumFromThen (Tagged x) (Tagged y) = map Tagged (enumFromThen x y)
-    enumFromTo (Tagged x) (Tagged y) = map Tagged (enumFromTo x y)
-    enumFromThenTo (Tagged x) (Tagged y) (Tagged z) =
-        map Tagged (enumFromThenTo x y z)
-
-instance Num a => Num (Tagged s a) where
-    (+) = liftA2 (+)
-    (-) = liftA2 (-)
-    (*) = liftA2 (*)
-    negate = fmap negate
-    abs = fmap abs
-    signum = fmap signum
-    fromInteger = Tagged . fromInteger
-
-instance Real a => Real (Tagged s a) where
-    toRational (Tagged x) = toRational x
-
-instance Integral a => Integral (Tagged s a) where
-    quot = liftA2 quot
-    rem = liftA2 rem
-    div = liftA2 div
-    mod = liftA2 mod
-    quotRem (Tagged x) (Tagged y) = (Tagged a, Tagged b) where
-        (a, b) = quotRem x y
-    divMod (Tagged x) (Tagged y) = (Tagged a, Tagged b) where
-        (a, b) = divMod x y
-    toInteger (Tagged x) = toInteger x
-
-instance Fractional a => Fractional (Tagged s a) where
-    (/) = liftA2 (/)
-    recip = fmap recip
-    fromRational = Tagged . fromRational
-
-instance Floating a => Floating (Tagged s a) where
-    pi = Tagged pi
-    exp = fmap exp
-    log = fmap log
-    sqrt = fmap sqrt
-    sin = fmap sin
-    cos = fmap cos
-    tan = fmap tan
-    asin = fmap asin
-    acos = fmap acos
-    atan = fmap atan
-    sinh = fmap sinh
-    cosh = fmap cosh
-    tanh = fmap tanh
-    asinh = fmap asinh
-    acosh = fmap acosh
-    atanh = fmap atanh
-    (**) = liftA2 (**)
-    logBase = liftA2 (**)
-
-instance RealFrac a => RealFrac (Tagged s a) where
-    properFraction (Tagged x) = (a, Tagged b) where
-        (a, b) = properFraction x
-    truncate (Tagged x) = truncate x
-    round (Tagged x) = round x
-    ceiling (Tagged x) = ceiling x
-    floor (Tagged x) = floor x
-
-instance RealFloat a => RealFloat (Tagged s a) where
-    floatRadix (Tagged x) = floatRadix x
-    floatDigits (Tagged x) = floatDigits x
-    floatRange (Tagged x) = floatRange x
-    decodeFloat (Tagged x) = decodeFloat x
-    encodeFloat m n = Tagged (encodeFloat m n)
-    exponent (Tagged x) = exponent x
-    significand = fmap significand
-    scaleFloat n = fmap (scaleFloat n)
-    isNaN (Tagged x) = isNaN x
-    isInfinite (Tagged x) = isInfinite x
-    isDenormalized (Tagged x) = isDenormalized x
-    isNegativeZero (Tagged x) = isNegativeZero x
-    isIEEE (Tagged x) = isIEEE x
-    atan2 = liftA2 atan2
-
--- | Some times you need to change the tag you have lying around.
--- Idiomatic usage is to make a new combinator for the relationship between the
--- tags that you want to enforce, and define that combinator using 'retag'.
---
--- @
--- data Succ n
--- retagSucc :: 'Tagged' n a -> 'Tagged' (Succ n) a
--- retagSucc = 'retag'
--- @
-retag :: Tagged s b -> Tagged t b
-retag = Tagged . unTagged
-{-# INLINE retag #-}
-
--- | Alias for 'unTagged'
-untag :: Tagged s b -> b
-untag = unTagged
-
--- | Tag a value with its own type.
-tagSelf :: a -> Tagged a a
-tagSelf = Tagged
-{-# INLINE tagSelf #-}
-
--- | 'asTaggedTypeOf' is a type-restricted version of 'const'. It is usually used as an infix operator, and its typing forces its first argument (which is usually overloaded) to have the same type as the tag of the second.
-asTaggedTypeOf :: s -> Tagged s b -> s
-asTaggedTypeOf = const
-{-# INLINE asTaggedTypeOf #-}
-
-witness :: Tagged a b -> a -> b
-witness (Tagged b) _ = b
-{-# INLINE witness #-}
-
--- | 'untagSelf' is a type-restricted version of 'untag'.
-untagSelf :: Tagged a a -> a
-untagSelf (Tagged x) = x
-{-# INLINE untagSelf #-}
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2009-2011 Edward Kmett
+Copyright (c) 2009-2015 Edward Kmett
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without
diff --git a/README.markdown b/README.markdown
--- a/README.markdown
+++ b/README.markdown
@@ -1,4 +1,6 @@
 tagged
 ======
 
-Values carrying an extra [phantom type](http://www.haskell.org/haskellwiki/Phantom_type) tag. 
+[![Hackage](https://img.shields.io/hackage/v/tagged.svg)](https://hackage.haskell.org/package/tagged) [![Build Status](https://github.com/ekmett/tagged/workflows/Haskell-CI/badge.svg)](https://github.com/ekmett/tagged/actions?query=workflow%3AHaskell-CI)
+
+Values carrying an extra [phantom type](https://wiki.haskell.org/Phantom_type) tag.
diff --git a/src/Data/Proxy/TH.hs b/src/Data/Proxy/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Proxy/TH.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE TemplateHaskellQuotes #-}
+#ifndef MIN_VERSION_template_haskell
+#define MIN_VERSION_template_haskell(x,y,z) 1
+#endif
+-- template-haskell is only safe since GHC-8.2
+#if __GLASGOW_HASKELL__ >= 802
+{-# LANGUAGE Safe #-}
+#else
+{-# LANGUAGE Trustworthy #-}
+#endif
+module Data.Proxy.TH
+  ( pr
+  , pr1
+  ) where
+
+import Data.Char
+import Data.Proxy (Proxy(..))
+import Language.Haskell.TH
+import Language.Haskell.TH.Quote
+
+proxy_d, proxy_tc :: Name
+proxy_d  = 'Proxy
+proxy_tc = ''Proxy
+
+proxyTypeQ :: TypeQ -> TypeQ
+proxyTypeQ t = appT (conT proxy_tc) t
+
+proxyExpQ :: TypeQ -> ExpQ
+proxyExpQ t = sigE (conE proxy_d) (proxyTypeQ t)
+
+proxyPatQ :: TypeQ -> PatQ
+proxyPatQ t = sigP (conP proxy_d []) (proxyTypeQ t)
+
+-- | A proxy value quasiquoter. @[pr|T|]@ will splice an expression
+-- @Proxy::Proxy T@, while @[pr|A,B,C|]@ will splice in a value of
+-- @Proxy :: Proxy [A,B,C]@.
+
+-- TODO: parse a richer syntax for the types involved here so we can include spaces, applications, etc.
+{-# DEPRECATED
+      pr
+      [ "'pr' will be removed in the next release. Use 'Proxy' with @TypeApplications@ instead. "
+      , "Instead of using @[pr|T|]@, use @Proxy \\@T@ instead. "
+      , "Instead of using @[pr|A,B,C|]@, use @Proxy \\@[A,B,C]@ instead. "
+      ] #-}
+pr :: QuasiQuoter
+pr = QuasiQuoter (mkProxy proxyExpQ) (mkProxy proxyPatQ) (mkProxy proxyTypeQ) undefined where
+  mkProxy :: (TypeQ -> r) -> String -> r
+  mkProxy p s = case ts of
+    [h@(t:_)]
+       | isUpper t -> p $ conT $ mkName h
+       | otherwise -> p $ varT $ mkName h
+    _ -> p $ mkList <$> cons
+    where
+      ts = map strip $ splitOn ',' s
+      cons = mapM (conT . mkName) ts
+      mkList = foldr (AppT . AppT PromotedConsT) PromotedNilT
+
+-- | Like 'pr', but takes a single type, which is used to produce a
+-- 'Proxy' for a single-element list containing only that type. This
+-- is useful for passing a single type to a function that wants a list
+-- of types.
+
+-- TODO: parse a richer syntax for the types involved here so we can include spaces, applications, etc.
+{-# DEPRECATED
+      pr1
+      [ "'pr1' will be removed in the next release. Use 'Proxy' with @TypeApplications@ instead. "
+      , "Instead of using @[pr1|T|]@, use @Proxy \\@'[T]@ instead. "
+      ] #-}
+pr1 :: QuasiQuoter
+pr1 = QuasiQuoter (mkProxy proxyExpQ) (mkProxy proxyPatQ) (mkProxy proxyTypeQ) undefined where
+  sing x = AppT (AppT PromotedConsT x) PromotedNilT
+  mkProxy p s = case s of
+    t:_
+      | isUpper t -> p (fmap sing (conT $ mkName s))
+      | otherwise -> p (fmap sing (varT $ mkName s))
+    _ -> error "Empty string passed to pr1"
+
+-- | Split on a delimiter.
+splitOn :: Eq a => a -> [a] -> [[a]]
+splitOn d = go where
+  go [] = []
+  go xs = case t of
+      [] -> [h]
+      (_:t') -> h : go t'
+    where (h,t) = break (== d) xs
+
+-- | Remove white space from both ends of a 'String'.
+strip :: String -> String
+strip = takeWhile (not . isSpace) . dropWhile isSpace
diff --git a/src/Data/Tagged.hs b/src/Data/Tagged.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Tagged.hs
@@ -0,0 +1,425 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE Safe #-}
+
+{-# OPTIONS_GHC -Wno-deprecations #-}
+----------------------------------------------------------------------------
+-- |
+-- Module     : Data.Tagged
+-- Copyright  : 2009-2015 Edward Kmett
+-- License    : BSD3
+--
+-- Maintainer  : Edward Kmett <ekmett@gmail.com>
+-- Stability   : experimental
+-- Portability : portable
+--
+-------------------------------------------------------------------------------
+
+module Data.Tagged
+    (
+    -- * Tagged values
+      Tagged(..)
+    , retag
+    , untag
+    , tagSelf
+    , untagSelf
+    , asTaggedTypeOf
+    , witness
+    -- * Conversion
+    , proxy
+    , unproxy
+    , tagWith
+    -- * Proxy methods GHC dropped
+    , reproxy
+    ) where
+
+#if !(MIN_VERSION_base(4,18,0))
+import Control.Applicative (liftA2)
+#endif
+import Data.Bits
+import Data.Foldable (Foldable(..))
+#ifdef MIN_VERSION_deepseq
+import Control.DeepSeq (NFData(..))
+#endif
+import Data.Functor.Classes ( Eq1(..), Ord1(..), Read1(..), Show1(..)
+                            , Eq2(..), Ord2(..), Read2(..), Show2(..)
+                            )
+import Control.Monad (liftM)
+import Data.Bifunctor
+#if MIN_VERSION_base(4,10,0)
+import Data.Bifoldable (Bifoldable(..))
+import Data.Bitraversable (Bitraversable(..))
+#endif
+#if MIN_VERSION_base(4,18,0)
+import Data.Foldable1 (Foldable1(..))
+import Data.Bifoldable1 (Bifoldable1(..))
+#endif
+#ifdef __GLASGOW_HASKELL__
+import Data.Data
+#endif
+import Data.Ix (Ix(..))
+import Data.Semigroup (Semigroup(..))
+import Data.String (IsString(..))
+#ifdef __MHS__
+import Data.Traversable (Traversable(..))
+#endif
+import Foreign.Ptr (castPtr)
+import Foreign.Storable (Storable(..))
+#ifdef __GLASGOW_HASKELL__
+import GHC.Generics (Generic, Generic1)
+#endif
+
+-- | A @'Tagged' s b@ value is a value @b@ with an attached phantom type @s@.
+-- This can be used in place of the more traditional but less safe idiom of
+-- passing in an undefined value with the type, because unlike an @(s -> b)@,
+-- a @'Tagged' s b@ can't try to use the argument @s@ as a real value.
+--
+-- Moreover, you don't have to rely on the compiler to inline away the extra
+-- argument, because the newtype is \"free\"
+--
+-- 'Tagged' has kind @k -> * -> *@ if the compiler supports @PolyKinds@, therefore
+-- there is an extra @k@ showing in the instance haddocks that may cause confusion.
+newtype Tagged s b = Tagged { unTagged :: b }
+  deriving ( Eq, Ord, Ix, Bounded
+#ifdef __GLASGOW_HASKELL__
+           , Generic, Generic1
+#endif
+           )
+
+#ifdef __GLASGOW_HASKELL__
+instance (Data s, Data b) => Data (Tagged s b) where
+  gfoldl f z (Tagged b) = z Tagged `f` b
+  toConstr _ = taggedConstr
+  gunfold k z c = case constrIndex c of
+    1 -> k (z Tagged)
+    _ -> error "gunfold"
+  dataTypeOf _ = taggedDataType
+  dataCast1 f = gcast1 f
+  dataCast2 f = gcast2 f
+
+taggedConstr :: Constr
+taggedConstr = mkConstr taggedDataType "Tagged" [] Prefix
+{-# INLINE taggedConstr #-}
+
+taggedDataType :: DataType
+taggedDataType = mkDataType "Data.Tagged.Tagged" [taggedConstr]
+{-# INLINE taggedDataType #-}
+#endif
+
+instance Show b => Show (Tagged s b) where
+    showsPrec n (Tagged b) = showParen (n > 10) $
+        showString "Tagged " .
+        showsPrec 11 b
+
+instance Read b => Read (Tagged s b) where
+    readsPrec d = readParen (d > 10) $ \r ->
+        [(Tagged a, t) | ("Tagged", s) <- lex r, (a, t) <- readsPrec 11 s]
+
+instance Semigroup a => Semigroup (Tagged s a) where
+    Tagged a <> Tagged b = Tagged (a <> b)
+    stimes n (Tagged a)  = Tagged (stimes n a)
+
+instance (Semigroup a, Monoid a) => Monoid (Tagged s a) where
+    mempty = Tagged mempty
+    mappend = (<>)
+
+instance Functor (Tagged s) where
+    fmap f (Tagged x) = Tagged (f x)
+    {-# INLINE fmap #-}
+
+-- this instance is provided by the bifunctors package for GHC<7.9
+instance Bifunctor Tagged where
+    bimap _ g (Tagged b) = Tagged (g b)
+    {-# INLINE bimap #-}
+
+#if MIN_VERSION_base(4,10,0)
+-- these instances are provided by the bifunctors package for GHC<8.1
+instance Bifoldable Tagged where
+    bifoldMap _ g (Tagged b) = g b
+    {-# INLINE bifoldMap #-}
+
+instance Bitraversable Tagged where
+    bitraverse _ g (Tagged b) = Tagged <$> g b
+    {-# INLINE bitraverse #-}
+#endif
+
+#if MIN_VERSION_base(4,18,0)
+instance Foldable1 (Tagged a) where
+  foldMap1 f (Tagged a) = f a
+  {-# INLINE foldMap1 #-}
+
+instance Bifoldable1 Tagged where
+  bifoldMap1 _ g (Tagged b) = g b
+  {-# INLINE bifoldMap1 #-}
+#endif
+
+#ifdef MIN_VERSION_deepseq
+instance NFData b => NFData (Tagged s b) where
+    rnf (Tagged b) = rnf b
+#endif
+
+instance Eq1 (Tagged s) where
+    liftEq eq (Tagged a) (Tagged b) = eq a b
+
+instance Ord1 (Tagged s) where
+    liftCompare cmp (Tagged a) (Tagged b) = cmp a b
+
+instance Read1 (Tagged s) where
+    liftReadsPrec rp _ d = readParen (d > 10) $ \r ->
+        [(Tagged a, t) | ("Tagged", s) <- lex r, (a, t) <- rp 11 s]
+
+instance Show1 (Tagged s) where
+    liftShowsPrec sp _ n (Tagged b) = showParen (n > 10) $
+        showString "Tagged " .
+        sp 11 b
+
+instance Eq2 Tagged where
+    liftEq2 _ eq (Tagged a) (Tagged b) = eq a b
+
+instance Ord2 Tagged where
+    liftCompare2 _ cmp (Tagged a) (Tagged b) = cmp a b
+
+instance Read2 Tagged where
+    liftReadsPrec2 _ _ rp _ d = readParen (d > 10) $ \r ->
+        [(Tagged a, t) | ("Tagged", s) <- lex r, (a, t) <- rp 11 s]
+
+instance Show2 Tagged where
+    liftShowsPrec2 _ _ sp _ n (Tagged b) = showParen (n > 10) $
+        showString "Tagged " .
+        sp 11 b
+
+instance Applicative (Tagged s) where
+    pure = Tagged
+    {-# INLINE pure #-}
+    Tagged f <*> Tagged x = Tagged (f x)
+    {-# INLINE (<*>) #-}
+    _ *> n = n
+    {-# INLINE (*>) #-}
+
+instance Monad (Tagged s) where
+    return = pure
+    {-# INLINE return #-}
+    Tagged m >>= k = k m
+    {-# INLINE (>>=) #-}
+    (>>) = (*>)
+    {-# INLINE (>>) #-}
+
+instance Foldable (Tagged s) where
+    foldMap f (Tagged x) = f x
+    {-# INLINE foldMap #-}
+    fold (Tagged x) = x
+    {-# INLINE fold #-}
+    foldr f z (Tagged x) = f x z
+    {-# INLINE foldr #-}
+    foldl f z (Tagged x) = f z x
+    {-# INLINE foldl #-}
+    foldl1 _ (Tagged x) = x
+    {-# INLINE foldl1 #-}
+    foldr1 _ (Tagged x) = x
+    {-# INLINE foldr1 #-}
+
+instance Traversable (Tagged s) where
+    traverse f (Tagged x) = Tagged <$> f x
+    {-# INLINE traverse #-}
+    sequenceA (Tagged x) = Tagged <$> x
+    {-# INLINE sequenceA #-}
+    mapM f (Tagged x) = liftM Tagged (f x)
+    {-# INLINE mapM #-}
+    sequence (Tagged x) = liftM Tagged x
+    {-# INLINE sequence #-}
+
+instance Enum a => Enum (Tagged s a) where
+    succ = fmap succ
+    pred = fmap pred
+    toEnum = Tagged . toEnum
+    fromEnum (Tagged x) = fromEnum x
+    enumFrom (Tagged x) = map Tagged (enumFrom x)
+    enumFromThen (Tagged x) (Tagged y) = map Tagged (enumFromThen x y)
+    enumFromTo (Tagged x) (Tagged y) = map Tagged (enumFromTo x y)
+    enumFromThenTo (Tagged x) (Tagged y) (Tagged z) =
+        map Tagged (enumFromThenTo x y z)
+
+instance Num a => Num (Tagged s a) where
+    (+) = liftA2 (+)
+    (-) = liftA2 (-)
+    (*) = liftA2 (*)
+    negate = fmap negate
+    abs = fmap abs
+    signum = fmap signum
+    fromInteger = Tagged . fromInteger
+
+instance Real a => Real (Tagged s a) where
+    toRational (Tagged x) = toRational x
+
+instance Integral a => Integral (Tagged s a) where
+    quot = liftA2 quot
+    rem = liftA2 rem
+    div = liftA2 div
+    mod = liftA2 mod
+    quotRem (Tagged x) (Tagged y) = (Tagged a, Tagged b) where
+        (a, b) = quotRem x y
+    divMod (Tagged x) (Tagged y) = (Tagged a, Tagged b) where
+        (a, b) = divMod x y
+    toInteger (Tagged x) = toInteger x
+
+instance Fractional a => Fractional (Tagged s a) where
+    (/) = liftA2 (/)
+    recip = fmap recip
+    fromRational = Tagged . fromRational
+
+instance Floating a => Floating (Tagged s a) where
+    pi = Tagged pi
+    exp = fmap exp
+    log = fmap log
+    sqrt = fmap sqrt
+    sin = fmap sin
+    cos = fmap cos
+    tan = fmap tan
+    asin = fmap asin
+    acos = fmap acos
+    atan = fmap atan
+    sinh = fmap sinh
+    cosh = fmap cosh
+    tanh = fmap tanh
+    asinh = fmap asinh
+    acosh = fmap acosh
+    atanh = fmap atanh
+    (**) = liftA2 (**)
+    logBase = liftA2 logBase
+
+instance RealFrac a => RealFrac (Tagged s a) where
+    properFraction (Tagged x) = (a, Tagged b) where
+        (a, b) = properFraction x
+    truncate (Tagged x) = truncate x
+    round (Tagged x) = round x
+    ceiling (Tagged x) = ceiling x
+    floor (Tagged x) = floor x
+
+instance RealFloat a => RealFloat (Tagged s a) where
+    floatRadix (Tagged x) = floatRadix x
+    floatDigits (Tagged x) = floatDigits x
+    floatRange (Tagged x) = floatRange x
+    decodeFloat (Tagged x) = decodeFloat x
+    encodeFloat m n = Tagged (encodeFloat m n)
+    exponent (Tagged x) = exponent x
+    significand = fmap significand
+    scaleFloat n = fmap (scaleFloat n)
+    isNaN (Tagged x) = isNaN x
+    isInfinite (Tagged x) = isInfinite x
+    isDenormalized (Tagged x) = isDenormalized x
+    isNegativeZero (Tagged x) = isNegativeZero x
+    isIEEE (Tagged x) = isIEEE x
+    atan2 = liftA2 atan2
+
+instance Bits a => Bits (Tagged s a) where
+    Tagged a .&. Tagged b = Tagged (a .&. b)
+    Tagged a .|. Tagged b = Tagged (a .|. b)
+    xor (Tagged a) (Tagged b) = Tagged (xor a b)
+    complement (Tagged a) = Tagged (complement a)
+    shift (Tagged a) i = Tagged (shift a i)
+    shiftL (Tagged a) i = Tagged (shiftL a i)
+    shiftR (Tagged a) i = Tagged (shiftR a i)
+    rotate (Tagged a) i = Tagged (rotate a i)
+    rotateL (Tagged a) i = Tagged (rotateL a i)
+    rotateR (Tagged a) i = Tagged (rotateR a i)
+    bit i = Tagged (bit i)
+    setBit (Tagged a) i = Tagged (setBit a i)
+    clearBit (Tagged a) i = Tagged (clearBit a i)
+    complementBit (Tagged a) i = Tagged (complementBit a i)
+    testBit (Tagged a) i = testBit a i
+    isSigned (Tagged a) = isSigned a
+    bitSize (Tagged a) = bitSize a -- deprecated, but still required :(
+    unsafeShiftL (Tagged a) i = Tagged (unsafeShiftL a i)
+    unsafeShiftR (Tagged a) i = Tagged (unsafeShiftR a i)
+    popCount (Tagged a) = popCount a
+    bitSizeMaybe (Tagged a) = bitSizeMaybe a
+    zeroBits = Tagged zeroBits
+
+instance FiniteBits a => FiniteBits (Tagged s a) where
+    finiteBitSize (Tagged a) = finiteBitSize a
+    countLeadingZeros (Tagged a) = countLeadingZeros a
+    countTrailingZeros (Tagged a) = countTrailingZeros a
+
+instance IsString a => IsString (Tagged s a) where
+    fromString = Tagged . fromString
+
+instance Storable a => Storable (Tagged s a) where
+    sizeOf t = sizeOf a
+      where
+        Tagged a = Tagged undefined `asTypeOf` t
+    alignment t = alignment a
+      where
+        Tagged a = Tagged undefined `asTypeOf` t
+    peek ptr = Tagged <$> peek (castPtr ptr)
+    poke ptr (Tagged a) = poke (castPtr ptr) a
+    peekElemOff ptr i = Tagged <$> peekElemOff (castPtr ptr) i
+    pokeElemOff ptr i (Tagged a) = pokeElemOff (castPtr ptr) i a
+    peekByteOff ptr i = Tagged <$> peekByteOff (castPtr ptr) i
+    pokeByteOff ptr i (Tagged a) = pokeByteOff (castPtr ptr) i a
+
+-- | Some times you need to change the tag you have lying around.
+-- Idiomatic usage is to make a new combinator for the relationship between the
+-- tags that you want to enforce, and define that combinator using 'retag'.
+--
+-- @
+-- data Succ n
+-- retagSucc :: 'Tagged' n a -> 'Tagged' (Succ n) a
+-- retagSucc = 'retag'
+-- @
+retag :: Tagged s b -> Tagged t b
+retag = Tagged . unTagged
+{-# INLINE retag #-}
+
+-- | Alias for 'unTagged'
+untag :: Tagged s b -> b
+untag = unTagged
+
+-- | Tag a value with its own type.
+tagSelf :: a -> Tagged a a
+tagSelf = Tagged
+{-# INLINE tagSelf #-}
+
+-- | 'asTaggedTypeOf' is a type-restricted version of 'const'. It is usually used as an infix operator, and its typing forces its first argument (which is usually overloaded) to have the same type as the tag of the second.
+asTaggedTypeOf :: s -> tagged s b -> s
+asTaggedTypeOf = const
+{-# INLINE asTaggedTypeOf #-}
+
+witness :: Tagged a b -> a -> b
+witness (Tagged b) _ = b
+{-# INLINE witness #-}
+
+-- | 'untagSelf' is a type-restricted version of 'untag'.
+untagSelf :: Tagged a a -> a
+untagSelf (Tagged x) = x
+{-# INLINE untagSelf #-}
+
+-- | Convert from a 'Tagged' representation to a representation
+-- based on a 'Proxy'.
+proxy :: Tagged s a -> proxy s -> a
+proxy (Tagged x) _ = x
+{-# INLINE proxy #-}
+
+-- | Convert from a representation based on a 'Proxy' to a 'Tagged'
+-- representation.
+unproxy :: (Proxy s -> a) -> Tagged s a
+unproxy f = Tagged (f Proxy)
+{-# INLINE unproxy #-}
+
+-- | Another way to convert a proxy to a tag.
+tagWith :: proxy s -> a -> Tagged s a
+tagWith _ = Tagged
+{-# INLINE tagWith #-}
+
+-- | Some times you need to change the proxy you have lying around.
+-- Idiomatic usage is to make a new combinator for the relationship
+-- between the proxies that you want to enforce, and define that
+-- combinator using 'reproxy'.
+--
+-- @
+-- data Succ n
+-- reproxySucc :: proxy n -> 'Proxy' (Succ n)
+-- reproxySucc = 'reproxy'
+-- @
+reproxy :: proxy a -> Proxy b
+reproxy _ = Proxy
diff --git a/tagged.cabal b/tagged.cabal
--- a/tagged.cabal
+++ b/tagged.cabal
@@ -1,5 +1,5 @@
 name:           tagged
-version:        0.4.5
+version:        0.8.10
 license:        BSD3
 license-file:   LICENSE
 author:         Edward A. Kmett
@@ -9,25 +9,65 @@
 synopsis:       Haskell 98 phantom types to avoid unsafely passing dummy arguments
 homepage:       http://github.com/ekmett/tagged
 bug-reports:    http://github.com/ekmett/tagged/issues
-copyright:      2009-2011 Edward A. Kmett
-description:    Haskell 98 phantom types to avoid unsafely passing dummy arguments
+copyright:      2009-2015 Edward A. Kmett
+description:    Haskell 98 phantom types to avoid unsafely passing dummy arguments.
 build-type:     Simple
 cabal-version:  >= 1.10
-extra-source-files: .travis.yml CHANGELOG.markdown README.markdown
+extra-source-files: .hlint.yaml CHANGELOG.markdown README.markdown
+tested-with:
+  GHC == 8.0.2
+  GHC == 8.2.2
+  GHC == 8.4.4
+  GHC == 8.6.5
+  GHC == 8.8.4
+  GHC == 8.10.7
+  GHC == 9.0.2
+  GHC == 9.2.8
+  GHC == 9.4.8
+  GHC == 9.6.6
+  GHC == 9.8.4
+  GHC == 9.10.1
+  GHC == 9.12.1
 
 source-repository head
   type: git
-  location: git://github.com/ekmett/tagged.git
+  location: https://github.com/ekmett/tagged.git
 
+flag deepseq
+  description:
+    You can disable the use of the `deepseq` package using `-f-deepseq`.
+    .
+    Disabing this is an unsupported configuration, but it may be useful for accelerating builds in sandboxes for expert users.
+  default: True
+  manual: True
+
+flag template-haskell
+  description:
+    You can disable the use of the `template-haskell` package using `-f-template-haskell`.
+    .
+    Disabling this is an unsupported configuration, but it may be useful for accelerating builds in sandboxes for expert users.
+  default: True
+  manual: True
+
 library
   default-language: Haskell98
   other-extensions: CPP
-  if !impl(hugs)
-    cpp-options: -DLANGUAGE_DeriveDataTypeable
-    other-extensions: DeriveDataTypeable
   build-depends:
-    base >= 2 && < 5
+    base >= 4.9 && < 5
+  ghc-options: -Wall
+  hs-source-dirs: src
   exposed-modules:
     Data.Tagged
-    Data.Proxy
-  ghc-options: -Wall
+
+  if impl(ghc >= 9.0)
+    -- these flags may abort compilation with GHC-8.10
+    -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295
+    ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode
+
+  if flag(deepseq)
+    build-depends: deepseq >= 1.1 && < 1.6
+
+  if flag(template-haskell) && impl(ghc)
+    build-depends: template-haskell >= 2.11 && < 2.24
+    exposed-modules:
+      Data.Proxy.TH