{-# language AllowAmbiguousTypes   #-}
{-# language ConstraintKinds       #-}
{-# 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.Eq where

import           Data.Kind
import           GHC.TypeLits
import           Generics.Kind

geq' :: forall t. (GenericK t, GEq (RepK t), ReqsEq (RepK t) 'LoT0)
     => t -> t -> Bool
geq' :: forall t.
(GenericK @(*) t, GEq @(*) (RepK @(*) t),
 ReqsEq @(*) (RepK @(*) t) 'LoT0) =>
t -> t -> Bool
geq' t
x t
y = RepK @(*) t 'LoT0 -> RepK @(*) t 'LoT0 -> Bool
forall k (f :: LoT k -> *) (tys :: LoT k).
(GEq @k f, ReqsEq @k f tys) =>
f tys -> f tys -> Bool
forall (tys :: LoT (*)).
ReqsEq @(*) (RepK @(*) t) tys =>
RepK @(*) t tys -> RepK @(*) t tys -> Bool
geq (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 GEq (f :: LoT k -> Type) where
  type family ReqsEq f (tys :: LoT k) :: Constraint
  geq :: ReqsEq f tys => f tys -> f tys -> Bool

instance GEq U1 where
  type ReqsEq U1 tys = ()
  geq :: forall (tys :: LoT k).
ReqsEq @k (U1 @(LoT k)) tys =>
U1 @(LoT k) tys -> U1 @(LoT k) tys -> Bool
geq U1 @(LoT k) tys
U1 U1 @(LoT k) tys
U1 = Bool
True

instance GEq f => GEq (M1 i c f) where
  type ReqsEq (M1 i c f) tys = ReqsEq f tys
  geq :: forall (tys :: LoT k).
ReqsEq @k (M1 @(LoT k) i c f) tys =>
M1 @(LoT k) i c f tys -> M1 @(LoT k) i c f tys -> Bool
geq (M1 f tys
x) (M1 f tys
y) = f tys -> f tys -> Bool
forall k (f :: LoT k -> *) (tys :: LoT k).
(GEq @k f, ReqsEq @k f tys) =>
f tys -> f tys -> Bool
forall (tys :: LoT k). ReqsEq @k f tys => f tys -> f tys -> Bool
geq f tys
x f tys
y

instance (GEq f, GEq g) => GEq (f :+: g) where
  type ReqsEq (f :+: g) tys = (ReqsEq f tys, ReqsEq g tys)
  geq :: forall (tys :: LoT k).
ReqsEq @k ((:+:) @(LoT k) f g) tys =>
(:+:) @(LoT k) f g tys -> (:+:) @(LoT k) f g tys -> Bool
geq (L1 f tys
x) (L1 f tys
y) = f tys -> f tys -> Bool
forall k (f :: LoT k -> *) (tys :: LoT k).
(GEq @k f, ReqsEq @k f tys) =>
f tys -> f tys -> Bool
forall (tys :: LoT k). ReqsEq @k f tys => f tys -> f tys -> Bool
geq f tys
x f tys
y
  geq (R1 g tys
x) (R1 g tys
y) = g tys -> g tys -> Bool
forall k (f :: LoT k -> *) (tys :: LoT k).
(GEq @k f, ReqsEq @k f tys) =>
f tys -> f tys -> Bool
forall (tys :: LoT k). ReqsEq @k g tys => g tys -> g tys -> Bool
geq g tys
x g tys
y
  geq (:+:) @(LoT k) f g tys
_      (:+:) @(LoT k) f g tys
_      = Bool
False

instance (GEq f, GEq g) => GEq (f :*: g) where
  type ReqsEq (f :*: g) tys = (ReqsEq f tys, ReqsEq g tys)
  geq :: forall (tys :: LoT k).
ReqsEq @k ((:*:) @(LoT k) f g) tys =>
(:*:) @(LoT k) f g tys -> (:*:) @(LoT k) f g tys -> Bool
geq (f tys
x1 :*: g tys
x2) (f tys
y1 :*: g tys
y2) = f tys -> f tys -> Bool
forall k (f :: LoT k -> *) (tys :: LoT k).
(GEq @k f, ReqsEq @k f tys) =>
f tys -> f tys -> Bool
forall (tys :: LoT k). ReqsEq @k f tys => f tys -> f tys -> Bool
geq f tys
x1 f tys
y1 Bool -> Bool -> Bool
&& g tys -> g tys -> Bool
forall k (f :: LoT k -> *) (tys :: LoT k).
(GEq @k f, ReqsEq @k f tys) =>
f tys -> f tys -> Bool
forall (tys :: LoT k). ReqsEq @k g tys => g tys -> g tys -> Bool
geq g tys
x2 g tys
y2

instance GEq (Field t) where
  type ReqsEq (Field t) tys = Eq (Interpret t tys)
  geq :: forall (tys :: LoT k).
ReqsEq @k (Field @k t) tys =>
Field @k t tys -> Field @k t tys -> Bool
geq (Field Interpret @k @(*) t tys
x) (Field Interpret @k @(*) t tys
y) = Interpret @k @(*) t tys
x Interpret @k @(*) t tys -> Interpret @k @(*) t tys -> Bool
forall a. Eq a => a -> a -> Bool
== Interpret @k @(*) t tys
y

instance GEq f => GEq (c :=>: f) where
  type ReqsEq (c :=>: f) tys = ReqsEq f tys
  -- really we want          = Interpret c tys => GEq f tys
  geq :: forall (tys :: LoT k).
ReqsEq @k ((:=>:) @k c f) tys =>
(:=>:) @k c f tys -> (:=>:) @k c f tys -> Bool
geq (SuchThat f tys
x) (SuchThat f tys
y) = f tys -> f tys -> Bool
forall k (f :: LoT k -> *) (tys :: LoT k).
(GEq @k f, ReqsEq @k f tys) =>
f tys -> f tys -> Bool
forall (tys :: LoT k). ReqsEq @k f tys => f tys -> f tys -> Bool
geq f tys
x f tys
y

instance TypeError ('Text "Existentials are not supported")
         => GEq (Exists k f) where
  type ReqsEq (Exists k f) tys = TypeError ('Text "Existentials are not supported")
  geq :: forall (tys :: LoT k).
ReqsEq @k (Exists @k k f) tys =>
Exists @k k f tys -> Exists @k k f tys -> Bool
geq = Exists @k k f tys -> Exists @k k f tys -> Bool
forall a. HasCallStack => a
undefined