Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Created May 29, 2021 05:49
Show Gist options
  • Save Lysxia/860f581b2cc56da155d5a92ba5be266d to your computer and use it in GitHub Desktop.
Save Lysxia/860f581b2cc56da155d5a92ba5be266d to your computer and use it in GitHub Desktop.
Generic implementation of TestEquality
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment