rerefined-0.2.0: Refinement types, again
Safe HaskellSafe-Inferred
LanguageGHC2021

Rerefined.Refine.Unsafe

Description

Unsafe refining.

Sometimes, you know that your value satisfies some predicate before validating. For those cases, we permit skipping validation and obtaining a refined value "for free".

You should be certain that your value cannot possibly fail the predicate you are skipping. A good practice is to annotate all call sites with an explanation of why the usage is safe.

Synopsis

Refined

data Refined p a Source #

a refined with predicate p.

Instances

Instances details
Lift a => Lift (Refined p a :: Type) Source # 
Instance details

Defined in Rerefined.Refined

Methods

lift :: Quote m => Refined p a -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => Refined p a -> Code m (Refined p a) #

Show a => Show (Refined p a) Source # 
Instance details

Defined in Rerefined.Refined

Methods

showsPrec :: Int -> Refined p a -> ShowS #

show :: Refined p a -> String #

showList :: [Refined p a] -> ShowS #

unsafeRefine :: a -> Refined p a Source #

Construct a Refined without validating the predicate p.

Unsafe. Use only when you can manually prove that the predicate holds.

unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a Source #

Replace a Refined's predicate without validating the new prdicate pNew.

Unsafe. Use only when you can manually prove that the new predicate holds.

Refined1

data Refined1 p f a Source #

f a refined with predicate p.

Instances

Instances details
Lift (f a) => Lift (Refined1 p f a :: Type) Source # 
Instance details

Defined in Rerefined.Refined1

Methods

lift :: Quote m => Refined1 p f a -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => Refined1 p f a -> Code m (Refined1 p f a) #

Functor f => Functor (Refined1 p f) Source # 
Instance details

Defined in Rerefined.Refined1

Methods

fmap :: (a -> b) -> Refined1 p f a -> Refined1 p f b #

(<$) :: a -> Refined1 p f b -> Refined1 p f a #

Show (f a) => Show (Refined1 p f a) Source # 
Instance details

Defined in Rerefined.Refined1

Methods

showsPrec :: Int -> Refined1 p f a -> ShowS #

show :: Refined1 p f a -> String #

showList :: [Refined1 p f a] -> ShowS #

unsafeRefine1 :: f a -> Refined1 p f a Source #

Construct a Refined1 without validating the predicate p.

Unsafe. Use only when you can manually prove that the predicate holds.

unsafeRerefine1 :: forall pNew pOld f a. Refined1 pOld f a -> Refined1 pNew f a Source #

Replace a Refined1's predicate without validating the new prdicate pNew.

Unsafe. Use only when you can manually prove that the new predicate holds.