[Haskell-cafe] Type equality with "forall"

[adam vogt]

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/ab2b56be/attachment.html>