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