[Haskell-cafe] Re: topEq for types

[oleg at pobox.com]

Nicolas Frisby described the problem and the solution of the type
equality comparison that takes into account the top-most type
constructor only. Thus `Maybe Bool' should be considered equal to
`Maybe Char' because both types have the same top constructor Maybe.

The following complete code shows another solution. The code includes
several tests, test1 through test6, along with the expected answers.

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# OPTIONS -fallow-overlapping-instances #-}

-- type equality for the top-level type constructor
-- That is, decide two types to be equal if the top-most type constructor
-- matches. Thus `Maybe Bool' should be considered equal to `Maybe Char'

module TEQ where

-- Our approach is simple. Given a type, we normalize it:
-- replace all arguments of the type constructor with unit.
-- After that, we use the regular HList's TypeEq.

class Normalize t r | t -> r

instance TypeCast (c ()) r => Normalize (c x) r
instance TypeCast (c () ()) r => Normalize (c x y) r
instance TypeCast (c () () ()) r => Normalize (c x y z) r
-- add instances for type constructors of higher arities
instance TypeCast y x => Normalize x y


top_eq :: (Normalize a a', Normalize b b', TypeEq a' b' r) =>
          a -> b -> r
top_eq = undefined


test1 = top_eq (undefined::Int) (undefined::Char)
-- :t test1
-- test1 :: HFalse
test2 = top_eq (undefined::Bool) (undefined::Bool)
-- test2 :: HTrue
test3 = top_eq (undefined::Maybe Bool) (undefined::Maybe Char)
-- test3 :: HTrue
test4 = top_eq (undefined::Maybe Bool) (undefined::[Char])
-- test4 :: HFalse
test5 = top_eq (undefined::Either Int Char) (undefined::Either Char Int)
-- test5 :: HTrue
test6 = top_eq (undefined::Either Int Char) (undefined::[Char])
-- test6 :: HFalse


-- The following is borrowed from HList and included here for completeness

data HTrue
data HFalse

class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x  = x

class  TypeEq x y b | x y -> b
instance TypeEq x x HTrue
instance TypeCast HFalse b => TypeEq x y b