{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Plutarch.TryFrom (
PTryFrom (..),
ptryFrom,
PSubtypeRelation (..),
PSubtype,
PSubtype',
pupcast,
pupcastF,
pdowncastF,
) where
import Data.Kind (Constraint)
import Data.Proxy (Proxy (Proxy))
import Plutarch.Internal (PType, Term, punsafeCoerce)
import Plutarch.Internal.PlutusType (PContravariant, PCovariant, PInner)
import Plutarch.Internal.Witness (witness)
import Plutarch.Reducible (Reduce)
import GHC.TypeLits (ErrorMessage (ShowType, Text, (:<>:)), TypeError)
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))
class PSubtype a b => PTryFrom (a :: PType) (b :: PType) where
type PTryFromExcess a b :: PType
type PTryFromExcess a b = PTryFromExcess a (PInner b)
ptryFrom' :: forall s r. Term s a -> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r) -> Term s r
default ptryFrom' :: forall s r. (PTryFrom a (PInner b), PTryFromExcess a b ~ PTryFromExcess a (PInner b)) => Term s a -> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r) -> Term s r
ptryFrom' Term s a
opq (Term s b, Reduce (PTryFromExcess a b s)) -> Term s r
f = forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PInner b) @a Term s a
opq \(Term s (PInner b)
inn, Reduce (PTryFromExcess a (PInner b) s)
exc) -> (Term s b, Reduce (PTryFromExcess a b s)) -> Term s r
f (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PInner b)
inn, Reduce (PTryFromExcess a (PInner b) s)
exc)
ptryFrom :: forall b a s r. PTryFrom a b => Term s a -> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r) -> Term s r
ptryFrom :: forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom = forall (a :: PType) (b :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom'
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 ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(PSubtype a b)) in forall (s :: S) (a :: PType) (b :: PType). 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 ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(PSubtype a b))
()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(PCovariant p))
in forall (s :: S) (a :: PType) (b :: PType). 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 ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(PSubtype a b))
()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(PContravariant p))
in forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce