diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,31 @@
+0.13 [2021.02.17]
+-----------------
+* `Data.Constraint.Symbol` now reexports the `GHC.TypeLits.AppendSymbol` type
+  family from recent versions of `base` (or, on old versions of `base`, it
+  defines a backwards-compatibile version of `AppendSymbol`). The existing
+  `(++)` type family for `Data.Constraint.Symbol` is now a synonym for
+  `AppendSymbol`.
+
+  This is technically a breaking change, as `(++)` was previously defined like
+  so:
+
+  ```hs
+  type family (++) :: Symbol -> Symbol -> Symbol
+  ```
+
+  This meant that `(++)` could be partially applied. However, for compatibility
+  with the way that `AppendSymbol` is defined, `(++)` is now defined like so:
+
+  ```hs
+  type m ++ n = AppendSymbol m n
+  ```
+
+  As a result, `(++)` can no longer be partially applied.
+* Make the `(++)` type family in `Data.Constraint.Symbol` be `infixr 5`.
+* Add `implied :: (a => b) -> (a :- b)` to `Data.Constraint`, which converts
+  a quantified constraint into an entailment. This is only available when
+  compiled with GHC 8.6 or later.
+
 0.12 [2020.02.03]
 -----------------
 * Relax the type signature for `divideTimes`:
diff --git a/README.markdown b/README.markdown
--- a/README.markdown
+++ b/README.markdown
@@ -1,7 +1,7 @@
 constraints
 ===========
 
-[![Hackage](https://img.shields.io/hackage/v/constraints.svg)](https://hackage.haskell.org/package/constraints) [![Build Status](https://secure.travis-ci.org/ekmett/constraints.png?branch=master)](http://travis-ci.org/ekmett/constraints)
+[![Hackage](https://img.shields.io/hackage/v/constraints.svg)](https://hackage.haskell.org/package/constraints) [![Build Status](https://github.com/ekmett/constraints/workflows/Haskell-CI/badge.svg)](https://github.com/ekmett/constraints/actions?query=workflow%3AHaskell-CI)
 
 This package provides data types and classes for manipulating the 'ConstraintKinds' exposed by GHC in 7.4.
 
diff --git a/constraints.cabal b/constraints.cabal
--- a/constraints.cabal
+++ b/constraints.cabal
@@ -1,6 +1,6 @@
 name:          constraints
 category:      Constraints
-version:       0.12
+version:       0.13
 license:       BSD2
 cabal-version: >= 1.10
 license-file:  LICENSE
@@ -23,7 +23,8 @@
              , GHC == 8.2.2
              , GHC == 8.4.4
              , GHC == 8.6.5
-             , GHC == 8.8.1
+             , GHC == 8.8.3
+             , GHC == 8.10.1
 extra-source-files: README.markdown
                   , CHANGELOG.markdown
 
@@ -54,10 +55,11 @@
     ghc-prim,
     hashable >= 1.2 && < 1.4,
     mtl >= 2.1.2 && < 2.3,
-    semigroups >= 0.17 && < 0.20,
     transformers >= 0.3.0.0 && < 0.6,
     transformers-compat >= 0.5 && < 1,
     type-equality >= 1 && < 2
+  if impl(ghc < 8.0)
+    build-depends: semigroups >= 0.17 && < 0.20
 
   exposed-modules:
     Data.Constraint
@@ -72,6 +74,8 @@
       Data.Constraint.Symbol
 
   ghc-options: -Wall
+  if impl(ghc >= 8.6)
+    ghc-options: -Wno-star-is-type
 
 test-suite spec
   type: exitcode-stdio-1.0
diff --git a/src/Data/Constraint.hs b/src/Data/Constraint.hs
--- a/src/Data/Constraint.hs
+++ b/src/Data/Constraint.hs
@@ -27,6 +27,9 @@
 #if __GLASGOW_HASKELL__ >= 708 && __GLASGOW_HASKELL__ < 710
 {-# LANGUAGE NullaryTypeClasses #-}
 #endif
+#if __GLASGOW_HASKELL__ >= 806
+{-# LANGUAGE QuantifiedConstraints #-}
+#endif
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Constraint
@@ -71,6 +74,9 @@
   , strengthen1, strengthen2
   , (&&&), (***)
   , trans, refl
+#if __GLASGOW_HASKELL__ >= 806
+  , implied
+#endif
   , Bottom(no)
   , top, bottom
   -- * Dict is fully faithful
@@ -124,7 +130,7 @@
 -- captures a dictionary that proves we have an:
 --
 -- @
--- instance 'Eq' 'Int
+-- instance 'Eq' 'Int'
 -- @
 --
 -- Pattern matching on the 'Dict' constructor will bring this instance into scope.
@@ -323,6 +329,18 @@
 -- If we view @(':-')@ as a Constraint-indexed category, then this is 'id'
 refl :: a :- a
 refl = Sub Dict
+
+--------------------------------------------------------------------------------
+-- QuantifiedConstraints
+--------------------------------------------------------------------------------
+
+#if __GLASGOW_HASKELL__ >= 806
+-- | Convert a quantified constraint into an entailment.
+--
+-- Only available on GHC 8.6 or later.
+implied :: forall a b. (a => b) => a :- b
+implied = Sub (Dict :: Dict b)
+#endif
 
 --------------------------------------------------------------------------------
 -- (,) is a Bifunctor
diff --git a/src/Data/Constraint/Symbol.hs b/src/Data/Constraint/Symbol.hs
--- a/src/Data/Constraint/Symbol.hs
+++ b/src/Data/Constraint/Symbol.hs
@@ -7,11 +7,13 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE CPP #-}
 -- | Utilities for working with 'KnownSymbol' constraints.
 --
 -- This module is only available on GHC 8.0 or later.
 module Data.Constraint.Symbol
-  ( type (++)
+  ( type AppendSymbol
+  , type (++)
   , type Take
   , type Drop
   , type Length
@@ -41,7 +43,14 @@
 import GHC.TypeLits
 import Unsafe.Coerce
 
-type family (++) :: Symbol -> Symbol -> Symbol where
+#if !(MIN_VERSION_base(4,10,0))
+type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol
+#endif
+
+-- | An infix synonym for 'AppendSymbol'.
+type (m :: Symbol) ++ (n :: Symbol) = AppendSymbol m n
+infixr 5 ++
+
 type family Take :: Nat -> Symbol -> Symbol where
 type family Drop :: Nat -> Symbol -> Symbol where
 type family Length :: Symbol -> Nat where
@@ -64,16 +73,26 @@
 
 -- axioms and operations
 
-appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (a ++ b)
+appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)
 appendSymbol = magicSSS (++)
 
-appendUnit1 :: forall a. Dict (("" ++ a) ~ a)
-appendUnit1 = axiom
+appendUnit1 :: forall a. Dict (AppendSymbol "" a ~ a)
+appendUnit1 =
+#if MIN_VERSION_base(4,10,0)
+  Dict
+#else
+  axiom
+#endif
 
-appendUnit2 :: forall a. Dict ((a ++ "") ~ a)
-appendUnit2 = axiom
+appendUnit2 :: forall a. Dict (AppendSymbol a "" ~ a)
+appendUnit2 =
+#if MIN_VERSION_base(4,10,0)
+  Dict
+#else
+  axiom
+#endif
 
-appendAssociates :: forall a b c. Dict (((a ++ b) ++ c) ~ (a ++ (b ++ c)))
+appendAssociates :: forall a b c. Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c))
 appendAssociates = axiom
 
 takeSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)
@@ -82,7 +101,7 @@
 dropSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)
 dropSymbol = magicNSS drop
 
-takeAppendDrop :: forall n a. Dict (Take n a ++ Drop n a ~ a)
+takeAppendDrop :: forall n a. Dict (AppendSymbol (Take n a) (Drop n a) ~ a)
 takeAppendDrop = axiom
 
 lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a)