module Refined.WithRefine
(
WithRefine
, withRefine, withoutRefine
, PredicateStatus(..)
, Strong, Weak
, enforce
, enforceFail
, unenforce
, enforcedToRefined
, refinedToEnforced
, reallyUnsafeEnforce
, unsafeWithRefine
, WithRefineRep
) where
import Refined
import Refined.Unsafe
import Data.Proxy
import Control.DeepSeq ( NFData )
import Data.Hashable ( Hashable )
import GHC.Generics ( Generic )
import Data.Aeson
import Control.Exception
newtype WithRefine (ps :: PredicateStatus) p a
= WithRefine {
forall {k} (ps :: PredicateStatus) (p :: k) a.
WithRefine ps p a -> a
withoutRefine :: a
} deriving (Eq (WithRefine ps p a)
Eq (WithRefine ps p a)
-> (Int -> WithRefine ps p a -> Int)
-> (WithRefine ps p a -> Int)
-> Hashable (WithRefine ps p a)
Int -> WithRefine ps p a -> Int
WithRefine ps p a -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall {ps :: PredicateStatus} {k} {p :: k} {a}.
Hashable a =>
Eq (WithRefine ps p a)
forall (ps :: PredicateStatus) k (p :: k) a.
Hashable a =>
Int -> WithRefine ps p a -> Int
forall (ps :: PredicateStatus) k (p :: k) a.
Hashable a =>
WithRefine ps p a -> Int
hash :: WithRefine ps p a -> Int
$chash :: forall (ps :: PredicateStatus) k (p :: k) a.
Hashable a =>
WithRefine ps p a -> Int
hashWithSalt :: Int -> WithRefine ps p a -> Int
$chashWithSalt :: forall (ps :: PredicateStatus) k (p :: k) a.
Hashable a =>
Int -> WithRefine ps p a -> Int
Hashable, WithRefine ps p a -> ()
(WithRefine ps p a -> ()) -> NFData (WithRefine ps p a)
forall a. (a -> ()) -> NFData a
forall (ps :: PredicateStatus) k (p :: k) a.
NFData a =>
WithRefine ps p a -> ()
rnf :: WithRefine ps p a -> ()
$crnf :: forall (ps :: PredicateStatus) k (p :: k) a.
NFData a =>
WithRefine ps p a -> ()
NFData, WithRefine ps p a -> WithRefine ps p a -> Bool
(WithRefine ps p a -> WithRefine ps p a -> Bool)
-> (WithRefine ps p a -> WithRefine ps p a -> Bool)
-> Eq (WithRefine ps p a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (ps :: PredicateStatus) k (p :: k) a.
Eq a =>
WithRefine ps p a -> WithRefine ps p a -> Bool
/= :: WithRefine ps p a -> WithRefine ps p a -> Bool
$c/= :: forall (ps :: PredicateStatus) k (p :: k) a.
Eq a =>
WithRefine ps p a -> WithRefine ps p a -> Bool
== :: WithRefine ps p a -> WithRefine ps p a -> Bool
$c== :: forall (ps :: PredicateStatus) k (p :: k) a.
Eq a =>
WithRefine ps p a -> WithRefine ps p a -> Bool
Eq, Eq (WithRefine ps p a)
Eq (WithRefine ps p a)
-> (WithRefine ps p a -> WithRefine ps p a -> Ordering)
-> (WithRefine ps p a -> WithRefine ps p a -> Bool)
-> (WithRefine ps p a -> WithRefine ps p a -> Bool)
-> (WithRefine ps p a -> WithRefine ps p a -> Bool)
-> (WithRefine ps p a -> WithRefine ps p a -> Bool)
-> (WithRefine ps p a -> WithRefine ps p a -> WithRefine ps p a)
-> (WithRefine ps p a -> WithRefine ps p a -> WithRefine ps p a)
-> Ord (WithRefine ps p a)
WithRefine ps p a -> WithRefine ps p a -> Bool
WithRefine ps p a -> WithRefine ps p a -> Ordering
WithRefine ps p a -> WithRefine ps p a -> WithRefine ps p a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {ps :: PredicateStatus} {k} {p :: k} {a}.
Ord a =>
Eq (WithRefine ps p a)
forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> WithRefine ps p a -> Bool
forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> WithRefine ps p a -> Ordering
forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> WithRefine ps p a -> WithRefine ps p a
min :: WithRefine ps p a -> WithRefine ps p a -> WithRefine ps p a
$cmin :: forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> WithRefine ps p a -> WithRefine ps p a
max :: WithRefine ps p a -> WithRefine ps p a -> WithRefine ps p a
$cmax :: forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> WithRefine ps p a -> WithRefine ps p a
>= :: WithRefine ps p a -> WithRefine ps p a -> Bool
$c>= :: forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> WithRefine ps p a -> Bool
> :: WithRefine ps p a -> WithRefine ps p a -> Bool
$c> :: forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> WithRefine ps p a -> Bool
<= :: WithRefine ps p a -> WithRefine ps p a -> Bool
$c<= :: forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> WithRefine ps p a -> Bool
< :: WithRefine ps p a -> WithRefine ps p a -> Bool
$c< :: forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> WithRefine ps p a -> Bool
compare :: WithRefine ps p a -> WithRefine ps p a -> Ordering
$ccompare :: forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> WithRefine ps p a -> Ordering
Ord) via a
deriving stock ((forall x. WithRefine ps p a -> Rep (WithRefine ps p a) x)
-> (forall x. Rep (WithRefine ps p a) x -> WithRefine ps p a)
-> Generic (WithRefine ps p a)
forall x. Rep (WithRefine ps p a) x -> WithRefine ps p a
forall x. WithRefine ps p a -> Rep (WithRefine ps p a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (ps :: PredicateStatus) k (p :: k) a x.
Rep (WithRefine ps p a) x -> WithRefine ps p a
forall (ps :: PredicateStatus) k (p :: k) a x.
WithRefine ps p a -> Rep (WithRefine ps p a) x
$cto :: forall (ps :: PredicateStatus) k (p :: k) a x.
Rep (WithRefine ps p a) x -> WithRefine ps p a
$cfrom :: forall (ps :: PredicateStatus) k (p :: k) a x.
WithRefine ps p a -> Rep (WithRefine ps p a) x
Generic, Int -> WithRefine ps p a -> ShowS
[WithRefine ps p a] -> ShowS
WithRefine ps p a -> String
(Int -> WithRefine ps p a -> ShowS)
-> (WithRefine ps p a -> String)
-> ([WithRefine ps p a] -> ShowS)
-> Show (WithRefine ps p a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (ps :: PredicateStatus) k (p :: k) a.
Show a =>
Int -> WithRefine ps p a -> ShowS
forall (ps :: PredicateStatus) k (p :: k) a.
Show a =>
[WithRefine ps p a] -> ShowS
forall (ps :: PredicateStatus) k (p :: k) a.
Show a =>
WithRefine ps p a -> String
showList :: [WithRefine ps p a] -> ShowS
$cshowList :: forall (ps :: PredicateStatus) k (p :: k) a.
Show a =>
[WithRefine ps p a] -> ShowS
show :: WithRefine ps p a -> String
$cshow :: forall (ps :: PredicateStatus) k (p :: k) a.
Show a =>
WithRefine ps p a -> String
showsPrec :: Int -> WithRefine ps p a -> ShowS
$cshowsPrec :: forall (ps :: PredicateStatus) k (p :: k) a.
Show a =>
Int -> WithRefine ps p a -> ShowS
Show, (forall m. Monoid m => WithRefine ps p m -> m)
-> (forall m a. Monoid m => (a -> m) -> WithRefine ps p a -> m)
-> (forall m a. Monoid m => (a -> m) -> WithRefine ps p a -> m)
-> (forall a b. (a -> b -> b) -> b -> WithRefine ps p a -> b)
-> (forall a b. (a -> b -> b) -> b -> WithRefine ps p a -> b)
-> (forall b a. (b -> a -> b) -> b -> WithRefine ps p a -> b)
-> (forall b a. (b -> a -> b) -> b -> WithRefine ps p a -> b)
-> (forall a. (a -> a -> a) -> WithRefine ps p a -> a)
-> (forall a. (a -> a -> a) -> WithRefine ps p a -> a)
-> (forall a. WithRefine ps p a -> [a])
-> (forall a. WithRefine ps p a -> Bool)
-> (forall a. WithRefine ps p a -> Int)
-> (forall a. Eq a => a -> WithRefine ps p a -> Bool)
-> (forall a. Ord a => WithRefine ps p a -> a)
-> (forall a. Ord a => WithRefine ps p a -> a)
-> (forall a. Num a => WithRefine ps p a -> a)
-> (forall a. Num a => WithRefine ps p a -> a)
-> Foldable (WithRefine ps p)
forall a. Eq a => a -> WithRefine ps p a -> Bool
forall a. Num a => WithRefine ps p a -> a
forall a. Ord a => WithRefine ps p a -> a
forall m. Monoid m => WithRefine ps p m -> m
forall a. WithRefine ps p a -> Bool
forall a. WithRefine ps p a -> Int
forall a. WithRefine ps p a -> [a]
forall a. (a -> a -> a) -> WithRefine ps p a -> a
forall m a. Monoid m => (a -> m) -> WithRefine ps p a -> m
forall b a. (b -> a -> b) -> b -> WithRefine ps p a -> b
forall a b. (a -> b -> b) -> b -> WithRefine ps p a -> b
forall (ps :: PredicateStatus) k (p :: k) a.
Eq a =>
a -> WithRefine ps p a -> Bool
forall (ps :: PredicateStatus) k (p :: k) a.
Num a =>
WithRefine ps p a -> a
forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> a
forall (ps :: PredicateStatus) k (p :: k) m.
Monoid m =>
WithRefine ps p m -> m
forall (ps :: PredicateStatus) k (p :: k) a.
WithRefine ps p a -> Bool
forall (ps :: PredicateStatus) k (p :: k) a.
WithRefine ps p a -> Int
forall (ps :: PredicateStatus) k (p :: k) a.
WithRefine ps p a -> [a]
forall (ps :: PredicateStatus) k (p :: k) a.
(a -> a -> a) -> WithRefine ps p a -> a
forall (ps :: PredicateStatus) k (p :: k) m a.
Monoid m =>
(a -> m) -> WithRefine ps p a -> m
forall (ps :: PredicateStatus) k (p :: k) b a.
(b -> a -> b) -> b -> WithRefine ps p a -> b
forall (ps :: PredicateStatus) k (p :: k) a b.
(a -> b -> b) -> b -> WithRefine ps p a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => WithRefine ps p a -> a
$cproduct :: forall (ps :: PredicateStatus) k (p :: k) a.
Num a =>
WithRefine ps p a -> a
sum :: forall a. Num a => WithRefine ps p a -> a
$csum :: forall (ps :: PredicateStatus) k (p :: k) a.
Num a =>
WithRefine ps p a -> a
minimum :: forall a. Ord a => WithRefine ps p a -> a
$cminimum :: forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> a
maximum :: forall a. Ord a => WithRefine ps p a -> a
$cmaximum :: forall (ps :: PredicateStatus) k (p :: k) a.
Ord a =>
WithRefine ps p a -> a
elem :: forall a. Eq a => a -> WithRefine ps p a -> Bool
$celem :: forall (ps :: PredicateStatus) k (p :: k) a.
Eq a =>
a -> WithRefine ps p a -> Bool
length :: forall a. WithRefine ps p a -> Int
$clength :: forall (ps :: PredicateStatus) k (p :: k) a.
WithRefine ps p a -> Int
null :: forall a. WithRefine ps p a -> Bool
$cnull :: forall (ps :: PredicateStatus) k (p :: k) a.
WithRefine ps p a -> Bool
toList :: forall a. WithRefine ps p a -> [a]
$ctoList :: forall (ps :: PredicateStatus) k (p :: k) a.
WithRefine ps p a -> [a]
foldl1 :: forall a. (a -> a -> a) -> WithRefine ps p a -> a
$cfoldl1 :: forall (ps :: PredicateStatus) k (p :: k) a.
(a -> a -> a) -> WithRefine ps p a -> a
foldr1 :: forall a. (a -> a -> a) -> WithRefine ps p a -> a
$cfoldr1 :: forall (ps :: PredicateStatus) k (p :: k) a.
(a -> a -> a) -> WithRefine ps p a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> WithRefine ps p a -> b
$cfoldl' :: forall (ps :: PredicateStatus) k (p :: k) b a.
(b -> a -> b) -> b -> WithRefine ps p a -> b
foldl :: forall b a. (b -> a -> b) -> b -> WithRefine ps p a -> b
$cfoldl :: forall (ps :: PredicateStatus) k (p :: k) b a.
(b -> a -> b) -> b -> WithRefine ps p a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> WithRefine ps p a -> b
$cfoldr' :: forall (ps :: PredicateStatus) k (p :: k) a b.
(a -> b -> b) -> b -> WithRefine ps p a -> b
foldr :: forall a b. (a -> b -> b) -> b -> WithRefine ps p a -> b
$cfoldr :: forall (ps :: PredicateStatus) k (p :: k) a b.
(a -> b -> b) -> b -> WithRefine ps p a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> WithRefine ps p a -> m
$cfoldMap' :: forall (ps :: PredicateStatus) k (p :: k) m a.
Monoid m =>
(a -> m) -> WithRefine ps p a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> WithRefine ps p a -> m
$cfoldMap :: forall (ps :: PredicateStatus) k (p :: k) m a.
Monoid m =>
(a -> m) -> WithRefine ps p a -> m
fold :: forall m. Monoid m => WithRefine ps p m -> m
$cfold :: forall (ps :: PredicateStatus) k (p :: k) m.
Monoid m =>
WithRefine ps p m -> m
Foldable)
deriving stock instance Functor (WithRefine 'Unenforced p)
deriving stock instance Traversable (WithRefine 'Unenforced p)
instance ToJSON a => ToJSON (WithRefine ps p a) where
toJSON :: WithRefine ps p a -> Value
toJSON = a -> Value
forall a. ToJSON a => a -> Value
toJSON (a -> Value)
-> (WithRefine ps p a -> a) -> WithRefine ps p a -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithRefine ps p a -> a
forall {k} (ps :: PredicateStatus) (p :: k) a.
WithRefine ps p a -> a
withoutRefine
toEncoding :: WithRefine ps p a -> Encoding
toEncoding = a -> Encoding
forall a. ToJSON a => a -> Encoding
toEncoding (a -> Encoding)
-> (WithRefine ps p a -> a) -> WithRefine ps p a -> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithRefine ps p a -> a
forall {k} (ps :: PredicateStatus) (p :: k) a.
WithRefine ps p a -> a
withoutRefine
instance FromJSON a => FromJSON (WithRefine 'Unenforced p a) where
parseJSON :: Value -> Parser (WithRefine 'Unenforced p a)
parseJSON = (a -> WithRefine 'Unenforced p a)
-> Parser a -> Parser (WithRefine 'Unenforced p a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> WithRefine 'Unenforced p a
forall {k} (p :: k) a. a -> WithRefine 'Unenforced p a
withRefine (Parser a -> Parser (WithRefine 'Unenforced p a))
-> (Value -> Parser a)
-> Value
-> Parser (WithRefine 'Unenforced p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser a
forall a. FromJSON a => Value -> Parser a
parseJSON
instance (FromJSON a, Predicate p a) => FromJSON (WithRefine 'Enforced p a) where
parseJSON :: Value -> Parser (WithRefine 'Enforced p a)
parseJSON Value
a = Value -> Parser (WithRefine 'Unenforced p a)
forall a. FromJSON a => Value -> Parser a
parseJSON Value
a Parser (WithRefine 'Unenforced p a)
-> (WithRefine 'Unenforced p a
-> Parser (WithRefine 'Enforced p a))
-> Parser (WithRefine 'Enforced p a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= WithRefine 'Unenforced p a -> Parser (WithRefine 'Enforced p a)
forall p (m :: * -> *) a.
(Predicate p a, MonadFail m) =>
WithRefine 'Unenforced p a -> m (WithRefine 'Enforced p a)
enforceFail
type role WithRefine nominal nominal nominal
withRefine :: forall p a. a -> WithRefine 'Unenforced p a
withRefine :: forall {k} (p :: k) a. a -> WithRefine 'Unenforced p a
withRefine = a -> WithRefine 'Unenforced p a
forall {k} (ps :: PredicateStatus) (p :: k) a.
a -> WithRefine ps p a
WithRefine
data PredicateStatus
= Enforced
| Unenforced
type Strong p a = WithRefine 'Enforced p a
type Weak p a = WithRefine 'Unenforced p a
enforce
:: forall p a. Predicate p a
=> WithRefine 'Unenforced p a
-> Either RefineException (WithRefine 'Enforced p a)
enforce :: forall p a.
Predicate p a =>
WithRefine 'Unenforced p a
-> Either RefineException (WithRefine 'Enforced p a)
enforce WithRefine 'Unenforced p a
wrua =
Either RefineException (WithRefine 'Enforced p a)
-> (RefineException
-> Either RefineException (WithRefine 'Enforced p a))
-> Maybe RefineException
-> Either RefineException (WithRefine 'Enforced p a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (WithRefine 'Enforced p a
-> Either RefineException (WithRefine 'Enforced p a)
forall a b. b -> Either a b
Right (a -> WithRefine 'Enforced p a
forall {k} (ps :: PredicateStatus) (p :: k) a.
a -> WithRefine ps p a
WithRefine a
a)) RefineException
-> Either RefineException (WithRefine 'Enforced p a)
forall a b. a -> Either a b
Left (Proxy p -> a -> Maybe RefineException
forall p x. Predicate p x => Proxy p -> x -> Maybe RefineException
validate (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @p) a
a)
where a :: a
a = WithRefine 'Unenforced p a -> a
forall {k} (ps :: PredicateStatus) (p :: k) a.
WithRefine ps p a -> a
withoutRefine WithRefine 'Unenforced p a
wrua
enforceFail
:: forall p m a. (Predicate p a, MonadFail m)
=> WithRefine 'Unenforced p a
-> m (WithRefine 'Enforced p a)
enforceFail :: forall p (m :: * -> *) a.
(Predicate p a, MonadFail m) =>
WithRefine 'Unenforced p a -> m (WithRefine 'Enforced p a)
enforceFail WithRefine 'Unenforced p a
wrua = case WithRefine 'Unenforced p a
-> Either RefineException (WithRefine 'Enforced p a)
forall p a.
Predicate p a =>
WithRefine 'Unenforced p a
-> Either RefineException (WithRefine 'Enforced p a)
enforce WithRefine 'Unenforced p a
wrua of
Left RefineException
e -> String -> m (WithRefine 'Enforced p a)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m (WithRefine 'Enforced p a))
-> String -> m (WithRefine 'Enforced p a)
forall a b. (a -> b) -> a -> b
$ RefineException -> String
forall e. Exception e => e -> String
displayException RefineException
e
Right WithRefine 'Enforced p a
wrea -> WithRefine 'Enforced p a -> m (WithRefine 'Enforced p a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure WithRefine 'Enforced p a
wrea
unenforce :: forall p a. WithRefine 'Enforced p a -> WithRefine 'Unenforced p a
unenforce :: forall {k} (p :: k) a.
WithRefine 'Enforced p a -> WithRefine 'Unenforced p a
unenforce = a -> WithRefine 'Unenforced p a
forall {k} (p :: k) a. a -> WithRefine 'Unenforced p a
withRefine (a -> WithRefine 'Unenforced p a)
-> (WithRefine 'Enforced p a -> a)
-> WithRefine 'Enforced p a
-> WithRefine 'Unenforced p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithRefine 'Enforced p a -> a
forall {k} (ps :: PredicateStatus) (p :: k) a.
WithRefine ps p a -> a
withoutRefine
enforcedToRefined :: forall p a. WithRefine 'Enforced p a -> Refined p a
enforcedToRefined :: forall p a. WithRefine 'Enforced p a -> Refined p a
enforcedToRefined = a -> Refined p a
forall x p. x -> Refined p x
reallyUnsafeRefine (a -> Refined p a)
-> (WithRefine 'Enforced p a -> a)
-> WithRefine 'Enforced p a
-> Refined p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithRefine 'Enforced p a -> a
forall {k} (ps :: PredicateStatus) (p :: k) a.
WithRefine ps p a -> a
withoutRefine
refinedToEnforced :: forall p a. Refined p a -> WithRefine 'Enforced p a
refinedToEnforced :: forall p a. Refined p a -> WithRefine 'Enforced p a
refinedToEnforced = a -> WithRefine 'Enforced p a
forall {k} (p :: k) a. a -> WithRefine 'Enforced p a
reallyUnsafeEnforce (a -> WithRefine 'Enforced p a)
-> (Refined p a -> a) -> Refined p a -> WithRefine 'Enforced p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined p a -> a
forall p x. Refined p x -> x
unrefine
reallyUnsafeEnforce :: forall p a. a -> WithRefine 'Enforced p a
reallyUnsafeEnforce :: forall {k} (p :: k) a. a -> WithRefine 'Enforced p a
reallyUnsafeEnforce = a -> WithRefine 'Enforced p a
forall {k} (ps :: PredicateStatus) (p :: k) a.
a -> WithRefine ps p a
WithRefine
unsafeWithRefine :: forall ps p a. a -> WithRefine ps p a
unsafeWithRefine :: forall {k} (ps :: PredicateStatus) (p :: k) a.
a -> WithRefine ps p a
unsafeWithRefine = a -> WithRefine ps p a
forall {k} (ps :: PredicateStatus) (p :: k) a.
a -> WithRefine ps p a
WithRefine
type WithRefineRep :: forall p a r. PredicateStatus -> p -> a -> r
type family WithRefineRep ps p a where
WithRefineRep 'Enforced p a = Refined p a
WithRefineRep 'Unenforced _ a = a