{-# LANGUAGE UndecidableInstances #-}
module Plutarch.Reducible (Reduce, NoReduce (..), reduce) where
import Data.Coerce (Coercible, coerce)
import Data.Kind (Type)
import GHC.Generics (C1, D1, Rec0, Rep, S1, pattern MetaData)
import Plutarch.Internal.Term (Term)
newtype NoReduce a = NoReduce a
type family GReduce (def :: Type) (rep :: Type -> Type) :: Type where
GReduce _ (D1 ('MetaData _ _ _ 'True) (C1 _ (S1 _ (Rec0 (x :: Type))))) = Reduce x
GReduce def _ = def
type family Reduce (x :: Type) :: Type where
Reduce (NoReduce a) = a
Reduce (Term s a) = Term s a
Reduce (a -> b) = a -> b
Reduce x = GReduce x (Rep x)
reduce :: Coercible a (Reduce a) => a -> Reduce a
reduce :: forall a. Coercible @Type a (Reduce a) => a -> Reduce a
reduce = a -> Reduce a
forall a b. Coercible @Type a b => a -> b
coerce