{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,
UndecidableInstances, IncoherentInstances, GADTs #-}
module Data.Comp.Param.Multi.Equality
(
PEq(..),
EqHD(..)
) where
import Data.Comp.Param.Multi.Term
import Data.Comp.Param.Multi.Sum
import Data.Comp.Param.Multi.Ops
import Data.Comp.Param.Multi.HDifunctor
import Data.Comp.Param.Multi.FreshM
class PEq a where
peq :: a i -> a j -> FreshM Bool
instance Eq a => PEq (K a) where
peq (K x) (K y) = return $ x == y
class EqHD f where
eqHD :: PEq a => f Name a i -> f Name a j -> FreshM Bool
instance (EqHD f, EqHD g) => EqHD (f :+: g) where
eqHD (Inl x) (Inl y) = eqHD x y
eqHD (Inr x) (Inr y) = eqHD x y
eqHD _ _ = return False
instance PEq Name where
peq x y = return $ nameCoerce x == y
instance EqHD f => EqHD (Cxt h f) where
eqHD (In e1) (In e2) = eqHD e1 e2
eqHD (Hole h1) (Hole h2) = peq h1 h2
eqHD (Var p1) (Var p2) = peq p1 p2
eqHD _ _ = return False
instance (EqHD f, PEq a) => PEq (Cxt h f Name a) where
peq = eqHD
instance (HDifunctor f, EqHD f) => Eq (Term f i) where
(==) (Term x) (Term y) = evalFreshM $ eqHD x y