module Data.TrieMap.MultiRec.Eq where
import Generics.MultiRec
import Generics.MultiRec.Eq
class HEq0 phi r where
heqH :: phi ix -> r ix -> r ix -> Bool
heqT :: (HEq phi f, HEq0 phi r) => phi ix -> f r ix -> f r ix -> Bool
heqT = heq heqH
instance Eq k => HEq0 phi (K k r) where
heqH _ (K x) (K y) = x == y
instance (El phi xi, HEq0 phi r) => HEq0 phi (I xi r) where
heqH pf (I x) (I y) = heqH (proofOn pf) x y where
proofOn :: El phi xi => phi ix -> phi xi
proofOn _ = proof
instance HEq0 phi (U r) where
heqH _ _ _ = True
instance (HEq phi f, HEq phi g, HEq0 phi r) => HEq0 phi ((f :*: g) r) where
heqH pf (x1 :*: y1) (x2 :*: y2) = heqT pf x1 x2 && heqT pf y1 y2
instance (HEq phi f, HEq phi g, HEq0 phi r) => HEq0 phi ((f :+: g) r) where
heqH pf (L x) (L y) = heqT pf x y
heqH pf (R x) (R y) = heqT pf x y
heqH _ _ _ = False
instance (HEq phi f, HEq0 phi r) => HEq0 phi ((f :>: ix) r) where
heqH pf (Tag x) (Tag y) = heqT pf x y
instance HEq phi f => HEq0 phi (HFix f) where
heqH pf (HIn x) (HIn y) = heqT pf x y