Safe Haskell	Safe-Inferred
Language	GHC2021

Plutarch.Reducible

Synopsis

type family Reduce (x :: Type) :: Type where ...
newtype NoReduce a = NoReduce a
reduce :: Coercible a (Reduce a) => a -> Reduce a

Documentation

type family Reduce (x :: Type) :: Type where ... Source #

This class provides a work-around for partially applying type families of kind a, where a is either Type or b -> c where c satisfies the same constraint.

Given a type family F : A -> Type, you can make the following type F' :: A -> Type newtype F' (a :: A) = F' (NoReduce (F a)) deriving stock Generic It is then true that forall a. Reduce (F' a) ~ F a.

Equations

Reduce (NoReduce a) = a
Reduce (Term s a) = Term s a
Reduce (a -> b) = a -> b
Reduce x = GReduce x (Rep x)

newtype NoReduce a Source #

Constructors

NoReduce a

reduce :: Coercible a (Reduce a) => a -> Reduce a Source #