{-# 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. p :-> q
unsafeSubset = forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (p :: k) x. Refined p x -> x
unrefine
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. p' :-> q'
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (p :: k) x. Refined p x -> x
unrefine
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. p'' :-> q''
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall {k} (p :: k) x. Refined p x -> x
unrefine forall a b. (a -> b) -> a -> b
$ p :-> q
f forall a b. (a -> b) -> a -> b
$ 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 = forall {k} (a :: k) (b :: k). Coercion a b -> Coercion b a
sym (forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @a @(InSet f s))
  forall {k} (a :: k) (b :: k) (c :: k).
Coercion a b -> Coercion b c -> Coercion a c
`trans` 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
  | () <- forall p q. (p :-> q) -> ()
rnfProof p :-> q
f
  , () <- forall p q. (p :-> q) -> ()
rnfProof q :-> p
g
  = forall {k} (a :: k) (b :: k). Coercion a b -> Coercion b a
sym (forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @a @p)
    forall {k} (a :: k) (b :: k) (c :: k).
Coercion a b -> Coercion b c -> Coercion a c
`trans` forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @a @q
{-# INLINE castRefined #-}