<div dir="ltr"><div><div>Hi Tom,<br><br></div><div>It looks like after a type variable is hidden (existentially quantified is probably the term), you don't get it back to pick the more specific instance. Here's a shorter example than yours:<br><br>{-# LANGUAGE FlexibleInstances, GADTs #-}<br><br>class C a where c :: a -> String<br><br>instance {-# OVERLAPPABLE #-} C a where c _ = "fallback"<br>instance {-# OVERLAPS #-} C Char where c _ = "char"<br><br>data T where T :: a -> T<br><br>example = case T 'x' of T x -> c x<br></div><div>-- prints "fallback"<br></div><div><br></div><div>In this example you can change the T constructor to  T :: C a => a -> T to get "char" printed, but I can't figure the equivalent of that for your class. The closest I can get is to store the Typeable dictionary with the Compose constructor <<a href="http://lpaste.net/9086245683987480576">http://lpaste.net/9086245683987480576</a>> which would let you return "yes" when the wrong instance is chosen. But then if you have Typeable you probably don't need overlapping instances.<br><br></div><div>Regards,<br></div><div>Adam<br></div></div><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 9, 2016 at 12:21 PM, Tom Murphy <span dir="ltr"><<a href="mailto:amindfv@gmail.com" target="_blank">amindfv@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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" target="_blank">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>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>