{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
#if __GLASGOW_HASKELL__ >= 706
{-# LANGUAGE PolyKinds #-}
#endif
{-# LANGUAGE TypeFamilies #-}
#if __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE EmptyCase #-}
#endif
module Data.Functor.Contravariant.Generic
( Deciding(..)
, Deciding1(..)
) where
import Data.Functor.Contravariant
import Data.Functor.Contravariant.Divisible
import GHC.Generics
class (Generic a, GDeciding q (Rep' a)) => Deciding q a where
#ifndef HLINT
deciding :: Decidable f => p q -> (forall b. q b => f b) -> f a
#endif
instance (Generic a, GG (Rep a), GDeciding q (Rep' a)) => Deciding q a where
deciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *).
Decidable f =>
p q -> (forall b. q b => f b) -> f a
deciding p q
p forall b. q b => f b
q = (a -> Swizzle (Rep a) Any) -> f (Swizzle (Rep a) Any) -> f a
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (Rep a Any -> Swizzle (Rep a) Any
forall p. Rep a p -> Swizzle (Rep a) p
forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle (Rep a Any -> Swizzle (Rep a) Any)
-> (a -> Rep a Any) -> a -> Swizzle (Rep a) Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from) (f (Swizzle (Rep a) Any) -> f a) -> f (Swizzle (Rep a) Any) -> f a
forall a b. (a -> b) -> a -> b
$ p q -> (forall b. q b => f b) -> f (Swizzle (Rep a) Any)
forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f (Swizzle (Rep a) a)
gdeciding p q
p f b
forall b. q b => f b
q
type Rep' a = Swizzle (Rep a)
type Rep1' f = Swizzle (Rep1 f)
type family Swizzle (r :: * -> *) :: * -> *
type instance Swizzle (M1 i c f) = M1 i c (Swizzle f)
type instance Swizzle V1 = V1
type instance Swizzle U1 = U1
type instance Swizzle Par1 = Par1
type instance Swizzle (Rec1 f) = Rec1 f
type instance Swizzle (K1 i c) = K1 i c
type instance Swizzle (f :+: g) = Swizzle f ::+: Swizzle g
type instance Swizzle (f :*: g) = Swizzle f ::*: Swizzle g
type instance Swizzle (f :.: g) = f :.: Swizzle g
newtype (::+:) f g a = Sum {forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(::+:) f g a -> Either (f a) (g a)
unSum :: Either (f a) (g a)}
newtype (::*:) f g a = Prod {forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(::*:) f g a -> (f a, g a)
unProd :: (f a, g a)}
class GG r where
swizzle :: r p -> Swizzle r p
instance GG f => GG (M1 i c f) where
swizzle :: forall p. M1 i c f p -> Swizzle (M1 i c f) p
swizzle (M1 f p
a) = Swizzle f p -> M1 i c (Swizzle f) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f p -> Swizzle f p
forall p. f p -> Swizzle f p
forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle f p
a)
instance GG V1 where swizzle :: forall p. V1 p -> Swizzle V1 p
swizzle V1 p
v = V1 p
Swizzle V1 p
v
instance GG U1 where swizzle :: forall p. U1 p -> Swizzle U1 p
swizzle U1 p
v = U1 p
Swizzle U1 p
v
instance GG (K1 i c) where swizzle :: forall p. K1 i c p -> Swizzle (K1 i c) p
swizzle K1 i c p
v = K1 i c p
Swizzle (K1 i c) p
v
instance GG Par1 where swizzle :: forall p. Par1 p -> Swizzle Par1 p
swizzle Par1 p
v = Par1 p
Swizzle Par1 p
v
instance GG (Rec1 f) where swizzle :: forall p. Rec1 f p -> Swizzle (Rec1 f) p
swizzle Rec1 f p
v = Rec1 f p
Swizzle (Rec1 f) p
v
instance (GG f, GG g) => GG (f :+: g) where
{-# INLINE swizzle #-}
swizzle :: forall p. (:+:) f g p -> Swizzle (f :+: g) p
swizzle (L1 f p
x) = Either (Swizzle f p) (Swizzle g p)
-> (::+:) (Swizzle f) (Swizzle g) p
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
Either (f a) (g a) -> (::+:) f g a
Sum (Swizzle f p -> Either (Swizzle f p) (Swizzle g p)
forall a b. a -> Either a b
Left (f p -> Swizzle f p
forall p. f p -> Swizzle f p
forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle f p
x))
swizzle (R1 g p
x) = Either (Swizzle f p) (Swizzle g p)
-> (::+:) (Swizzle f) (Swizzle g) p
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
Either (f a) (g a) -> (::+:) f g a
Sum (Swizzle g p -> Either (Swizzle f p) (Swizzle g p)
forall a b. b -> Either a b
Right (g p -> Swizzle g p
forall p. g p -> Swizzle g p
forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle g p
x))
instance (GG f, GG g) => GG (f :*: g) where
{-# INLINE swizzle #-}
swizzle :: forall p. (:*:) f g p -> Swizzle (f :*: g) p
swizzle (f p
x :*: g p
y) = (Swizzle f p, Swizzle g p) -> (::*:) (Swizzle f) (Swizzle g) p
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(f a, g a) -> (::*:) f g a
Prod (f p -> Swizzle f p
forall p. f p -> Swizzle f p
forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle f p
x, g p -> Swizzle g p
forall p. g p -> Swizzle g p
forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle g p
y)
class (Generic1 t, GDeciding1 q (Rep1' t)) => Deciding1 q t where
#ifndef HLINT
deciding1 :: Decidable f => p q -> (forall b. q b => f b) -> f a -> f (t a)
#endif
instance (Generic1 t, GDeciding1 q (Rep1' t), GG (Rep1 t)) => Deciding1 q t where
deciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
deciding1 p q
p forall b. q b => f b
q f a
r = (t a -> Swizzle (Rep1 t) a) -> f (Swizzle (Rep1 t) a) -> f (t a)
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (Rep1 t a -> Swizzle (Rep1 t) a
forall p. Rep1 t p -> Swizzle (Rep1 t) p
forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle (Rep1 t a -> Swizzle (Rep1 t) a)
-> (t a -> Rep1 t a) -> t a -> Swizzle (Rep1 t) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Rep1 t a
forall a. t a -> Rep1 t a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1) (f (Swizzle (Rep1 t) a) -> f (t a))
-> f (Swizzle (Rep1 t) a) -> f (t a)
forall a b. (a -> b) -> a -> b
$ p q -> (forall b. q b => f b) -> f a -> f (Swizzle (Rep1 t) a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (Swizzle (Rep1 t) a)
forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p f b
forall b. q b => f b
q f a
r
class GDeciding q t where
#ifndef HLINT
gdeciding :: Decidable f => p q -> (forall b. q b => f b) -> f (t a)
#endif
instance GDeciding q U1 where
gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (U1 a)
gdeciding p q
_ forall b. q b => f b
_ = f (U1 a)
forall a. f a
forall (f :: * -> *) a. Divisible f => f a
conquer
instance GDeciding q V1 where
gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (V1 a)
gdeciding p q
_ forall b. q b => f b
_ = f (V1 a)
forall {k} (f :: * -> *) (a :: k). Decidable f => f (V1 a)
glose
instance (GDeciding q f, GDeciding q g) => GDeciding q (f ::*: g) where
gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f ((::*:) f g a)
gdeciding p q
p forall b. q b => f b
q = f (f a) -> f (g a) -> f ((::*:) f g a)
forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Divisible f =>
f (g a) -> f (h a) -> f ((::*:) g h a)
gdivide (p q -> (forall b. q b => f b) -> f (f a)
forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (f a)
gdeciding p q
p f b
forall b. q b => f b
q) (p q -> (forall b. q b => f b) -> f (g a)
forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (g a)
gdeciding p q
p f b
forall b. q b => f b
q)
instance (GDeciding q f, GDeciding q g) => GDeciding q (f ::+: g) where
gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f ((::+:) f g a)
gdeciding p q
p forall b. q b => f b
q = f (f a) -> f (g a) -> f ((::+:) f g a)
forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Decidable f =>
f (g a) -> f (h a) -> f ((::+:) g h a)
gchoose (p q -> (forall b. q b => f b) -> f (f a)
forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (f a)
gdeciding p q
p f b
forall b. q b => f b
q) (p q -> (forall b. q b => f b) -> f (g a)
forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (g a)
gdeciding p q
p f b
forall b. q b => f b
q)
#ifndef HLINT
instance q p => GDeciding q (K1 i p) where
#endif
gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (K1 i p a)
gdeciding p q
_ forall b. q b => f b
q = (K1 i p a -> p) -> f p -> f (K1 i p a)
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap K1 i p a -> p
forall k i c (p :: k). K1 i c p -> c
unK1 f p
forall b. q b => f b
q
instance GDeciding q f => GDeciding q (M1 i c f) where
gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (M1 i c f a)
gdeciding p q
p forall b. q b => f b
q = (M1 i c f a -> f a) -> f (f a) -> f (M1 i c f a)
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 (p q -> (forall b. q b => f b) -> f (f a)
forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (f a)
gdeciding p q
p f b
forall b. q b => f b
q)
class GDeciding1 q t where
#ifndef HLINT
gdeciding1 :: Decidable f => p q -> (forall b. q b => f b) -> f a -> f (t a)
#endif
instance GDeciding1 q U1 where
gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (U1 a)
gdeciding1 p q
_ forall b. q b => f b
_ f a
_ = f (U1 a)
forall a. f a
forall (f :: * -> *) a. Divisible f => f a
conquer
instance GDeciding1 q V1 where
gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (V1 a)
gdeciding1 p q
_ forall b. q b => f b
_ f a
_ = f (V1 a)
forall {k} (f :: * -> *) (a :: k). Decidable f => f (V1 a)
glose
instance (GDeciding1 q f, GDeciding1 q g) => GDeciding1 q (f ::*: g) where
gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f ((::*:) f g a)
gdeciding1 p q
p forall b. q b => f b
q f a
r = f (f a) -> f (g a) -> f ((::*:) f g a)
forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Divisible f =>
f (g a) -> f (h a) -> f ((::*:) g h a)
gdivide (p q -> (forall b. q b => f b) -> f a -> f (f a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (f a)
forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p f b
forall b. q b => f b
q f a
r) (p q -> (forall b. q b => f b) -> f a -> f (g a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (g a)
forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p f b
forall b. q b => f b
q f a
r)
instance (GDeciding1 q f, GDeciding1 q g) => GDeciding1 q (f ::+: g) where
gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f ((::+:) f g a)
gdeciding1 p q
p forall b. q b => f b
q f a
r = f (f a) -> f (g a) -> f ((::+:) f g a)
forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Decidable f =>
f (g a) -> f (h a) -> f ((::+:) g h a)
gchoose (p q -> (forall b. q b => f b) -> f a -> f (f a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (f a)
forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p f b
forall b. q b => f b
q f a
r) (p q -> (forall b. q b => f b) -> f a -> f (g a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (g a)
forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p f b
forall b. q b => f b
q f a
r)
absurd1 :: V1 a -> b
#if defined(HLINT) || (__GLASGOW_HASKELL__ < 708)
absurd1 x = x `seq` error "impossible"
#else
absurd1 :: forall {k} (a :: k) b. V1 a -> b
absurd1 V1 a
x = case V1 a
x of
#endif
glose :: Decidable f => f (V1 a)
glose :: forall {k} (f :: * -> *) (a :: k). Decidable f => f (V1 a)
glose = (V1 a -> Void) -> f (V1 a)
forall a. (a -> Void) -> f a
forall (f :: * -> *) a. Decidable f => (a -> Void) -> f a
lose V1 a -> Void
forall {k} (a :: k) b. V1 a -> b
absurd1
{-# INLINE glose #-}
gdivide :: Divisible f => f (g a) -> f (h a) -> f ((g::*:h) a)
gdivide :: forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Divisible f =>
f (g a) -> f (h a) -> f ((::*:) g h a)
gdivide = ((::*:) g h a -> (g a, h a))
-> f (g a) -> f (h a) -> f ((::*:) g h a)
forall a b c. (a -> (b, c)) -> f b -> f c -> f a
forall (f :: * -> *) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide (::*:) g h a -> (g a, h a)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(::*:) f g a -> (f a, g a)
unProd
{-# INLINE gdivide #-}
gchoose :: Decidable f => f (g a) -> f (h a) -> f ((g::+:h) a)
gchoose :: forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Decidable f =>
f (g a) -> f (h a) -> f ((::+:) g h a)
gchoose = ((::+:) g h a -> Either (g a) (h a))
-> f (g a) -> f (h a) -> f ((::+:) g h a)
forall a b c. (a -> Either b c) -> f b -> f c -> f a
forall (f :: * -> *) a b c.
Decidable f =>
(a -> Either b c) -> f b -> f c -> f a
choose (::+:) g h a -> Either (g a) (h a)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(::+:) f g a -> Either (f a) (g a)
unSum
{-# INLINE gchoose #-}
#ifndef HLINT
instance q p => GDeciding1 q (K1 i p) where
gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (K1 i p a)
gdeciding1 p q
_ forall b. q b => f b
q f a
_ = (K1 i p a -> p) -> f p -> f (K1 i p a)
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap K1 i p a -> p
forall k i c (p :: k). K1 i c p -> c
unK1 f p
forall b. q b => f b
q
#endif
instance GDeciding1 q f => GDeciding1 q (M1 i c f) where
gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (M1 i c f a)
gdeciding1 p q
p forall b. q b => f b
q f a
r = (M1 i c f a -> f a) -> f (f a) -> f (M1 i c f a)
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 (p q -> (forall b. q b => f b) -> f a -> f (f a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (f a)
forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p f b
forall b. q b => f b
q f a
r)
instance GDeciding1 q Par1 where
gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (Par1 a)
gdeciding1 p q
_ forall b. q b => f b
_ f a
r = (Par1 a -> a) -> f a -> f (Par1 a)
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap Par1 a -> a
forall p. Par1 p -> p
unPar1 f a
r
instance Deciding1 q f => GDeciding1 q (Rec1 f) where
gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (Rec1 f a)
gdeciding1 p q
p forall b. q b => f b
q f a
r = (Rec1 f a -> f a) -> f (f a) -> f (Rec1 f a)
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap Rec1 f a -> f a
forall k (f :: k -> *) (p :: k). Rec1 f p -> f p
unRec1 (p q -> (forall b. q b => f b) -> f a -> f (f a)
forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (f a)
forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
(p :: (* -> Constraint) -> *) a.
(Deciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
deciding1 p q
p f b
forall b. q b => f b
q f a
r)