[Haskell-cafe] Type equality with "forall"

[Tom Murphy]

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 at 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 at 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160309/bc0cab36/attachment.html>