<div dir="ltr"><div><div><div>Thanks for the reply, Adam!<br><br></div>It looks like the problem is the combination of existentials and overlapping instances (which don't behave sensibly together).<br><br></div>Here's a new version (that also doesn't work!) but that I think is a lot closer -- this one uses type families instead of overlapping instances:<br><br></div>[pragmas [0]]<br><br><br>import Data.Proxy<br><br>-- Same as before:<br>data Fs a c where<br> F :: (a -> c) -> Fs a c<br> Compose :: forall a b c. Fs b c -> Fs a b -> Fs a c<br><br><br><br>class TEq x0 x1 y0 y1 where<br> isEq :: Fs x0 x1 -> (y0 -> y1) -> String<br><br>instance (<br> flag ~ IEq (Fs x0 x1) (y0 -> y1)<br> , TEq' x0 x1 y0 y1 flag<br> ) => TEq x0 x1 y0 y1 where<br> isEq = isEq' (Proxy::Proxy flag)<br><br><br><br>type family IEq a b :: Bool where<br> IEq (Fs x0 x1) (xo -> x1) = 'True<br> IEq a b = 'False<br><br><br><br>class TEq' x0 x1 y0 y1 (flag :: Bool) where<br> isEq' :: Proxy flag -> (Fs x0 x1) -> (y0 -> y1) -> String<br><br>instance TEq' x0 x1 y0 y1 'True where<br> isEq' _ _ _ = "yes!"<br><br>instance TEq' x0 x1 y0 y1 'False where<br> isEq' _ (F _) _ = "no"<br> -- isEq' _ (Compose a b) f = "compose("++isEq a f++", "++isEq b f++")"<br><br><div><br></div><div>The problem is the last line -- the "hidden" type can't be inferred to be in TEq', although every type is in fact in TEq'<br></div><div><br></div><div>Any more help would be very appreciated!<br></div><div><br></div><div>Thanks,<br></div><div>Tom<br><br>[0]<br><br><br>{-# LANGUAGE DataKinds #-}<br>{-# LANGUAGE FlexibleInstances #-}<br>{-# LANGUAGE FunctionalDependencies #-}<br>{-# LANGUAGE GADTs, NoMonoLocalBinds #-}<br>{-# LANGUAGE KindSignatures #-}<br>{-# LANGUAGE MultiParamTypeClasses #-}<br>{-# LANGUAGE Rank2Types #-}<br>{-# LANGUAGE ScopedTypeVariables #-} -- new<br>{-# LANGUAGE TypeFamilies #-} -- new<br>{-# LANGUAGE UndecidableInstances #-}<br></div><div><br><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 9, 2016 at 1:51 PM, adam vogt <span dir="ltr"><<a href="mailto:vogt.adam@gmail.com" target="_blank">vogt.adam@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>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" target="_blank">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"><div><div class="h5">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></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><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></div></div>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">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>
</blockquote></div><br></div>