{-# language AllowAmbiguousTypes   #-}
{-# language DataKinds             #-}
{-# language FlexibleContexts      #-}
{-# language FlexibleInstances     #-}
{-# language MultiParamTypeClasses #-}
{-# language PolyKinds             #-}
{-# language QuantifiedConstraints #-}
{-# language ScopedTypeVariables   #-}
{-# language TypeApplications      #-}
{-# language TypeFamilies          #-}
{-# language TypeOperators         #-}
{-# language UndecidableInstances  #-}
module Generics.Kind.Derive.EqTwoParams where

import           Data.Kind
import           Generics.Kind

geq2' :: forall t. (GenericK t, GEq2 (RepK t) 'LoT0 'LoT0)
      => t -> t -> Bool
geq2' :: forall t.
(GenericK @(*) t, GEq2 @(*) (RepK @(*) t) 'LoT0 'LoT0) =>
t -> t -> Bool
geq2' t
x t
y = RepK @(*) t 'LoT0 -> RepK @(*) t 'LoT0 -> Bool
forall k (f :: LoT k -> *) (xs :: LoT k) (ys :: LoT k).
GEq2 @k f xs ys =>
f xs -> f ys -> Bool
geq2 (forall k (f :: k) (x :: LoT k).
GenericK @k f =>
(:@@:) @k f x -> RepK @k f x
fromK @_ @t @'LoT0 t
(:@@:) @(*) t 'LoT0
x) (forall k (f :: k) (x :: LoT k).
GenericK @k f =>
(:@@:) @k f x -> RepK @k f x
fromK @_ @t @'LoT0 t
(:@@:) @(*) t 'LoT0
y)

class GEq2 (f :: LoT k -> Type) (xs :: LoT k) (ys :: LoT k) where
  geq2 :: f xs -> f ys -> Bool

instance GEq2 U1 xs ys where
  geq2 :: U1 @(LoT k) xs -> U1 @(LoT k) ys -> Bool
geq2 U1 @(LoT k) xs
U1 U1 @(LoT k) ys
U1 = Bool
True

instance (GEq2 f xs ys) => GEq2 (M1 i c f) xs ys where
  geq2 :: M1 @(LoT k) i c f xs -> M1 @(LoT k) i c f ys -> Bool
geq2 (M1 f xs
x) (M1 f ys
y) = f xs -> f ys -> Bool
forall k (f :: LoT k -> *) (xs :: LoT k) (ys :: LoT k).
GEq2 @k f xs ys =>
f xs -> f ys -> Bool
geq2 f xs
x f ys
y

instance (GEq2 f xs ys, GEq2 g xs ys) => GEq2 (f :+: g) xs ys where
  geq2 :: (:+:) @(LoT k) f g xs -> (:+:) @(LoT k) f g ys -> Bool
geq2 (L1 f xs
x) (L1 f ys
y) = f xs -> f ys -> Bool
forall k (f :: LoT k -> *) (xs :: LoT k) (ys :: LoT k).
GEq2 @k f xs ys =>
f xs -> f ys -> Bool
geq2 f xs
x f ys
y
  geq2 (R1 g xs
x) (R1 g ys
y) = g xs -> g ys -> Bool
forall k (f :: LoT k -> *) (xs :: LoT k) (ys :: LoT k).
GEq2 @k f xs ys =>
f xs -> f ys -> Bool
geq2 g xs
x g ys
y
  geq2 (:+:) @(LoT k) f g xs
_      (:+:) @(LoT k) f g ys
_      = Bool
False

instance (GEq2 f xs ys, GEq2 g xs ys) => GEq2 (f :*: g) xs ys where
  geq2 :: (:*:) @(LoT k) f g xs -> (:*:) @(LoT k) f g ys -> Bool
geq2 (f xs
x1 :*: g xs
x2) (f ys
y1 :*: g ys
y2) = f xs -> f ys -> Bool
forall k (f :: LoT k -> *) (xs :: LoT k) (ys :: LoT k).
GEq2 @k f xs ys =>
f xs -> f ys -> Bool
geq2 f xs
x1 f ys
y1 Bool -> Bool -> Bool
&& g xs -> g ys -> Bool
forall k (f :: LoT k -> *) (xs :: LoT k) (ys :: LoT k).
GEq2 @k f xs ys =>
f xs -> f ys -> Bool
geq2 g xs
x2 g ys
y2

instance (Interpret t xs ~ Interpret t ys, Eq (Interpret t xs)) => GEq2 (Field t) xs ys where
  geq2 :: Field @k t xs -> Field @k t ys -> Bool
geq2 (Field Interpret @k @(*) t xs
x) (Field Interpret @k @(*) t ys
y) = Interpret @k @(*) t xs
Interpret @k @(*) t ys
x Interpret @k @(*) t ys -> Interpret @k @(*) t ys -> Bool
forall a. Eq a => a -> a -> Bool
== Interpret @k @(*) t ys
y

instance ((Interpret c xs, Interpret c ys) => GEq2 f xs ys)
         => GEq2 (c :=>: f) xs ys where
  geq2 :: (:=>:) @k c f xs -> (:=>:) @k c f ys -> Bool
geq2 (SuchThat f xs
x) (SuchThat f ys
y) = f xs -> f ys -> Bool
forall k (f :: LoT k -> *) (xs :: LoT k) (ys :: LoT k).
GEq2 @k f xs ys =>
f xs -> f ys -> Bool
geq2 f xs
x f ys
y

instance (forall x y. GEq2 f (x ':&&: xs) (y ':&&: ys))
         => GEq2 (Exists k f) xs ys where
  geq2 :: Exists @k k f xs -> Exists @k k f ys -> Bool
geq2 (Exists f ((':&&:) @k @k t xs)
x) (Exists f ((':&&:) @k @k t ys)
y) = f ((':&&:) @k @k t xs) -> f ((':&&:) @k @k t ys) -> Bool
forall k (f :: LoT k -> *) (xs :: LoT k) (ys :: LoT k).
GEq2 @k f xs ys =>
f xs -> f ys -> Bool
geq2 f ((':&&:) @k @k t xs)
x f ((':&&:) @k @k t ys)
y

{-
instance (forall x y. GEq2 f (x ':&&: xs) (y ':&&: ys))
         => GEq2 (ERefl f) xs ys where
  geq2 (ERefl (x :: f (x :&&: xs))) (ERefl (y :: f (y :&&: ys)))
    = case eqTypeRep (typeRep @x) (typeRep @y) of
        Nothing    -> False
        Just HRefl -> geq2 x y
-}