module Generics.SOP.Eq (geq) where
import Data.Function
import Generics.SOP
geq :: (Generic a, All2 Eq (Code a)) => a -> a -> Bool
geq :: forall a. (Generic a, All2 Eq (Code a)) => a -> a -> Bool
geq = forall (xss :: [[*]]).
(All2 Eq xss, All SListI xss) =>
SOP I xss -> SOP I xss -> Bool
go forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. Generic a => a -> Rep a
from
where
go :: forall xss. (All2 Eq xss, All SListI xss) => SOP I xss -> SOP I xss -> Bool
go :: forall (xss :: [[*]]).
(All2 Eq xss, All SListI xss) =>
SOP I xss -> SOP I xss -> Bool
go (SOP (Z NP I x
xs)) (SOP (Z NP I x
ys)) = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse forall a b. (a -> b) -> a -> b
$ forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
(xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
(f' :: k -> *) (f'' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
hcliftA2 Proxy Eq
p forall a. Eq a => I a -> I a -> K Bool a
eq NP I x
xs NP I x
ys
go (SOP (S NS (NP I) xs
xss)) (SOP (S NS (NP I) xs
yss)) = forall (xss :: [[*]]).
(All2 Eq xss, All SListI xss) =>
SOP I xss -> SOP I xss -> Bool
go (forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP NS (NP I) xs
xss) (forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP NS (NP I) xs
yss)
go SOP I xss
_ SOP I xss
_ = Bool
False
p :: Proxy Eq
p :: Proxy Eq
p = forall {k} (t :: k). Proxy t
Proxy
eq :: forall (a :: *). Eq a => I a -> I a -> K Bool a
eq :: forall a. Eq a => I a -> I a -> K Bool a
eq (I a
a) (I a
b) = forall k a (b :: k). a -> K a b
K (a
a forall a. Eq a => a -> a -> Bool
== a
b)