{- | 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.
-}

module Rerefined.Refine.Unsafe
  (
  -- * @Refined@
    type Refined
  , unsafeRefine
  , unsafeRerefine

  -- * @Refined1@
  , type Refined1
  , unsafeRefine1
  , unsafeRerefine1
  ) where

import Rerefined.Refined
import Rerefined.Refined1

-- | Construct a 'Refined' without validating the predicate @p@.
--
-- Unsafe. Use only when you can manually prove that the predicate holds.
unsafeRefine :: a -> Refined p a
unsafeRefine :: forall {k} a (p :: k). a -> Refined p a
unsafeRefine = a -> Refined p a
forall {k} (p :: k) a. a -> Refined p a
Refined

-- | Replace a 'Refined''s predicate without validating the new prdicate @pNew@.
--
-- Unsafe. Use only when you can manually prove that the new predicate holds.
unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a
unsafeRerefine :: forall {k} {k} (pNew :: k) (pOld :: k) a.
Refined pOld a -> Refined pNew a
unsafeRerefine = a -> Refined pNew a
forall {k} (p :: k) a. a -> Refined p a
Refined (a -> Refined pNew a)
-> (Refined pOld a -> a) -> Refined pOld a -> Refined pNew a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined pOld a -> a
forall {k} (p :: k) a. Refined p a -> a
unrefine

-- | Construct a 'Refined1' without validating the predicate @p@.
--
-- Unsafe. Use only when you can manually prove that the predicate holds.
unsafeRefine1 :: f a -> Refined1 p f a
unsafeRefine1 :: forall {k1} {k} (f :: k1 -> Type) (a :: k1) (p :: k).
f a -> Refined1 p f a
unsafeRefine1 = f a -> Refined1 p f a
forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
f a -> Refined1 p f a
Refined1

-- | Replace a 'Refined1''s predicate without validating the new prdicate
--   @pNew@.
--
-- Unsafe. Use only when you can manually prove that the new predicate holds.
unsafeRerefine1 :: forall pNew pOld f a. Refined1 pOld f a -> Refined1 pNew f a
unsafeRerefine1 :: forall {k} {k} {k1} (pNew :: k) (pOld :: k) (f :: k1 -> Type)
       (a :: k1).
Refined1 pOld f a -> Refined1 pNew f a
unsafeRerefine1 = f a -> Refined1 pNew f a
forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
f a -> Refined1 p f a
Refined1 (f a -> Refined1 pNew f a)
-> (Refined1 pOld f a -> f a)
-> Refined1 pOld f a
-> Refined1 pNew f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined1 pOld f a -> f a
forall {k1} {k2} (p :: k1) (f :: k2 -> Type) (a :: k2).
Refined1 p f a -> f a
unrefine1