attenuation 0.1.0.0 → 0.2.0

raw patch · 5 files changed

+417/−151 lines, 5 filesdep +constraintsdep −profunctorsdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: constraints

Dependencies removed: profunctors

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−0
• attenuation.cabal +7/−8
• src/Data/Type/Attenuation.hs +62/−143
• src/Data/Type/Attenuation/Internal.hs +290/−0
• src/Data/Type/Attenuation/Unsafe.hs +48/−0

@@ -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`.

@@ -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

@@ -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

@@ -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

@@ -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)