[Haskell-cafe] Type equality with "forall"

[Tom Murphy]

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 #-}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160309/0234f96b/attachment.html>