Generalised Coercible

Coercible.hs

-- These coercions could probably be generated automatically with a
-- type class and this plugin:
--   https://github.com/noughtmare/transitive-constraint-plugin

{-# LANGUAGE UnboxedTuples, UnliftedNewtypes, ExplicitNamespaces #-}
{-# LANGUAGE RoleAnnotations, DataKinds, QuantifiedConstraints #-}

module Coercible (

  Coercible(..),

  type (~~>),
  refl, (~), symm,

  Repr,
  Positive, pos,
  Negative, neg,

  -- Extension
  Coercion(..),
  useCo,

  -- User-space Utils / Examples
  sub, contrasub,
  Repr2, bisub,

) where

-- base
import GHC.Exts (TYPE, ZeroBitType, LiftedRep, UnliftedRep)
import Unsafe.Coerce (unsafeCoerce, unsafeCoerceUnlifted)

import Data.Kind (Type, Constraint)
import Data.Coerce qualified as Symm
import Data.Functor.Contravariant (Contravariant(..))
import Data.Bifunctor (Bifunctor(..))


class Coercible rr where
  coerce :: forall (a :: TYPE rr) (b :: TYPE rr). a ~~> b -> a -> b

-- Further instances to be written at need.
instance Coercible   LiftedRep where coerce !_ = unsafeCoerce
instance Coercible UnliftedRep where coerce !_ = unsafeCoerceUnlifted


type role (~~>) nominal nominal
type (~~>) :: k -> k -> ZeroBitType
newtype a ~~> b = UnsafeCoercion (# #)

refl :: forall {k} (a :: k). (# #) -> a ~~> a
refl = UnsafeCoercion

(~) :: forall {k} (a :: k) (b :: k) (c :: k). a ~~> b -> b ~~> c -> a ~~> c
!_ ~ !_ = UnsafeCoercion (# #)

symm :: forall {k} (a :: k) (b :: k). Symm.Coercible a b => a ~~> b
symm = UnsafeCoercion (# #)


type Repr :: (k1 -> k2) -> Constraint
type Repr f = forall a b. Symm.Coercible a b => Symm.Coercible (f a) (f b)

type HO k = forall rr1 rr2. (TYPE rr1 -> TYPE rr2) -> k

type Positive :: HO Type
type Positive f = forall a b. (a -> b) -> f a -> f b

-- `Positive f` means that the symmetric coercion `Repr f` depends upon is
-- only used /forwards/, so we can safely substitute a forward coercion.
pos
  :: forall {rr1} {rr2} a b (f :: TYPE rr1 -> TYPE rr2)
   . Repr f => Positive f -> a ~~> b -> f a ~~> f b
pos !_ !_ = UnsafeCoercion (# #)

type Negative :: HO Type
type Negative f = forall a b. (b -> a) -> f a -> f b

-- `Negative f` means that the symmetric coercion `Repr f` depends upon is
-- only used /backwards/, so we can safely substitute a backward coercion.
neg
  :: forall {rr1} {rr2} a b (f :: TYPE rr1 -> TYPE rr2)
   . Repr f => Negative f -> b ~~> a -> f a ~~> f b
neg !_ !_ = UnsafeCoercion (# #)


{-# WARNING in "x-not-for-direct-use" co "Use via `coerce` and `useCo`." #-}

-- | A type class for user declared coercions.
--   Law: @a@ and @b@ have the same runtime representation.
type  Coercion :: TYPE rr -> TYPE rr -> Constraint
class Coercion a b where
  co :: a -> b

useCo :: forall {rr} (a :: TYPE rr) (b :: TYPE rr). Coercion a b => a ~~> b
useCo = UnsafeCoercion (# #)


-- `pos` and `neg` may look limited, but they really go a long way.
-- Here we implement `sub`, `contrasub` and `bisub` safely in user-space.
-- The `Profunctor` equivalent would be the same as `bisub`, but using `neg`
-- and `lmap` in place of `pos` and `first`.

sub :: (Repr f, Functor f) => a ~~> b -> f a ~~> f b
sub = pos fmap

contrasub :: (Repr f, Contravariant f) => b ~~> a -> f a ~~> f b
contrasub = neg contramap

type Repr2 :: (k1 -> k2 -> k3) -> Constraint
type Repr2 p
   = forall a b c d
   . (Symm.Coercible a c, Symm.Coercible b d)
  => Symm.Coercible (p a b) (p c d)

newtype Flip p a b = Flip{ unFlip :: p b a }

bisub
  :: forall p a b c d
   . (Repr2 p, Bifunctor p)
  => a ~~> c -> b ~~> d -> p a b ~~> p c d
bisub ac bd
  = symm @(p a b) @(Flip p b a)
  ~ pos (\f -> Flip . first f . unFlip) ac
  ~ symm @(Flip p b c) @(p c b)
  ~ sub bd