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

module Data.TrieMap.MultiRec.Eq where

-- import Data.TrieMap.MultiRec.Base
-- import Generics.MultiRec.HFix
import Generics.MultiRec.Eq
-- import Data.TrieMap.Regular.Eq

-- class HEq phi r where
-- 	heqH :: phi ix -> r ix -> r ix -> Bool

-- class EqFam phi where
-- 	eqF :: phi ix -> (ix -> ix -> Bool)

class HEq0 phi r where
	heq0 :: 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 heq0
{-
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 HEq0 phi r => HEq0 phi (A0 r) where
	heqH pf (A0 x) (A0 y) = heqH pf x y-}

-- instance (HEq phi f, HEq0 phi r) => HEq0 phi (A f r) where
-- 	heqH pf (A x) (A y) = heqT pf 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