{-# LANGUAGE UndecidableInstances #-}
module Plutarch.Internal.Subtype (
PSubtypeRelation (PSubtypeRelation, PNoSubtypeRelation),
PSubtype,
PSubtype',
pupcast,
pupcastF,
pdowncastF,
) where
import Data.Kind (Constraint)
import Data.Proxy (Proxy (Proxy))
import GHC.TypeError (
ErrorMessage (ShowType, Text, (:<>:)),
TypeError,
)
import Plutarch.Internal.PlutusType (
PContravariant,
PCovariant,
PlutusType (PInner),
)
import Plutarch.Internal.Term (PType, Term, punsafeCoerce)
import Plutarch.Internal.Witness (witness)
data PSubtypeRelation
= PSubtypeRelation
| PNoSubtypeRelation
type family Helper (a :: PType) (b :: PType) (bi :: PType) :: PSubtypeRelation where
Helper _ b b = 'PNoSubtypeRelation
Helper a _ bi = PSubtype' a bi
type family PSubtype' (a :: PType) (b :: PType) :: PSubtypeRelation where
PSubtype' a a = 'PSubtypeRelation
PSubtype' a b = Helper a b (PInner b)
type family PSubtypeHelper (a :: PType) (b :: PType) (r :: PSubtypeRelation) :: Constraint where
PSubtypeHelper a b 'PNoSubtypeRelation =
TypeError
( 'Text "\""
':<>: 'ShowType b
':<>: 'Text "\""
':<>: 'Text " is not a subtype of "
':<>: 'Text "\""
':<>: 'ShowType a
':<>: 'Text "\""
)
PSubtypeHelper _ _ 'PSubtypeRelation = ()
type family PSubtype (a :: PType) (b :: PType) :: Constraint where
PSubtype a b = (PSubtype' a b ~ 'PSubtypeRelation, PSubtypeHelper a b (PSubtype' a b))
pupcast :: forall a b s. PSubtype a b => Term s b -> Term s a
pupcast :: forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast = let ()
_ = Proxy @Constraint (PSubtype a b) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(PSubtype a b)) in Term s b -> Term s a
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce
pupcastF :: forall a b (p :: PType -> PType) s. (PSubtype a b, PCovariant p) => Proxy p -> Term s (p b) -> Term s (p a)
pupcastF :: forall (a :: PType) (b :: PType) (p :: PType -> PType) (s :: S).
(PSubtype a b, PCovariant p) =>
Proxy @(PType -> PType) p -> Term s (p b) -> Term s (p a)
pupcastF Proxy @(PType -> PType) p
_ =
let ()
_ = Proxy @Constraint (PSubtype a b) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(PSubtype a b))
()
_ = Proxy @Constraint (PCovariant p) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(PCovariant p))
in Term s (p b) -> Term s (p a)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce
pdowncastF :: forall a b (p :: PType -> PType) s. (PSubtype a b, PContravariant p) => Proxy p -> Term s (p a) -> Term s (p b)
pdowncastF :: forall (a :: PType) (b :: PType) (p :: PType -> PType) (s :: S).
(PSubtype a b, PContravariant p) =>
Proxy @(PType -> PType) p -> Term s (p a) -> Term s (p b)
pdowncastF Proxy @(PType -> PType) p
_ =
let ()
_ = Proxy @Constraint (PSubtype a b) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(PSubtype a b))
()
_ = Proxy @Constraint (PContravariant p) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(PContravariant p))
in Term s (p a) -> Term s (p b)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce