rerefined-0.8.0: Refinement types, again
Safe HaskellNone
LanguageGHC2021

Rerefined.Refine.TH

Synopsis

Documentation

refineTH :: forall {k} (p :: k) a (m :: Type -> Type). (Refine p a, Lift a, Quote m, MonadFail m) => a -> Code m (Refined p a) Source #

Refine a with predicate p at compile time via Template Haskell.

Use like $$(refineTH @p a).

refine1TH :: forall {k} {k1} (p :: k) f (a :: k1) (m :: Type -> Type). (Refine1 p f, Lift (f a), Quote m, MonadFail m) => f a -> Code m (Refined1 p f a) Source #

Refine f a with functor predicate p at compile time via Template Haskell.

Use like $$(refine1TH @p a).