{-# LANGUAGE UndecidableInstances #-}

module Plutarch.Internal.Subtype (
  PSubtypeRelation (PSubtypeRelation, PNoSubtypeRelation),
  PSubtype,
  PSubtype',
  pupcast,
  pto,
  punsafeDowncast,
) where

import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import GHC.TypeError (
  ErrorMessage (ShowType, Text, (:<>:)),
  TypeError,
 )
import Plutarch.Internal.PlutusType (
  PlutusType (PInner),
 )
import Plutarch.Internal.Term (S, Term, punsafeCoerce)
import Plutarch.Internal.Witness (witness)

data PSubtypeRelation
  = PSubtypeRelation
  | PNoSubtypeRelation

type family Helper (a :: S -> Type) (b :: S -> Type) (bi :: S -> Type) :: PSubtypeRelation where
  Helper _ b b = 'PNoSubtypeRelation
  Helper a _ bi = PSubtype' a bi

type family PSubtype' (a :: S -> Type) (b :: S -> Type) :: PSubtypeRelation where
  PSubtype' a a = 'PSubtypeRelation
  PSubtype' a b = Helper a b (PInner b)

{- | @PSubtype a b@ constitutes a subtyping relation between @a@ and @b@.
 This concretely means that `\(x :: Term s b) -> punsafeCoerce x :: Term s a`
 is legal and sound.

 You can not make an instance for this yourself.
 You must use the 'PInner' type family of 'PlutusType' to get this instance.

 Caveat: Only @PInner a POpaque@ is considered unfortunately, as otherwise
 getting GHC to figure out the relation with multiple supertypes is quite hard.

 Subtyping is transitive.
-}
type family PSubtypeHelper (a :: S -> Type) (b :: S -> Type) (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 :: S -> Type) (b :: S -> Type) :: 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 :: S -> Type) (b :: S -> Type) (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 :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce

{- |
  Safely coerce from a Term to it's 'PInner' representation.
-}
pto :: forall (a :: S -> Type) (s :: S). Term s a -> Term s (PInner a)
pto :: forall (a :: S -> Type) (s :: S). Term s a -> Term s (PInner a)
pto = Term s a -> Term s (PInner a)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce

{- |
  Unsafely coerce from the 'PInner' representation of a Term,
  assuming that the value is a safe construction of the Term.
-}
punsafeDowncast :: Term s (PInner a) -> Term s a
punsafeDowncast :: forall (s :: S) (a :: S -> Type). Term s (PInner a) -> Term s a
punsafeDowncast = Term s (PInner a) -> Term s a
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce