diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,3 +2,13 @@
 
 Added everything that exists in this version.  See Haddock documentation for a
 complete accounting.
+
+# 0.2.0
+
+* Rename `attenuate` to `attenuateWith` (breaking change).
+* Split `profunctors` features to a separate package (breaking change).
+* Add an `Attenuable` class that does a decent job of deriving `Attenuation`s.
+* Add a new `attenuate` that uses `Attenuable`.
+* Add a `Data.Attenuation.Unsafe` module giving access to the internals.
+* Add `HasDict` for `Attenuation` (with new enough `constraints`).
+* Add `:-` entailments corresponding to pseudo-instances of `Attenuable`.
diff --git a/attenuation.cabal b/attenuation.cabal
--- a/attenuation.cabal
+++ b/attenuation.cabal
@@ -1,13 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.33.0.
+-- This file has been generated from package.yaml by hpack version 0.34.4.
 --
 -- see: https://github.com/sol/hpack
---
--- hash: 92d47a2950ec019ac542be7970e219dab7309ba103c1c46acae9beb21fef6f06
 
 name:           attenuation
-version:        0.1.0.0
+version:        0.2.0
 synopsis:       Representational subtyping relations and variance roles.
 description:    This lets you coerce containers (among other things) from stronger types to
                 weaker types with zero runtime cost when it's safe to do so, e.g.
@@ -28,15 +26,16 @@
 source-repository head
   type: git
   location: https://github.com/google/hs-attenuation
+  subdir: attenuation
 
 library
   exposed-modules:
       Data.Type.Attenuation
-  other-modules:
-      Paths_attenuation
+      Data.Type.Attenuation.Unsafe
+      Data.Type.Attenuation.Internal
   hs-source-dirs:
       src
   build-depends:
-      base >=4.7 && <4.16
-    , profunctors >=0.1 && <5.7
+      base >=4.12 && <4.16
+    , constraints >=0.10 && <0.14
   default-language: Haskell2010
diff --git a/src/Data/Type/Attenuation.hs b/src/Data/Type/Attenuation.hs
--- a/src/Data/Type/Attenuation.hs
+++ b/src/Data/Type/Attenuation.hs
@@ -12,162 +12,85 @@
 -- See the License for the specific language governing permissions and
 -- limitations under the License.
 
--- | Representational subtyping relations and variance roles.
-
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
+-- | Representational subtyping relations and variance roles.
+
 module Data.Type.Attenuation
          ( -- * Attenuation
-           Attenuation, attenuate, coercible
-         , trans, repr, coer
+           Attenuation, type (:⊆:), attenuateWith, coercible
+         , trans, repr, coer, iso, inst
            -- ** Representationality
          , Representational, Representational0, Representational1, Variance
            -- ** Functor and Contravariant
          , co, contra
            -- ** Bifunctor
          , fstco, sndco
-           -- ** Profunctor
-         , lcontra, rco
+           -- ** (->)
+         , domain, codomain
            -- ** Initial and Final Objects
          , attVoid, attAny
+           -- * Attenuable
+         , Attenuable(..), type (⊆), attenuate
+         , withAttenuation
+           -- ** Entailments
+         , contravariance, transitivity
          ) where
 
+import Prelude hiding ((.))
+
 import Control.Category (Category(..))
-import Data.Bifunctor (Bifunctor)
 import Data.Coerce (Coercible, coerce)
-import Data.Functor.Contravariant (Contravariant)
-import Data.Kind (Constraint)
-import Data.Profunctor (Profunctor)
+import Data.Functor.Contravariant (Contravariant(..))
 import Data.Type.Coercion (Coercion(..), sym)
-import qualified Data.Type.Coercion as Coercion
-import Data.Type.Equality ((:~:)(..))
+import Data.Type.Equality ((:~:)(..), gcastWith)
 import Data.Void (Void)
 import GHC.Exts (Any)
 
+import Data.Constraint ((:-)(Sub), Dict(..))
+
 #if MIN_VERSION_base(4,15,0)
 import Unsafe.Coerce (unsafeEqualityProof, UnsafeEquality(..))
 #else
 import Unsafe.Coerce (unsafeCoerce)
 #endif
 
--- | @Attenuation a b@ is a unidirectional 'Coercion' from @a@ to @b@.
---
--- "Attenuate: reduce the force, effect, or value of."  An @Attenuation@ takes
--- a stronger, stricter type to a weaker, more lax type.  It's meant to sound a
--- bit like 'Coercion', while conveying that it weakens the type of its
--- argument.
---
--- This arises from newtypes that impose additional invariants on their
--- representations: if we define @Fin :: Nat -> Type@ as a newtype over 'Int',
--- such as in <https://hackage.haskell.org/package/fin-int fin-int>, then it's
--- safe to 'coerce' @Fin@s to 'Int's, and @Fin@s to other @Fin@s with larger
--- @Nat@ parameters, but not vice versa.
---
--- Within the module defining this @Fin@ type, we can obtain 'Coercible'
--- between any two @Fin@ types regardless of their roles, because their newtype
--- constructors are in scope, but if we've taken appropriate precautions
--- (namely not exporting the constructor), we can't obtain it outside the
--- module.  We can relax this and make the coercion "opt-in" by exporting it in
--- the form of a 'Coercion' with a scary name like @unsafeCoFin@, but this is
--- still error-prone.
---
--- Instead, we introduce a newtype wrapper around 'Coercion' which restricts it
--- to be used only in the forward direction, and carefully design its API so
--- that it can only be obtained under the appropriate circumstances.
---
--- @Attenuation a b@ can be seen as a witness that @a@ is, semantically and
--- representationally, a subtype of @b@: that is, any runtime object that
--- inhabits @a@ also inhabits @b@ without any conversion.  Note, however, that
--- we can't have a useful typeclass of this subtyping relation because all of
--- its instances would have to be specified individually: whereas 'Coercible'
--- is willing to invert or compose coercions implicitly because of GHC magic, a
--- subtyping class would not have that affordance.
-newtype Attenuation a b = Attenuation (Coercion a b)
-  deriving (Eq, Ord, Show)
+import Data.Type.Attenuation.Internal
 
-instance Category Attenuation where
-  id = coercible
-  (.) = flip trans
+-- | An operator form of 'Attenuation', by analogy to (':~:').
+type (:⊆:) = Attenuation
 
 -- | Coerce along an 'Attenuation'.
 --
 -- This is really, truly a coercion when it reaches Core.
-attenuate :: Attenuation a b -> a -> b
-attenuate (Attenuation Coercion) = coerce
+attenuateWith :: Attenuation a b -> a -> b
+attenuateWith (Attenuation Coercion) = coerce
 
 -- | Any coercible types have an 'Attenuation'.
 coercible :: Coercible a b => Attenuation a b
 coercible = Attenuation Coercion
 
--- | Transitivity of 'Attenuation's.  See also the 'Category' instance.
-trans :: Attenuation a b -> Attenuation b c -> Attenuation a c
-trans (Attenuation coAB) (Attenuation coBC) =
-  Attenuation (Coercion.trans coAB coBC)
-
 -- | Any type is unidirectionally coercible to itself.
 repr :: (a :~: b) -> Attenuation a b
-repr Refl = Attenuation Coercion
+repr eq = gcastWith eq refl
 
 -- | Bidirectional coercions can be weakened to unidirectional coercions.
 coer :: Coercion a b -> Attenuation a b
 coer = Attenuation
 
--- | A witness that @a@ occurs representationally in @s@ and that, when
--- substituting it for @b@, you get @t@.
---
--- These compose like Lenses from the "lens" package, so you can e.g. lift
--- 'Attenuation's through several @Functor@s by @'co'.co.co $ x@.
-type Variance s t a b = Attenuation a b -> Attenuation s t
-
--- | A constraint that behaves like @type role f representational@.
---
--- This means that if we have this constraint in context and GHC can solve
--- 'Coercible' for some types @a@ and @b@, it will also lift the coercion to @f
--- a@ and @f b@.
-type Representational f =
-  (forall a b. Coercible a b => Coercible (f a) (f b) :: Constraint)
-
--- | Lift a 'Coercion' over a type constructor.
-rep :: Representational f => Coercion a b -> Coercion (f a) (f b)
-rep Coercion = Coercion
-
--- | A constraint that behaves like @type role f _ representational@.
---
--- See also 'Representational'.
-type Representational1 f =
-  (forall a b x. Coercible a b => Coercible (f x a) (f x b) :: Constraint)
-
--- | A constraint that behaves like @type role f representational _@.
---
--- See also 'Representational'.
-type Representational0 f =
-  (forall a b x. Coercible a b => Coercible (f a x) (f b x) :: Constraint)
-
--- | Lift a 'Coercion' over the last-but-one parameter of a type constructor.
-rep0 :: Representational0 f => Coercion a b -> Coercion (f a x) (f b x)
-rep0 Coercion = Coercion
-
--- | Lift an 'Attenuation' covariantly over a type constructor @f@.
---
--- Although we don't /use/ the 'Functor' constraint, it serves an important
--- purpose: to guarantee that the type parameter @a@ doesn't appear
--- contravariantly in @f a@; otherwise it'd be impossible to write a 'Functor'
--- instance.  This is used as a standin for more-detailed "covariant" and
--- "contravariant" type roles, which GHC doesn't have because there's no
--- built-in notion of subtyping to use them with.  'Representational1' provides
--- the actual lifting of coercions, and 'Functor' guarantees we've got the
--- variance right.
-co :: (Functor f, Representational f) => Variance (f a) (f b) a b
-co (Attenuation c) = Attenuation (rep c)
-
 -- | Lift an 'Attenuation' contravariantly over a type constructor @f@.
 --
 -- Regarding the 'Contravariant' constraint, see 'co', and interchange mentions
@@ -175,46 +98,14 @@
 contra :: (Contravariant f, Representational f) => Variance (f b) (f a) a b
 contra (Attenuation c) = Attenuation (sym $ rep c)
 
--- | Lift an 'Attenuation' covariantly over the left of a 'Bifunctor'.
---
--- Like with 'co' and 'contra', we require a not-actually-used constraint as
--- proof that the type has the appropriate variance.  Since there's not a
--- commonly-used class for functors over the last-but-one parameter, we use
--- 'Bifunctor'.  Sadly, this rules out types which are covariant in parameter
--- -1 and contravariant in parameter -0.
-fstco :: (Bifunctor f, Representational0 f) => Variance (f a x) (f b x) a b
-fstco (Attenuation c) = Attenuation (rep0 c)
-
--- | Lift an 'Attenuation' covariantly over the last-but-one type parameter.
---
--- Like with 'co' and 'contra', we require a not-actually-used constraint as
--- proof that the type has the appropriate variance.  Since there's not a
--- commonly-used class for functors over the last-but-one parameter, we use
--- 'Bifunctor'.  Sadly, this rules out types which are covariant in parameter
--- -1 and contravariant in parameter -0.
---
--- Note that any particular type with a @Bifunctor f@ instance should also have
--- @Functor (f x)@, so 'co' should work on any type that 'sndco' works on, but
--- in polymorphic contexts, the 'Functor' instance may not be available.
-sndco :: (Bifunctor f, Representational1 f) => Variance (f x a) (f x b) a b
-sndco (Attenuation c) = Attenuation (rep c)
-
--- | Lift an 'Attenuation' covariantly over the left of a 'Profunctor'.
---
--- Similarly to the use of 'Functor' in 'co', we use 'Profunctor' to guarantee
--- contravariance in the appropriate parameter.
-lcontra :: (Profunctor p, Representational0 p) => Variance (p b x) (p a x) a b
-lcontra (Attenuation c) = Attenuation (sym $ rep0 c)
-
--- | Lift an 'Attenuation' covariantly over the right of a 'Profunctor'.
+-- | 'Attenuation's across type constructors can be instantiated.
 --
--- Similarly to the use of 'Functor' in 'co', we use 'Profunctor' to guarantee
--- contravariance in the appropriate parameter.
+-- This means 'Attenuation's across type constructors lift equality of type
+-- parameters to 'Attenuation' of the applied result.
 --
--- As with 'sndco', this functions the same as 'co', but the needed 'Functor'
--- instance might not be available in polymorphic contexts.
-rco :: (Profunctor p, Representational1 p) => Variance (p x a) (p x b) a b
-rco (Attenuation c) = Attenuation (rep c)
+-- This is analogous to how @Coercible f g@ works.
+inst :: Attenuation f g -> Attenuation (f x) (g x)
+inst (Attenuation Coercion) = Attenuation Coercion
 
 -- | 'Attenuation' of 'Void' to any type.
 --
@@ -248,3 +139,31 @@
 #else
   (unsafeCoerce (Coercion :: Coercion a a) :: Coercion a Any)
 #endif
+
+-- | An operator form of 'Attenuable'.
+type (⊆) = Attenuable
+
+-- | Coerce from a representational subtype @a@ to its supertype @b@.
+attenuate :: Attenuable a b => a -> b
+attenuate = attenuateWith attenuation
+
+-- Type inference aid for use in entailments: otherwise it's ambiguous what
+-- 'Attenuation' we want to promote with 'withAttenuation'.
+toDict :: Attenuation a b -> Dict (Attenuable a b)
+toDict att = withAttenuation att Dict
+
+-- | 'Contravariant' functors map attenuation contravariantly.
+contravariance
+  :: forall f a b
+   . (Representational f, Contravariant f)
+  => Attenuable a b :- Attenuable (f b) (f a)
+contravariance = Sub (toDict (contra attenuation))
+
+-- | 'Attenuation's are transitive.
+transitivity
+  :: forall b a c. (Attenuable b c, Attenuable a b) :- Attenuable a c
+transitivity = Sub (toDict $ attenuation @b @c . attenuation @a @b)
+
+-- | If 'Attenuation's in both directions exist, they're actually a 'Coercion'.
+iso :: Attenuation a b -> Attenuation b a -> Coercion a b
+iso (Attenuation c) _ = c
diff --git a/src/Data/Type/Attenuation/Internal.hs b/src/Data/Type/Attenuation/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Attenuation/Internal.hs
@@ -0,0 +1,290 @@
+-- Copyright 2020-2021 Google LLC
+--
+-- Licensed under the Apache License, Version 2.0 (the "License");
+-- you may not use this file except in compliance with the License.
+-- You may obtain a copy of the License at
+--
+--      http://www.apache.org/licenses/LICENSE-2.0
+--
+-- Unless required by applicable law or agreed to in writing, software
+-- distributed under the License is distributed on an "AS IS" BASIS,
+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+-- See the License for the specific language governing permissions and
+-- limitations under the License.
+
+{-# OPTIONS_HADDOCK not-home #-}
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Internal implementation details of @attenuation@.
+--
+-- Prefer "Data.Type.Attenuation" and "Data.Type.Attenuation.Unsafe" instead
+-- whenever possible.  This exports the constructor of 'Attenuation', which is
+-- much easier to misuse by accident than
+-- 'Data.Type.Attenuation.Unsafe.unsafeToCoercion'.
+
+module Data.Type.Attenuation.Internal
+         ( Attenuation(..), Attenuable(..)
+         , Variance, Representational, Representational0, Representational1
+         , refl, trans, co, fstco, sndco, domain, codomain, rep, rep0
+         , withAttenuation
+         ) where
+
+import Prelude hiding ((.))
+
+import Control.Category (Category(..))
+import Data.Bifunctor (Bifunctor)
+import Data.Coerce (Coercible)
+import Data.Kind (Constraint, Type)
+import Data.Type.Coercion (Coercion(..), sym)
+import qualified Data.Type.Coercion as Coercion
+
+#if MIN_VERSION_constraints(0, 11, 0)
+import Data.Constraint (Dict(..), HasDict(..))
+#endif
+
+-- | A constraint that behaves like @type role f representational@.
+--
+-- This means that if we have this constraint in context and GHC can solve
+-- 'Coercible' for some types @a@ and @b@, it will also lift the coercion to @f
+-- a@ and @f b@.
+type Representational f =
+  (forall a b. Coercible a b => Coercible (f a) (f b) :: Constraint)
+
+-- | A constraint that behaves like @type role f _ representational@.
+--
+-- See also 'Representational'.
+type Representational1 f =
+  (forall a b x. Coercible a b => Coercible (f x a) (f x b) :: Constraint)
+
+-- | A constraint that behaves like @type role f representational _@.
+--
+-- See also 'Representational'.
+type Representational0 f =
+  (forall a b x. Coercible a b => Coercible (f a x) (f b x) :: Constraint)
+
+-- | A witness that @a@ occurs representationally in @s@ and that, when
+-- substituting it for @b@, you get @t@.
+--
+-- These compose like Lenses from the "lens" package, so you can e.g. lift
+-- 'Attenuation's through several @Functor@s by @'co'.co.co $ x@.
+type Variance s t a b = Attenuation a b -> Attenuation s t
+
+-- | Lift a 'Coercion' over a type constructor.
+rep :: Representational f => Coercion a b -> Coercion (f a) (f b)
+rep Coercion = Coercion
+
+-- | Lift a 'Coercion' over the last-but-one parameter of a type constructor.
+rep0 :: Representational0 f => Coercion a b -> Coercion (f a x) (f b x)
+rep0 Coercion = Coercion
+
+-- | @Attenuation a b@ is a unidirectional 'Coercion' from @a@ to @b@.
+--
+-- "Attenuate: reduce the force, effect, or value of."  An @Attenuation@ takes
+-- a stronger, stricter type to a weaker, more lax type.  It's meant to sound a
+-- bit like 'Coercion', while conveying that it weakens the type of its
+-- argument.
+--
+-- This arises from newtypes that impose additional invariants on their
+-- representations: if we define @Fin :: Nat -> Type@ as a newtype over 'Int',
+-- such as in <https://hackage.haskell.org/package/fin-int fin-int>, then it's
+-- safe to 'Data.Coerce.coerce' @Fin@s to 'Int's, and @Fin@s to other @Fin@s
+-- with larger @Nat@ parameters, but not vice versa.
+--
+-- Within the module defining this @Fin@ type, we can obtain 'Coercible'
+-- between any two @Fin@ types regardless of their roles, because their newtype
+-- constructors are in scope, but if we've taken appropriate precautions
+-- (namely not exporting the constructor), we can't obtain it outside the
+-- module.  We can relax this and make the coercion "opt-in" by exporting it in
+-- the form of a 'Coercion' with a scary name like @unsafeCoFin@, but this is
+-- still error-prone.
+--
+-- Instead, we introduce a newtype wrapper around 'Coercion' which restricts it
+-- to be used only in the forward direction, and carefully design its API so
+-- that it can only be obtained under the appropriate circumstances.
+--
+-- @Attenuation a b@ can be seen as a witness that @a@ is, semantically and
+-- representationally, a subtype of @b@: that is, any runtime object that
+-- inhabits @a@ also inhabits @b@ without any conversion.
+newtype Attenuation a b = Attenuation (Coercion a b)
+  deriving (Eq, Ord, Show)
+
+-- | Lift an 'Attenuation' covariantly over a type constructor @f@.
+--
+-- Although we don't /use/ the 'Functor' constraint, it serves an important
+-- purpose: to guarantee that the type parameter @a@ doesn't appear
+-- contravariantly in @f a@; otherwise it'd be impossible to write a 'Functor'
+-- instance.  This is used as a standin for more-detailed "covariant" and
+-- "contravariant" type roles, which GHC doesn't have because there's no
+-- built-in notion of subtyping to use them with.  'Representational1' provides
+-- the actual lifting of coercions, and 'Functor' guarantees we've got the
+-- variance right.
+co :: (Functor f, Representational f) => Variance (f a) (f b) a b
+co (Attenuation c) = Attenuation (rep c)
+
+-- | Lift an 'Attenuation' covariantly over the left of a 'Bifunctor'.
+--
+-- Like with 'co' and 'Data.Type.Attenuation.contra', we require a
+-- not-actually-used constraint as proof that the type has the appropriate
+-- variance.  Since there's not a commonly-used class for functors over the
+-- last-but-one parameter, we use 'Bifunctor'.  Sadly, this rules out types
+-- which are covariant in parameter -1 and contravariant in parameter -0.
+fstco :: (Bifunctor f, Representational0 f) => Variance (f a x) (f b x) a b
+fstco (Attenuation c) = Attenuation (rep0 c)
+
+-- | Lift an 'Attenuation' covariantly over the last-but-one type parameter.
+--
+-- Like with 'co' and 'Data.Type.Attenuation.contra', we require a
+-- not-actually-used constraint as proof that the type has the appropriate
+-- variance.  Since there's not a commonly-used class for functors over the
+-- last-but-one parameter, we use 'Bifunctor'.  Sadly, this rules out types
+-- which are covariant in parameter -1 and contravariant in parameter -0.
+--
+-- Note that any particular type with a @Bifunctor f@ instance should also have
+-- @Functor (f x)@, so 'co' should work on any type that 'sndco' works on, but
+-- in polymorphic contexts, the 'Functor' instance may not be available.
+sndco :: (Bifunctor f, Representational1 f) => Variance (f x a) (f x b) a b
+sndco (Attenuation c) = Attenuation (rep c)
+
+-- | Lift an 'Attenuation' contravariantly over the argument of a functiwon.
+domain :: Variance (b -> x) (a -> x) a b
+domain (Attenuation c) = Attenuation (sym $ rep0 c)
+
+-- | Lift an 'Attenuation' covariantly over the result of a function.
+--
+-- This is just a specialization of 'co'.
+codomain :: Variance (x -> a) (x -> b) a b
+codomain (Attenuation c) = Attenuation (rep c)
+
+-- | Lift an 'Attenuation' to a constraint within a subexpression.
+--
+-- This is just specialization of 'Data.Constraint.withDict'; consider using
+-- that or ('Data.Constraint.\\').
+withAttenuation :: Attenuation a b -> (Attenuable a b => r) -> r
+-- Some fairly neat trickery here: because we have the (incoherent) instance
+-- that demotes Coercible to Attenuable, and because Attenuation internally
+-- just holds a Coercion, which in turn is just a GADT constructor holding a
+-- Coercible instance, we can actually just unwrap everything (unsafely) to
+-- reify an Attenuation back to an Attenuable instance without making any
+-- assumptions about the representation of the Attenuable dictionary.
+withAttenuation (Attenuation Coercion) r = r
+
+-- If all else fails, we can promote a Coercible instance.  Since this is
+-- less-specific than any sensible instance and is overlappable, it'll never be
+-- selected if we have any other option, so we won't incur Coercible
+-- constraints needlessly.
+instance {-# INCOHERENT #-} Coercible a b => Attenuable a b
+
+-- A more-specific, less-demanding version of the previous instance.  This
+-- exists to suppress the 'Functor' and 'Bifunctor' instances when the
+-- parameter is equal on both sides, since letting those instances win would
+-- introduce 'Representational' constraints that we don't actually need.
+instance {-# INCOHERENT #-} Attenuable (a :: Type) a
+
+#if MIN_VERSION_constraints(0, 11, 0)
+instance HasDict (Attenuable a b) (Attenuation a b) where
+  evidence = (`withAttenuation` Dict)
+#endif
+
+-- Any covariant functor with representational role for its parameter is
+-- representationally covariant.
+--
+-- Since this instance is incoherent (and thus overlappable), it'll be
+-- suppressed by any more-specific instance, so you can write instances by hand
+-- for 'Contravariant' functors.
+--
+-- The main downside is that, by default, GHC will assume that unary type
+-- constructors should solve 'Attenuable' by looking for a 'Functor' instance,
+-- which could lead to confusing type errors for any 'Contravariant's that
+-- don't have specific instances.  Since the alternative is that any covariant
+-- types that aren't aware of the @attenuation@ package (which, let's be
+-- honest, is gonna be pretty much all of them) will have no instance
+-- available, this seems worth the tradeoff.
+instance {-# INCOHERENT #-} (Functor f, Representational f, Attenuable x y)
+      => Attenuable (f x) (f y) where
+  attenuation = co attenuation
+
+-- Similarly to the 'Functor' instance, this assumes by default that binary
+-- type constructors should be 'Bifunctor's.
+--
+-- As before, this doesn't prevent specific instances for e.g. @Profunctor@s,
+-- but rather just defines what GHC will look for if there's not a
+-- more-specific instance.
+--
+-- This is more specific than the 'Functor' instance, so unfortunately we'll
+-- end up picking 'Bifunctor' in preference to 'Functor'.  In that case, either
+-- just write a manual instance for the particular type constructor, or build
+-- the 'Attenuation' manually with 'co'.
+instance {-# INCOHERENT #-}
+         ( Bifunctor f, Representational0 f, Representational1 f
+         , Attenuable a c
+         , Attenuable b d
+         )
+      => Attenuable (f a b) (f c d) where
+  attenuation = fstco attenuation . sndco attenuation
+
+instance (Attenuable c a, Attenuable b d)
+      => Attenuable (a -> b) (c -> d) where
+  attenuation = domain attenuation . codomain attenuation
+
+instance (Attenuable a a', Attenuable b b')
+      => Attenuable (a, b) (a', b') where
+  attenuation = fstco attenuation . sndco attenuation
+
+instance (Attenuable a a', Attenuable b b', Attenuable c c')
+      => Attenuable (a, b, c) (a', b', c') where
+  attenuation = fst3 . fstco attenuation . sndco attenuation
+   where
+    fst3 :: Attenuation (a, b', c') (a', b', c')
+    fst3 = case attenuation @a @a' of Attenuation Coercion -> attenuation
+
+-- | Transitivity of 'Attenuation's.  See also the 'Category' instance.
+trans :: Attenuation a b -> Attenuation b c -> Attenuation a c
+trans (Attenuation coAB) (Attenuation coBC) =
+  Attenuation (Coercion.trans coAB coBC)
+
+-- | Any type is unidirectionally-coercible to itself.
+refl :: Attenuation a a
+refl = Attenuation Coercion
+
+instance Category Attenuation where
+  id = refl
+  (.) = flip trans
+
+-- | @Attenuable a b@ is satisfiable iff there exists an @'Attenuation' a b@.
+--
+-- Since an 'Attenuation' is unique for a given pair of types (as it's
+-- internally just a wrapper around a 'Coercible' instance), any way of
+-- obtaining an 'Attenuation' gives exactly the same result.  This means all
+-- 'Attenuable' instances that /could/ exist for a pair of types are also
+-- identical.  In turn, this means that even "incoherent" instances for
+-- 'Attenuable' are actually coherent after all: any arbitrary choice of an
+-- instance gives the same result.  As such, it's perfectly fine for instances
+-- of 'Attenuable' to be marked @INCOHERENT@, as long as it results in good
+-- instance resolution behavior.  This is used to provide some convenient
+-- "fallback" instances filling in the (numerous) gaps in the set of specific
+-- instances: specifically, automatic demotion of 'Coercible' to 'Attenuable';
+-- and automatic lifting of 'Attenuable' across 'Functor's and 'Bifunctor's.
+--
+-- The word "satisfiable" in the first paragraph is chosen carefully: not all
+-- instances that are satisfiable will be solved automatically by GHC.  One can
+-- obtain 'Attenuable' instances by 'Data.Constraint.\\' or by an entailment
+-- ('Data.Constraint.:-'), for some types that wouldn't be solved by any of the
+-- "real" instances.  In particular, this is useful for compositions of
+-- attenuations and for lifting attenuations across
+-- 'Data.Functor.Contravariant.Contravariant's and @Profunctor@s.
+class Attenuable a b where
+  attenuation :: Attenuation a b
+  default attenuation :: Coercible a b => Attenuation a b
+  attenuation = Attenuation Coercion
diff --git a/src/Data/Type/Attenuation/Unsafe.hs b/src/Data/Type/Attenuation/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Attenuation/Unsafe.hs
@@ -0,0 +1,48 @@
+-- Copyright 2021 Google LLC
+--
+-- Licensed under the Apache License, Version 2.0 (the "License");
+-- you may not use this file except in compliance with the License.
+-- You may obtain a copy of the License at
+--
+--      http://www.apache.org/licenses/LICENSE-2.0
+--
+-- Unless required by applicable law or agreed to in writing, software
+-- distributed under the License is distributed on an "AS IS" BASIS,
+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+-- See the License for the specific language governing permissions and
+-- limitations under the License.
+
+-- | Unsafe misuses of 'Attenuation's\' underlying 'Coercion's.
+--
+-- This can allow violating the invariants of the source type, since it allows
+-- casting in the opposite direction from the intended 'Attenuation'.  If the
+-- 'Coercion' is lifted to a 'Data.Coerce.Coercible' instance, this is
+-- especially bad, since it can get used invisibly to allow lifted or composed
+-- coercions that shouldn't be allowed.  The contract defined here is that
+-- types may rely absolutely on 'Attenuation's not being used backwards in a
+-- way that violates their internal invariants, including for type-safety and
+-- memory-safety purposes.  As such, it is /unsafe/ to extract the 'Coercion'
+-- from an 'Attenuation', and any nonsense that results from doing so
+-- constitutes a bug in the client code that called 'unsafeToCoercion'.
+--
+-- This means extreme caution must be used with the contents of this module.
+-- It's always safe to use this to cast values back to their original type or
+-- to any type the original type is attenuable to.  Otherwise, the safety of a
+-- particular backwards cast depends entirely on the specific types involved.
+--
+-- Take care not to hold onto / leak inverted 'Attenuation's or
+-- illegitimately-obtained 'Coercion's by accident!
+
+module Data.Type.Attenuation.Unsafe (unsafeToCoercion, unsafeSym) where
+
+import Data.Type.Coercion (Coercion, sym)
+
+import Data.Type.Attenuation.Internal (Attenuation(..))
+
+-- | Unsafely access the internal 'Coercion' of an 'Attenuation'.
+unsafeToCoercion :: Attenuation a b -> Coercion a b
+unsafeToCoercion (Attenuation c) = c
+
+-- | Unsafely invert an 'Attenuation'.
+unsafeSym :: Attenuation a b -> Attenuation b a
+unsafeSym (Attenuation c) = Attenuation (sym c)