Hi Tom,

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:

{-# LANGUAGE FlexibleInstances, GADTs #-}

class C a where c :: a -> String

instance {-# OVERLAPPABLE #-} C a where c _ = "fallback"
instance {-# OVERLAPS #-} C Char where c _ = "char"

data T where T :: a -> T

example = case T 'x' of T x -> c x

-- prints "fallback"

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 <http://lpaste.net/9086245683987480576> 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.

Regards,

Adam

On Wed, Mar 9, 2016 at 12:21 PM, Tom Murphy <amindfv@gmail.com> wrote:

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 #-}

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe