[Haskell-cafe] Scope of type variables in associated types

[Matthew Sackman]

On Mon, May 21, 2007 at 10:36:00AM +0100, Simon Peyton-Jones wrote:
> | The following doesn't seem to work. Is this a limitation of the current
> | implementation or will it never work? Are there any work arounds without
> | introducing extra type params into the data type E?
> |
> | > class G a b | a -> b where
> | >     data E a :: *
> | >     wrap :: b -> E a
> | >     unwrap :: E a -> b
> |
> | > instance G a b where
> | >     data E a = EC b -- this line - the b is not in scope.
> | >     wrap = EC
> | >     unwrap (EC b) = b
> |
> | I get "Not in scope: type variable `b'".
> 
> That's a bug.  b should be in scope

Ahh, cool. I which case I wonder if this too is a bug? :

data Nil = Nil
data Cons :: * -> * -> * where
             Cons :: val -> tail -> Cons val tail

class F c v t | c -> v t where
    data FD c t :: *

instance F (Cons v t) v t where
    -- this blows up with "conflicting definitions for `t'"
    data FD (Cons v t) t = FDC v

> However, your program is very suspicious!  Associated data types
> *replace* functional dependencies, so you should not use both.  Your
> probably want something like

>         class G a where
>           data E a :: *
>           wrap :: a -> E a
>           unwrap :: E a -> a

I'm afraid not. I really need wrap to take a 'b' and unwrap to return a 'b'.
Talking on #haskell to sjanssen last night, he came up with:

class F a b where
    data F a :: *

instance F a b where
    data F a = F b

cast :: (F a b, F a c) => b -> c
cast x = case F x of
            (F y) -> y

as evidence as to why it's unsafe. But with the fundep, I would have
thought it would have been safe. The associated type "way" would be to
drop the b and then have data F a :: * -> *  - just like in the papers.
But I really need the b to be part of the class in order to match the b
against other class constraints in other functions. In particular I need
to be able to write something like:

instance (G a b) => F a b where
...

Somehow I doubt it, but is the following any less suspicious?

class F a b where
    type BThing a :: *
    data FD a :: *
    wrap :: b -> FD a
    unwrap :: FD a -> b

instance F a b where
    type BThing a = b
    data FD a = FDC (BThing a)
    wrap b = FDC b
    unwrap (FDC b) = b

Incidentally, that "type BThing a = b" line also blows up with
"Not in scope: type variable `b'".

Thanks,

Matthew
-- 
Matthew Sackman
http://www.wellquite.org/