{-|
A wrapper on top of "Refined" that encourages using the same type for refined
and unrefined views of the same data. Useful when both views have identical
structure (i.e. the only difference is that whether some invariants are
enforced). For information on refinement types and the underlying concept, see
"Refined".

Definitions generally order typevars predicate first and @a@ last, to support
visible type application (@a@ is usually obvious to the compiler).

Say you're already sold on refinement types as a method to easily describe data
more precisely without complicating algorithms or comprising runtime
performance. You work with plain types internally, and refine only when you need
to. This means when working with records with refined types, you necessarily
duplicate the record: one for refined, one for unrefined.

Sometimes this is fine, because you change the data structure between refining
(e.g. you drop some indices that are generatable). Sometimes, it means you have
two records storing the same data, where one has some invariants enforced and
the other doesn't. In the former case, you should have one data type with
'Refined' fields, one without. This module focuses on the latter use case.

The 'WithRefine' newtype enables you to use the same type for both views by
wrapping refined types with a type-level switch that tracks whether the
predicate is currently enforced.

  * The type @t'WithRefine' ''Enforced' p a@ corresponds to @'Refined' p a@: a
    value of type @a@ with an enforced predicate @p@. Also available at
    @'Strong' p a@.
  * The type @t'WithRefine' ''Unenforced' p a@ corresponds to... @a@. It's a
    value of type @a@ tagged with predicate @p@, but the predicate remains
    unenforced. Also available at @'Weak' p a@.

Now internally, you write your code to only transform @'Weak' p a@ values. When,
say, serializing between an external system, you 'enforce' the predicate,
upgrading to a @'Strong' p a@. The upshot compared to plain refined:

  * No need to duplicate types when working with refined types.
  * Your internal code must be aware of your refined types. This can be good and
    bad: more wrapping, but also more type information.

Runtime impact should be the same as refined, pretty much nothing.
-}

module Refined.WithRefine
  (
  -- * 'WithRefine' types
    WithRefine
  , withRefine, withoutRefine
  , PredicateStatus(..)
  , Strong, Weak

  -- * Enforcing
  , enforce
  , enforceFail

  -- * Unenforcing
  , unenforce

  -- * Coercing between Refined
  , enforcedToRefined
  , refinedToEnforced

  -- * Unsafe enforcing
  , reallyUnsafeEnforce

  -- * Unsafe creation
  , unsafeWithRefine

  -- * Other definitions
  , 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

-- | A wrapper over a type @a@ with a predicate @p@, and a type-level "switch"
--   indicating whether the predicate is enforced or not.
--
-- @t'WithRefine' ''Enforced' p a@ is equivalent to 'Refined p a', while
-- @t'WithRefine' ''Unenforced' p a@ is equivalent to @a@. This newtype lets you
-- use the same term-level constructor for both. One could then combine multiple
-- t'WithRefine'-wrapped fields into a single record and parameterize over the
-- predicate status to essentially enable "weak" and "strong" views of the
-- record, while conveniently using the same value-level representation.
newtype WithRefine (ps :: PredicateStatus) p a
  = WithRefine {
      -- | Strips the predicate from a any wrapped value (enforced or not).
      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

-- | Use the underlying type's instance.
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

-- | Use the unenforced type's instance, and wrap the enforcing error into
--   Aeson's 'MonadFail'.
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

-- TODO I don't really understand this. I naively use the same role annotation
-- as 'Refined'. GHC user's guide page:
-- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/roles.html
type role WithRefine nominal nominal nominal

-- | Wrap a value with any unenforced predicate. This is like tagging your value
--   with the note "this value needs to be checked using the given predicate".
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

-- | Is the associated predicate currently enforced or not?
data PredicateStatus
  = Enforced   -- ^ value is read-only
  | Unenforced -- ^ value is read-write

-- | Synonym for a wrapped type with an enforced predicate.
type Strong p a = WithRefine 'Enforced   p a

-- | Synonym for a wrapped type with an unenforced predicate.
type Weak   p a = WithRefine 'Unenforced p a

-- | Enforce a wrapped value's predicate at runtime.
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

-- | Enforce a wrapped value's predicate at runtime, calling 'fail' if the value
--   does not satisfy the predicate.
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

-- | Stop enforcing a wrapped value's predicate.
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

-- | If you have a @t'WithRefine' ''Enforced'@ value, you can obtain a matching
--   'Refined'.
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

-- | If you have a 'Refined' value, you can obtain a matching @t'WithRefine'
--   ''Enforced'@.
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

-- | Construct an enforced type, completely ignoring any refinements!
--
-- You should only use this if you can prove that the refinement holds. (We need
-- it internally to coerce between 'Refined'.)
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

-- | Wrap a value with any predicate, enforced or unenforced. This is useful for
--   "no-op" refinements, potentially letting you to merge two instances into
--   one, where you explicitly ignore the 'PredicateStatus' (perhaps clearer).
--
-- You should only use this if you can prove that the refinement holds for all
-- values of @a@.
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

-- | Not very useful, but clarifies the meaning of enforced and unenforced
--   refinements.
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