[Haskell-cafe] Type equality with "forall"
Tom Murphy
amindfv at gmail.com
Wed Mar 9 17:21:06 UTC 2016
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>
More information about the Haskell-Cafe
mailing list