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