{-# LANGUAGE ImpredicativeTypes #-}
module Data.Container.Refined.Unsafe where

import Data.Container.Refined.Proofs
import Data.Type.Coercion
import Refined
import Refined.Unsafe


unsafeSubset :: p :-> q
unsafeSubset :: forall p q x. Refined p x -> Refined q x
unsafeSubset = x -> Refined q x
forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine (x -> Refined q x)
-> (Refined p x -> x) -> Refined p x -> Refined q x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined p x -> x
forall {k} (p :: k) x. Refined p x -> x
unrefine
{-# INLINE unsafeSubset #-}

unsafeSubsetWith2 :: p' :-> q' -> p'' :-> q'' -> p :-> q
unsafeSubsetWith2 :: forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 p' :-> q'
f p'' :-> q''
g = x -> Refined q x
forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine (x -> Refined q x)
-> (Refined p x -> x) -> Refined p x -> Refined q x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined q' x -> x
forall {k} (p :: k) x. Refined p x -> x
unrefine
  (Refined q' x -> x)
-> (Refined p x -> Refined q' x) -> Refined p x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined p' x -> Refined q' x
p' :-> q'
f (Refined p' x -> Refined q' x)
-> (Refined p x -> Refined p' x) -> Refined p x -> Refined q' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Refined p' x
forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine (x -> Refined p' x)
-> (Refined p x -> x) -> Refined p x -> Refined p' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined q'' x -> x
forall {k} (p :: k) x. Refined p x -> x
unrefine
  (Refined q'' x -> x)
-> (Refined p x -> Refined q'' x) -> Refined p x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined p'' x -> Refined q'' x
p'' :-> q''
g (Refined p'' x -> Refined q'' x)
-> (Refined p x -> Refined p'' x) -> Refined p x -> Refined q'' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Refined p'' x
forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine (x -> Refined p'' x)
-> (Refined p x -> x) -> Refined p x -> Refined p'' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined p x -> x
forall {k} (p :: k) x. Refined p x -> x
unrefine
{-# INLINE unsafeSubsetWith2 #-}

-- Because `Refined p x` is a newtype over `x`, by parametricity a `p :-> q`
-- can either diverge or be `id`. This ensures that it does not diverge.
rnfProof :: (p :-> q) -> ()
rnfProof :: forall p q. (p :-> q) -> ()
rnfProof p :-> q
f = Refined q () -> ()
forall {k} (p :: k) x. Refined p x -> x
unrefine (Refined q () -> ()) -> Refined q () -> ()
forall a b. (a -> b) -> a -> b
$ Refined p () -> Refined q ()
p :-> q
f (Refined p () -> Refined q ()) -> Refined p () -> Refined q ()
forall a b. (a -> b) -> a -> b
$ () -> Refined p ()
forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine ()
{-# INLINE rnfProof #-}

-- | This function can be used to freely convert between @Element@ and @Key@
-- types of various flavors ('Regular', v'Int', 'Hashed'), corresponding to the
-- different implementations of sets and maps.
castFlavor
  :: forall (f :: Flavor) (g :: Flavor) s a. Coercion
    (Refined (InSet f s) a)
    (Refined (InSet g s) a)
castFlavor :: forall (f :: Flavor) (g :: Flavor) s a.
Coercion (Refined (InSet f s) a) (Refined (InSet g s) a)
castFlavor = Coercion a (Refined (InSet f s) a)
-> Coercion (Refined (InSet f s) a) a
forall {k} (a :: k) (b :: k). Coercion a b -> Coercion b a
sym (forall x p. Coercion x (Refined p x)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @a @(InSet f s))
  Coercion (Refined (InSet f s) a) a
-> Coercion a (Refined (InSet g s) a)
-> Coercion (Refined (InSet f s) a) (Refined (InSet g s) a)
forall {k} (a :: k) (b :: k) (c :: k).
Coercion a b -> Coercion b c -> Coercion a c
`trans` forall x p. Coercion x (Refined p x)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @a @(InSet g s)
{-# INLINE castFlavor #-}

castRefined
  :: forall a p q. (p :-> q)
  -> (q :-> p)
  -> Coercion (Refined p a) (Refined q a)
castRefined :: forall a p q.
(p :-> q) -> (q :-> p) -> Coercion (Refined p a) (Refined q a)
castRefined p :-> q
f q :-> p
g
  | () <- (p :-> q) -> ()
forall p q. (p :-> q) -> ()
rnfProof Refined p x -> Refined q x
p :-> q
f
  , () <- (q :-> p) -> ()
forall p q. (p :-> q) -> ()
rnfProof Refined q x -> Refined p x
q :-> p
g
  = Coercion a (Refined p a) -> Coercion (Refined p a) a
forall {k} (a :: k) (b :: k). Coercion a b -> Coercion b a
sym (forall x p. Coercion x (Refined p x)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @a @p)
    Coercion (Refined p a) a
-> Coercion a (Refined q a) -> Coercion (Refined p a) (Refined q a)
forall {k} (a :: k) (b :: k) (c :: k).
Coercion a b -> Coercion b c -> Coercion a c
`trans` forall x p. Coercion x (Refined p x)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @a @q
{-# INLINE castRefined #-}