Thanks for the reply, Adam!

It looks like the problem is the combination of existentials and overlapping instances (which don't behave sensibly together).

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:

[pragmas [0]]

import Data.Proxy

-- Same as before:
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

class TEq x0 x1 y0 y1 where
   isEq :: Fs x0 x1 -> (y0 -> y1) -> String

instance (
     flag ~ IEq (Fs x0 x1) (y0 -> y1)
   , TEq' x0 x1 y0 y1 flag
   ) => TEq x0 x1 y0 y1 where
   isEq = isEq' (Proxy::Proxy flag)

type family IEq a b :: Bool where
   IEq (Fs x0 x1) (xo -> x1) = 'True
   IEq a b = 'False

class TEq' x0 x1 y0 y1 (flag :: Bool) where
   isEq' :: Proxy flag -> (Fs x0 x1) -> (y0 -> y1) -> String

instance TEq' x0 x1 y0 y1 'True where
   isEq' _ _ _ = "yes!"

instance TEq' x0 x1 y0 y1 'False where
   isEq' _ (F _) _ = "no"
   -- isEq' _ (Compose a b) f = "compose("++isEq a f++", "++isEq b f++")"

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'

Any more help would be very appreciated!

Thanks,

Tom

[0]

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs, NoMonoLocalBinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-} -- new
{-# LANGUAGE TypeFamilies #-} -- new
{-# LANGUAGE UndecidableInstances #-}

On Wed, Mar 9, 2016 at 1:51 PM, adam vogt <vogt.adam@gmail.com> wrote:

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