{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances #-}

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