{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Plutarch.Repr.Newtype (
  DeriveAsNewtype (DeriveAsNewtype, unDeriveAsNewtype),
) where

import Data.Kind (Type)
import GHC.Exts (Any)
import Generics.SOP (
  Code,
  I (I),
  NP (Nil, (:*)),
  NS (Z),
  SOP (SOP),
 )
import Generics.SOP qualified as SOP
import Generics.SOP.Constraint (Head)
import Plutarch.Internal.PlutusType (
  PContravariant',
  PCovariant',
  PInner,
  PVariant',
  PlutusType,
  pcon',
  pmatch',
 )
import Plutarch.Internal.Term (S, Term)

-- | @since WIP
newtype DeriveAsNewtype (a :: S -> Type) s = DeriveAsNewtype
  { forall (a :: S -> Type) (s :: S). DeriveAsNewtype a s -> a s
unDeriveAsNewtype :: a s
  -- ^ @since WIP
  }

-- Helpers

type family UnTermSingle (x :: Type) :: S -> Type where
  UnTermSingle (Term _ a) = a

class (SOP.Generic (a s), Code (a s) ~ '[ '[Term s pt]]) => H s a pt
instance (SOP.Generic (a s), Code (a s) ~ '[ '[Term s pt]]) => H s a pt

instance
  forall (a :: S -> Type) (pt :: S -> Type).
  ( pt ~ UnTermSingle (Head (Head (Code (a Any))))
  , forall s. H s a pt
  ) =>
  PlutusType (DeriveAsNewtype a)
  where
  type PInner (DeriveAsNewtype a) = UnTermSingle (Head (Head (Code (a Any))))
  type PCovariant' (DeriveAsNewtype a) = PCovariant' a
  type PContravariant' (DeriveAsNewtype a) = PContravariant' a
  type PVariant' (DeriveAsNewtype a) = PVariant' a

  -- This breaks without type signature because of (s :: S) needs to be bind.
  pcon' :: forall s. DeriveAsNewtype a s -> Term s (PInner (DeriveAsNewtype a))
  pcon' :: forall (s :: S).
DeriveAsNewtype a s -> Term s (PInner (DeriveAsNewtype a))
pcon' (DeriveAsNewtype a s
x) =
    case NS
  @[Type]
  (NP @Type I)
  ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> NP @Type I ((':) @Type (Term s pt) ('[] @Type))
forall {k} (f :: k -> Type) (x :: k).
NS @k f ((':) @k x ('[] @k)) -> f x
SOP.unZ (NS
   @[Type]
   (NP @Type I)
   ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
 -> NP @Type I ((':) @Type (Term s pt) ('[] @Type)))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> NP @Type I ((':) @Type (Term s pt) ('[] @Type))
forall a b. (a -> b) -> a -> b
$ SOP
  @Type
  I
  ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall {k} (f :: k -> Type) (xss :: [[k]]).
SOP @k f xss -> NS @[k] (NP @k f) xss
SOP.unSOP (a s -> Rep (a s)
forall a. Generic a => a -> Rep a
SOP.from a s
x :: SOP I '[ '[Term s pt]]) of
      (I x
x) :* NP @Type I xs
Nil -> x
Term s pt
x :: Term s pt

  pmatch' :: forall s b. Term s (PInner (DeriveAsNewtype a)) -> (DeriveAsNewtype a s -> Term s b) -> Term s b
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (DeriveAsNewtype a))
-> (DeriveAsNewtype a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveAsNewtype a))
x DeriveAsNewtype a s -> Term s b
f =
    DeriveAsNewtype a s -> Term s b
f (a s -> DeriveAsNewtype a s
forall (a :: S -> Type) (s :: S). a s -> DeriveAsNewtype a s
DeriveAsNewtype (a s -> DeriveAsNewtype a s) -> a s -> DeriveAsNewtype a s
forall a b. (a -> b) -> a -> b
$ Rep (a s) -> a s
forall a. Generic a => Rep a -> a
SOP.to ((NS
  @[Type]
  (NP @Type I)
  ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> SOP
     @Type
     I
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS
   @[Type]
   (NP @Type I)
   ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
 -> SOP
      @Type
      I
      ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type])))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> SOP
     @Type
     I
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall a b. (a -> b) -> a -> b
$ NP @Type I ((':) @Type (Term s pt) ('[] @Type))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z (NP @Type I ((':) @Type (Term s pt) ('[] @Type))
 -> NS
      @[Type]
      (NP @Type I)
      ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type])))
-> NP @Type I ((':) @Type (Term s pt) ('[] @Type))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall a b. (a -> b) -> a -> b
$ Term s (PInner (DeriveAsNewtype a))
-> I (Term s (PInner (DeriveAsNewtype a)))
forall a. a -> I a
I Term s (PInner (DeriveAsNewtype a))
x I (Term s (PInner (DeriveAsNewtype a)))
-> NP @Type I ('[] @Type)
-> NP
     @Type
     I
     ((':) @Type (Term s (PInner (DeriveAsNewtype a))) ('[] @Type))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @Type I ('[] @Type)
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) :: SOP I '[ '[Term s pt]]))