{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_HADDOCK hide #-}

module Data.Coerce.Directed.Internal (module Data.Coerce.Directed.Internal) where

import Data.Coerce (Coercible)
import Data.Kind (Constraint, Type)
import Data.Type.Ord
import GHC.Base (Multiplicity (..))
import Generics.Linear
import Prelude.Linear
import Unsafe.Coerce (unsafeCoerce)
import Unsafe.Linear qualified as Unsafe

infix 4 <:

-- Orphan instance!
type instance Compare (a :: Multiplicity) (b :: Multiplicity) = CmpMult One Many

type CmpMult :: Multiplicity -> Multiplicity -> Ordering
type family CmpMult p q where
  CmpMult One One = EQ
  CmpMult One Many = LT
  CmpMult Many One = GT
  CmpMult Many Many = EQ

data SubtypeWitness a b = UnsafeSubtype

class a <: b where
  subtype :: SubtypeWitness a b

upcast :: (a <: b) => a %1 -> b
upcast :: forall a b. (a <: b) => a %1 -> b
upcast = (a -> b) %1 -> a %1 -> b
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear a -> b
forall a b. a -> b
unsafeCoerce

instance {-# INCOHERENT #-} (Coercible a b) => a <: b where
  subtype :: SubtypeWitness a b
subtype = SubtypeWitness a b
forall {k} {k} (a :: k) (b :: k). SubtypeWitness a b
UnsafeSubtype

newtype AsCoercible a = AsCoercible {forall a. AsCoercible a -> a
runAsCoercible :: a}

instance (Coercible a b) => a <: AsCoercible b where
  subtype :: SubtypeWitness a (AsCoercible b)
subtype = SubtypeWitness a (AsCoercible b)
forall {k} {k} (a :: k) (b :: k). SubtypeWitness a b
UnsafeSubtype

deriving via
  Generically [b]
  instance
    (a <: b) => [a] <: [b]

deriving via
  Generically (a', b')
  instance
    (a <: a', b <: b') => (a, b) <: (a', b')

deriving via
  Generically (Either a' b')
  instance
    (a <: a', b <: b') => Either a b <: Either a' b'

deriving via
  Generically (a', b', c')
  instance
    (a <: a', b <: b', c <: c') => (a, b, c) <: (a', b', c')

instance
  (a' <: a, b <: b', p Data.Type.Ord.<= q) =>
  (a %p -> b) <: (a' %q -> b')
  where
  subtype :: SubtypeWitness (a %p -> b) (a' %q -> b')
subtype = SubtypeWitness (a %p -> b) (a' %q -> b')
forall {k} {k} (a :: k) (b :: k). SubtypeWitness a b
UnsafeSubtype

type GSubtype :: (k -> Type) -> (k -> Type) -> Constraint
class GSubtype f g where
  gsubtype :: SubtypeWitness f g

gupcast :: (GSubtype f g) => f a %1 -> g a
gupcast :: forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
GSubtype f g =>
f a %1 -> g a
gupcast = (f a -> g a) %1 -> f a %1 -> g a
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear f a -> g a
forall a b. a -> b
unsafeCoerce

instance (a <: b) => GSubtype (K1 i a) (K1 i b) where
  gsubtype :: SubtypeWitness (K1 i a) (K1 i b)
gsubtype = SubtypeWitness (K1 i a) (K1 i b)
forall {k} {k} (a :: k) (b :: k). SubtypeWitness a b
UnsafeSubtype

instance {-# INCOHERENT #-} GSubtype f f where
  gsubtype :: SubtypeWitness f f
gsubtype = SubtypeWitness f f
forall {k} {k} (a :: k) (b :: k). SubtypeWitness a b
UnsafeSubtype

instance (GSubtype f g) => GSubtype (MP1 p f) (MP1 p g) where
  gsubtype :: SubtypeWitness (MP1 p f) (MP1 p g)
gsubtype = SubtypeWitness (MP1 p f) (MP1 p g)
forall {k} {k} (a :: k) (b :: k). SubtypeWitness a b
UnsafeSubtype

instance (GSubtype f g) => GSubtype (M1 i c f) (M1 i c g) where
  gsubtype :: SubtypeWitness (M1 i c f) (M1 i c g)
gsubtype = SubtypeWitness (M1 i c f) (M1 i c g)
forall {k} {k} (a :: k) (b :: k). SubtypeWitness a b
UnsafeSubtype

instance (GSubtype f f', GSubtype g g') => GSubtype (f :*: g) (f' :*: g') where
  gsubtype :: SubtypeWitness (f :*: g) (f' :*: g')
gsubtype = SubtypeWitness (f :*: g) (f' :*: g')
forall {k} {k} (a :: k) (b :: k). SubtypeWitness a b
UnsafeSubtype

instance (GSubtype l l', GSubtype r r') => GSubtype (l :+: r) (l' :+: r') where
  gsubtype :: SubtypeWitness (l :+: r) (l' :+: r')
gsubtype = SubtypeWitness (l :+: r) (l' :+: r')
forall {k} {k} (a :: k) (b :: k). SubtypeWitness a b
UnsafeSubtype

type GenericSubtype a b = (Generic a, Generic b, GSubtype (Rep a) (Rep b))

instance (GenericSubtype a b) => a <: Generically b where
  subtype :: SubtypeWitness a (Generically b)
subtype = SubtypeWitness a (Generically b)
forall {k} {k} (a :: k) (b :: k). SubtypeWitness a b
UnsafeSubtype

genericUpcast :: (GenericSubtype a b) => a %1 -> b
genericUpcast :: forall a b. GenericSubtype a b => a %1 -> b
genericUpcast = Rep b (ZonkAny 0) %1 -> b
forall a p (m :: Multiplicity). Generic a => Rep a p %m -> a
forall p (m :: Multiplicity). Rep b p %m -> b
to (Rep b (ZonkAny 0) %1 -> b)
-> (a %1 -> Rep b (ZonkAny 0)) -> a %1 -> b
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. Rep a (ZonkAny 0) %1 -> Rep b (ZonkAny 0)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
GSubtype f g =>
f a %1 -> g a
gupcast (Rep a (ZonkAny 0) %1 -> Rep b (ZonkAny 0))
-> (a %1 -> Rep a (ZonkAny 0)) -> a %1 -> Rep b (ZonkAny 0)
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> Rep a (ZonkAny 0)
forall a p (m :: Multiplicity). Generic a => a %m -> Rep a p
forall p (m :: Multiplicity). a %m -> Rep a p
from