Re: [Haskell-cafe] Type equality with "forall"

9 Mar 2016

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