So I've written a library I'm pretty excited about, and there's just one type issue keeping it from all working! I've got a graph that represents functions and function composition, and I've written a class (pretty directly from Oleg's "TypeEq" work [0]) that tells whether two types are equal. The problem is it doesn't always say they're equal. Here's a simplified version that has the same issue: [pragmas [1]] data Fs a c where F :: (a -> c) -> Fs a c Compose :: forall a b c. Fs b c -> Fs a b -> Fs a c -- Type equality: class TEq x0 x1 y0 y1 (b :: Bool) | x0 x1 y0 y1 -> b where isEq :: Fs x0 x1 -> (y0 -> y1) -> String -- The case where the types are equal: instance {-# OVERLAPS #-} TEq x y x y 'True where isEq _ _ = "yes!" -- The case where they're unequal: instance (b ~ 'False) => TEq x0 x1 y0 y1 b where isEq (F _) = "no" isEq (Compose a b) f = "compose("++isEq a f++", "++isEq b f++")" When I try this on example programs, I see weird results:
isEq (F not) not "yes!" -- expected isEq (Compose (F (\_->"")) (F not)) not "compose(no, no)" -- weird!
I would expect the result of the second one to be "compose(no, yes!)". It seems to think that the (F not) in the Compose has a different type than (F not) not in a Compose. Anyone spot my problem? Thanks! Tom [0] http://okmij.org/ftp/Haskell/typeEQ.html [1] {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs, NoMonoLocalBinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE UndecidableInstances #-}