Generic implementation of TestEquality

testeq.hs

{-# LANGUAGE KindSignatures, DataKinds, TemplateHaskell, GADTs, TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, QuantifiedConstraints, ConstraintKinds, PolyKinds, TypeApplications, ScopedTypeVariables #-}

import Data.Kind (Type)
import Data.Type.Equality
import Data.Maybe (isJust, isNothing)

import Generics.Kind hiding ((:~:))
import Generics.Kind.TH

-- * Example

data T = A | B

data ST (k :: T) where
  SA :: ST 'A
  SB :: ST 'B

$(deriveGenericK ''ST)

instance TestEquality ST where
  testEquality = gTestEquality
-- Works!

-- Test. Should exit successfully.
main :: IO ()
main = do
  assert (isJust (SA `testEquality` SA))
  assert (isJust (SB `testEquality` SB))
  assert (isNothing (SA `testEquality` SB))
  assert (isNothing (SB `testEquality` SA))

assert :: Bool -> IO ()
assert False = error "assertion failed"
assert True = pure ()

-- * Implementation

gTestEquality :: forall f a b. (GenericK f, GTE a b (a :&&: LoT0) (b :&&: LoT0) (RepK f) (RepK f)) => f a -> f b -> Maybe (a :~: b)
gTestEquality x y = gTE (fromK @_ @f @(a :&&: LoT0) x) (fromK @_ @f @(b :&&: LoT0) y)

class GTE a b x y (f :: LoT kf -> Type) (g :: LoT kg -> Type) where
  gTE :: f x -> g y -> Maybe (a :~: b)

instance GTE a b x y f g => GTE a b x y (M1 i c f) g where
  gTE (M1 x) = gTE x

instance (GTE a b x y f1 g, GTE a b x y f2 g) => GTE a b x y (f1 :+: f2) g where
  gTE (L1 x) = gTE x
  gTE (R1 x) = gTE x

instance (Interpret c x => GTE a b x y f g) => GTE a b x y (c :=>: f) g where
  gTE (SuchThat x) = gTE x

instance (forall z. GTE a b (z :&&: x) y f g) => GTE a b x y (Exists k f) g where
  gTE (Exists x) = gTE x

instance {-# OVERLAPPABLE #-} GTE a b y x g U1 => GTE a b x y U1 g where
  gTE = flip gTE

instance ProspectEq (a == b) a b => GTE a b x y U1 U1 where
  gTE _ _ = prospectEq

class (t ~ (a == b)) => ProspectEq t a b where
  prospectEq :: Maybe (a :~: b)

instance ('True ~ (a == b), a ~ b) => ProspectEq 'True a b where
  prospectEq = Just Refl

instance ('False ~ (a == b)) => ProspectEq 'False a b where
  prospectEq = Nothing

-- * Extra (WIP)

instance {-# OVERLAPPABLE #-} GTE a b y x g (Field t) => GTE a b x y (Field t) g where
  gTE = flip gTE

instance {-# OVERLAPPABLE #-} GTE a b y x g (f1 :*: f2) => GTE a b x y (f1 :*: f2) g where
  gTE = flip gTE

instance ProspectEq (a == b) a b => GTE a b x y (Field tf) (Field tg) where
  gTE _ _ = prospectEq