-- 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 a b -> Coercion (f a) (f b)
rep Coercion a b
Coercion = Coercion (f a) (f b)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
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 a b -> Coercion (f a x) (f b x)
rep0 Coercion a b
Coercion = Coercion (f a x) (f b x)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
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 (Attenuation a b -> Attenuation a b -> Bool
(Attenuation a b -> Attenuation a b -> Bool)
-> (Attenuation a b -> Attenuation a b -> Bool)
-> Eq (Attenuation a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
/= :: Attenuation a b -> Attenuation a b -> Bool
$c/= :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
== :: Attenuation a b -> Attenuation a b -> Bool
$c== :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
Eq, Eq (Attenuation a b)
Eq (Attenuation a b)
-> (Attenuation a b -> Attenuation a b -> Ordering)
-> (Attenuation a b -> Attenuation a b -> Bool)
-> (Attenuation a b -> Attenuation a b -> Bool)
-> (Attenuation a b -> Attenuation a b -> Bool)
-> (Attenuation a b -> Attenuation a b -> Bool)
-> (Attenuation a b -> Attenuation a b -> Attenuation a b)
-> (Attenuation a b -> Attenuation a b -> Attenuation a b)
-> Ord (Attenuation a b)
Attenuation a b -> Attenuation a b -> Bool
Attenuation a b -> Attenuation a b -> Ordering
Attenuation a b -> Attenuation a b -> Attenuation a b
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (a :: k) (b :: k). Eq (Attenuation a b)
forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Ordering
forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Attenuation a b
min :: Attenuation a b -> Attenuation a b -> Attenuation a b
$cmin :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Attenuation a b
max :: Attenuation a b -> Attenuation a b -> Attenuation a b
$cmax :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Attenuation a b
>= :: Attenuation a b -> Attenuation a b -> Bool
$c>= :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
> :: Attenuation a b -> Attenuation a b -> Bool
$c> :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
<= :: Attenuation a b -> Attenuation a b -> Bool
$c<= :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
< :: Attenuation a b -> Attenuation a b -> Bool
$c< :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
compare :: Attenuation a b -> Attenuation a b -> Ordering
$ccompare :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Ordering
$cp1Ord :: forall k (a :: k) (b :: k). Eq (Attenuation a b)
Ord, Int -> Attenuation a b -> ShowS
[Attenuation a b] -> ShowS
Attenuation a b -> String
(Int -> Attenuation a b -> ShowS)
-> (Attenuation a b -> String)
-> ([Attenuation a b] -> ShowS)
-> Show (Attenuation a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k) (b :: k). Int -> Attenuation a b -> ShowS
forall k (a :: k) (b :: k). [Attenuation a b] -> ShowS
forall k (a :: k) (b :: k). Attenuation a b -> String
showList :: [Attenuation a b] -> ShowS
$cshowList :: forall k (a :: k) (b :: k). [Attenuation a b] -> ShowS
show :: Attenuation a b -> String
$cshow :: forall k (a :: k) (b :: k). Attenuation a b -> String
showsPrec :: Int -> Attenuation a b -> ShowS
$cshowsPrec :: forall k (a :: k) (b :: k). Int -> Attenuation a b -> ShowS
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 :: Variance (f a) (f b) a b
co (Attenuation Coercion a b
c) = Coercion (f a) (f b) -> Attenuation (f a) (f b)
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (f a) (f b)
forall k k (f :: k -> k) (a :: k) (b :: k).
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
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 :: Variance (f a x) (f b x) a b
fstco (Attenuation Coercion a b
c) = Coercion (f a x) (f b x) -> Attenuation (f a x) (f b x)
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (f a x) (f b x)
forall k k k (f :: k -> k -> k) (a :: k) (b :: k) (x :: k).
Representational0 f =>
Coercion a b -> Coercion (f a x) (f b x)
rep0 Coercion a b
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 :: Variance (f x a) (f x b) a b
sndco (Attenuation Coercion a b
c) = Coercion (f x a) (f x b) -> Attenuation (f x a) (f x b)
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (f x a) (f x b)
forall k k (f :: k -> k) (a :: k) (b :: k).
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
c)

-- | Lift an 'Attenuation' contravariantly over the argument of a functiwon.
domain :: Variance (b -> x) (a -> x) a b
domain :: Variance (b -> x) (a -> x) a b
domain (Attenuation Coercion a b
c) = Coercion (b -> x) (a -> x) -> Attenuation (b -> x) (a -> x)
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion (a -> x) (b -> x) -> Coercion (b -> x) (a -> x)
forall k (a :: k) (b :: k). Coercion a b -> Coercion b a
sym (Coercion (a -> x) (b -> x) -> Coercion (b -> x) (a -> x))
-> Coercion (a -> x) (b -> x) -> Coercion (b -> x) (a -> x)
forall a b. (a -> b) -> a -> b
$ Coercion a b -> Coercion (a -> x) (b -> x)
forall k k k (f :: k -> k -> k) (a :: k) (b :: k) (x :: k).
Representational0 f =>
Coercion a b -> Coercion (f a x) (f b x)
rep0 Coercion a b
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 :: Variance (x -> a) (x -> b) a b
codomain (Attenuation Coercion a b
c) = Coercion (x -> a) (x -> b) -> Attenuation (x -> a) (x -> b)
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (x -> a) (x -> b)
forall k k (f :: k -> k) (a :: k) (b :: k).
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
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 a b -> (Attenuable a b => r) -> r
withAttenuation (Attenuation Coercion a b
Coercion) Attenuable a b => r
r = r
Attenuable a b => 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 :: Attenuation a b -> Dict (Attenuable a b)
evidence = (Attenuation a b
-> (Attenuable a b => Dict (Attenuable a b))
-> Dict (Attenuable a b)
forall k (a :: k) (b :: k) r.
Attenuation a b -> (Attenuable a b => r) -> r
`withAttenuation` Attenuable a b => Dict (Attenuable a b)
forall (a :: Constraint). a => Dict a
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 :: Attenuation (f x) (f y)
attenuation = Variance (f x) (f y) x y
forall (f :: * -> *) a b.
(Functor f, Representational f) =>
Variance (f a) (f b) a b
co Attenuation x y
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
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 :: Attenuation (f a b) (f c d)
attenuation = Variance (f a d) (f c d) a c
forall (f :: * -> * -> *) a x b.
(Bifunctor f, Representational0 f) =>
Variance (f a x) (f b x) a b
fstco Attenuation a c
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation Attenuation (f a d) (f c d)
-> Attenuation (f a b) (f a d) -> Attenuation (f a b) (f c d)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (f a b) (f a d) b d
forall (f :: * -> * -> *) x a b.
(Bifunctor f, Representational1 f) =>
Variance (f x a) (f x b) a b
sndco Attenuation b d
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation

instance (Attenuable c a, Attenuable b d)
      => Attenuable (a -> b) (c -> d) where
  attenuation :: Attenuation (a -> b) (c -> d)
attenuation = Variance (a -> d) (c -> d) c a
forall b x a. Variance (b -> x) (a -> x) a b
domain Attenuation c a
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation Attenuation (a -> d) (c -> d)
-> Attenuation (a -> b) (a -> d) -> Attenuation (a -> b) (c -> d)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (a -> b) (a -> d) b d
forall x a b. Variance (x -> a) (x -> b) a b
codomain Attenuation b d
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation

instance (Attenuable a a', Attenuable b b')
      => Attenuable (a, b) (a', b') where
  attenuation :: Attenuation (a, b) (a', b')
attenuation = Variance (a, b') (a', b') a a'
forall (f :: * -> * -> *) a x b.
(Bifunctor f, Representational0 f) =>
Variance (f a x) (f b x) a b
fstco Attenuation a a'
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation Attenuation (a, b') (a', b')
-> Attenuation (a, b) (a, b') -> Attenuation (a, b) (a', b')
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (a, b) (a, b') b b'
forall (f :: * -> * -> *) x a b.
(Bifunctor f, Representational1 f) =>
Variance (f x a) (f x b) a b
sndco Attenuation b b'
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation

instance (Attenuable a a', Attenuable b b', Attenuable c c')
      => Attenuable (a, b, c) (a', b', c') where
  attenuation :: Attenuation (a, b, c) (a', b', c')
attenuation = Attenuation (a, b', c') (a', b', c')
fst3 Attenuation (a, b', c') (a', b', c')
-> Attenuation (a, b, c) (a, b', c')
-> Attenuation (a, b, c) (a', b', c')
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (a, b, c') (a, b', c') b b'
forall (f :: * -> * -> *) a x b.
(Bifunctor f, Representational0 f) =>
Variance (f a x) (f b x) a b
fstco Attenuation b b'
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation Attenuation (a, b, c') (a, b', c')
-> Attenuation (a, b, c) (a, b, c')
-> Attenuation (a, b, c) (a, b', c')
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (a, b, c) (a, b, c') c c'
forall (f :: * -> * -> *) x a b.
(Bifunctor f, Representational1 f) =>
Variance (f x a) (f x b) a b
sndco Attenuation c c'
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation
   where
    fst3 :: Attenuation (a, b', c') (a', b', c')
    fst3 :: Attenuation (a, b', c') (a', b', c')
fst3 = case Attenuable a a' => Attenuation a a'
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation @a @a' of Attenuation Coercion a a'
Coercion -> Attenuation (a, b', c') (a', b', c')
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation

-- | Transitivity of 'Attenuation's.  See also the 'Category' instance.
trans :: Attenuation a b -> Attenuation b c -> Attenuation a c
trans :: Attenuation a b -> Attenuation b c -> Attenuation a c
trans (Attenuation Coercion a b
coAB) (Attenuation Coercion b c
coBC) =
  Coercion a c -> Attenuation a c
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion b c -> Coercion a c
forall k (a :: k) (b :: k) (c :: k).
Coercion a b -> Coercion b c -> Coercion a c
Coercion.trans Coercion a b
coAB Coercion b c
coBC)

-- | Any type is unidirectionally-coercible to itself.
refl :: Attenuation a a
refl :: Attenuation a a
refl = Coercion a a -> Attenuation a a
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation Coercion a a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

instance Category Attenuation where
  id :: Attenuation a a
id = Attenuation a a
forall k (a :: k). Attenuation a a
refl
  . :: Attenuation b c -> Attenuation a b -> Attenuation a c
(.) = (Attenuation a b -> Attenuation b c -> Attenuation a c)
-> Attenuation b c -> Attenuation a b -> Attenuation a c
forall a b c. (a -> b -> c) -> b -> a -> c
flip Attenuation a b -> Attenuation b c -> Attenuation a c
forall k (a :: k) (b :: k) (c :: k).
Attenuation a b -> Attenuation b c -> Attenuation a c
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 = Coercion a b -> Attenuation a b
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation Coercion a b
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion