Scope of type variables in associated types

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
15 messages Options
Reply | Threaded
Open this post in threaded view
|

Scope of type variables in associated types

Matthew Sackman-2
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'". I was rather hoping it would be
in scope. I've tried:

> instance forall a b . G a b where
> ...

but that doesn't seem to extend the scope as it does with functions. I
realise this is bleeding edge stuff. But I can't seem to work out
from the various wiki pages on this whether this is going to be
eventually supported. This is all with today's GHC HEAD.

Cheers,

Matthew
--
Matthew Sackman
http://www.wellquite.org/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Matthew Sackman-2
On Sat, May 19, 2007 at 08:40:46PM +0100, Matthew Sackman 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'". I was rather hoping it would be
> in scope.

Having thought about this for some time, I think I can see a reason that
this might not be possible.

Classes are open, thus the a -> b does not ensure that there will
only ever be one E a for each unique a in G a b, given multiple modules.

>From the paper [0], pg 10:

   "We could also in principle allow an associated type to mention only
   a subset of its parent class parameters; but then we would need to
   make extra tests to ensure the instance declarations did not overlap
   taking into account only the selected class parameters to ensure the
   type translation described by \Omega is confluent."

Well, I suppose that given the open type classes, the instance
declarations can overlap, despite the fundep. Does this mean that until
we get closed classes, this sort of thing is impossible (without ugly
workarounds)?

Any thoughts at all? Anyone? Is it the case that associated types really
allow nothing that can't be done with fundeps?

[0] "Associated Types with Class"
    http://www.cse.unsw.edu.au/~chak/papers/CKPM05.html

Matthew
--
Matthew Sackman
http://www.wellquite.org/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

RE: Scope of type variables in associated types

Simon Peyton Jones
In reply to this post by Matthew Sackman-2
| 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


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

Simon
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Matthew Sackman-2
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/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

RE: Scope of type variables in associated types

Simon Peyton Jones
| > | > 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

I was wrong.  It's not a bug.  E is supposed to be a type *function*, so it can't mention anything on the RHS that is not bound on the LHS.  We'll improve the documentation.

| 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

As I said, associated types are an *alternative* to fundeps. We have not even begun to think about what happens if you use both of them together.  You should not need to do so.

| 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'".

No, that is wrong in the same way as before.  BThing is a *function* so its results must depend only on its arguments.

S
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Matthew Sackman-2
On Mon, May 21, 2007 at 12:39:20PM +0100, Simon Peyton-Jones wrote:

> | > | > 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
>
> I was wrong.  It's not a bug.  E is supposed to be a type *function*,
> so it can't mention anything on the RHS that is not bound on the LHS.
> We'll improve the documentation.

Ok, thanks for the clarification. One final question then, how could I
rewrite the following in associated types:

class OneStep a b | a -> b
instance OneStep (Cons v t) t

class TwoStep a b | a -> b
instance (OneStep a b, OneStep b c) => TwoStep a c

If the fundep and b is dropped then I get:

class OneStep a
    data OS a :: *
instance OneStep (Cons v t)
    data OS (Cons v t) = t

class TwoStep a
    data TS a :: *
instance (OneStep a, OneStep b) => TwoStep a

This last one can't be right, as I can't express the fact that the OS in
"OneStep a" provides the link with "OneStep b". So is there a way to
achieve this sort of chaining with associated types?

Sure, the fundep version requires undecidable instances, but I've been
writing quite a lot of code lately that requires that!

Many thanks,

Matthew
--
Matthew Sackman
http://www.wellquite.org/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Andres Loeh-2
> class OneStep a
>     data OS a :: *
> instance OneStep (Cons v t)
>     data OS (Cons v t) = t
>
> class TwoStep a
>     data TS a :: *
> instance (OneStep a, OneStep b) => TwoStep a

instance (OneStep a, OneStep (OS a)) => TwoStep a
?

Cheers,
  Andres
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Tom Schrijvers-2
In reply to this post by Matthew Sackman-2
> Ok, thanks for the clarification. One final question then, how could I
> rewrite the following in associated types:
>
> class OneStep a b | a -> b
> instance OneStep (Cons v t) t
>
> class TwoStep a b | a -> b
> instance (OneStep a b, OneStep b c) => TwoStep a c
>
> If the fundep and b is dropped then I get:
>
> class OneStep a
>    data OS a :: *
> instance OneStep (Cons v t)
>    data OS (Cons v t) = t <<<< data constructor missing !!!
>
> class TwoStep a
>    data TS a :: *
> instance (OneStep a, OneStep b) => TwoStep a
>
> This last one can't be right, as I can't express the fact that the OS in
> "OneStep a" provides the link with "OneStep b". So is there a way to
> achieve this sort of chaining with associated types?

You'd have to write

> class OneStep a
>    data OS a :: *
> instance OneStep (Cons v t)
>    data OS (Cons v t) = OSC t
>
> class TwoStep a
>    data TS a :: *
> instance (OneStep a, OneStep (OS a)) => TwoStep a where
>    type TS a = TSC (OS (OS a))

which seems rather awkward with all these additional data type
constructors.

You'd be better off with associated type synonyms:

> class OneStep a
>    type OS a :: *
> instance OneStep (Cons v t)
>    type OS (Cons v t) = t
>
> class TwoStep a
>    type TS a :: *
> instance (OneStep a, OneStep (OS a)) => TwoStep a
>    type TS a = OS (OS a)

which are currently under development.

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Matthew Sackman-2
In reply to this post by Andres Loeh-2
Andres Loeh <[hidden email]> wrote:

> > class OneStep a
> >     data OS a :: *
> > instance OneStep (Cons v t)
> >     data OS (Cons v t) = t
> >
> > class TwoStep a
> >     data TS a :: *
> > instance (OneStep a, OneStep b) => TwoStep a
>
> instance (OneStep a, OneStep (OS a)) => TwoStep a
> ?

Doesn't seem to work. Ok, my original was wrong as I had no constructor
on the associated type. So below are 2 versions, one with fundeps, which
works, one with associated type synonynms which doesn't work, which
made me remember the warnings about how type synonynms aren't fully
implemented yet, and so I wrote a third version with indexed types, but
whilst I can make it work, wrapping up values in indexed types gets
really really messy.

> {-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
>
> module TestProb where
>
> data Nil = Nil
> data Cons v t = Cons v t
>
> class OneStep a b | a -> b
> instance OneStep (Cons v t) t
>
> class TwoStep a b | a -> b
> instance (OneStep a b, OneStep b c) => TwoStep a c
>
> class OneStep' a where
>     type OS' a :: *
>
> instance OneStep' (Cons v t) where
>     type OS' (Cons v t) = t
>
> class TwoStep' a where
>     type TS' a :: *
>
> instance (OneStep' a, OneStep' (OS' a)) => TwoStep' a where
>     type TS' a = (OS' (OS' a))
>
> foo :: (TwoStep a b) => a -> b -> Bool
> foo _ _ = True
>
> foo' :: (TwoStep' a) => a -> TS' a -> Bool
> foo' _ _ = True

*TestProb> foo (Cons True (Cons 'b' (Cons "hello" Nil))) (Cons "boo" Nil)
True

*TestProb> :t foo (Cons True (Cons 'b' (Cons "hello" Nil)))
foo (Cons True (Cons 'b' (Cons "hello" Nil))) :: Cons [Char] Nil -> Bool

*TestProb> :t foo' (Cons True (Cons 'b' (Cons "hello" Nil)))

<interactive>:1:0:
    No instance for (OneStep'
                       (OS' (Cons Bool (Cons Char (Cons [Char] Nil)))))
      arising from a use of `foo'' at <interactive>:1:0-45
    Possible fix:
      add an instance declaration for
      (OneStep' (OS' (Cons Bool (Cons Char (Cons [Char] Nil)))))

Mmm. This is as a result of the instance (OneStep' a, OneStep' (OS' a))
constraint. Is it just me or does this look like the type synonynm isn't
being applied? So how about adding:

> instance (OneStep' a) => OneStep' (OS' a) where
>     type OS' (OS' a) = a

*TestProb> :t foo' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil))))
foo' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) :: (Fractional t) =>
                                                             TS' (Cons Bool (Cons Char (Cons t (Cons [Char] Nil))))
                                                             -> Bool

Okay, but how do I inhabit that type?

*TestProb> :t foo' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) (Cons 5.3 (Cons "hello" Nil))

<interactive>:1:59:
    Couldn't match expected type `TS'
                                    (Cons Bool (Cons Char (Cons t (Cons [Char] Nil))))'
           against inferred type `Cons t1 (Cons [Char] Nil)'
    In the second argument of `foo'', namely
        `(Cons 5.3 (Cons "hello" Nil))'

So now, the third (and final!) version using indexed types:

> class OneStep'' a where
>     data OS'' a :: *
>     mkOS'' :: a -> OS'' a
>
> instance OneStep'' (Cons v t) where
>     data OS'' (Cons v t) = OSC'' t
>     mkOS'' (Cons v t) = OSC'' t
>
> instance (OneStep'' a) => OneStep'' (OS'' a) where
>     data OS'' (OS'' a) = OSC''w a
>
> class TwoStep'' a where
>     data TS'' a :: *
>     mkTS'' :: a -> TS'' a
>
> instance (OneStep'' a, OneStep'' (OS'' a)) => TwoStep'' a where
>     data TS'' a = TSC'' (OS'' (OS'' a))
>     mkTS'' = TSC'' . mkOS'' . mkOS''
>
> foo'' :: (TwoStep'' a) => a -> TS'' a -> Bool
> foo'' _ _ = True

This, sort of works:

*TestProb> let ts = mkTS'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts
True

But of course, the wrapping into the indexed type demands the use of
mkTS''.

You can't even write:
*TestProb> let ts = mkOS'' (Cons 'c' (Cons 5.3 (Cons "hello" Nil))) in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts

<interactive>:1:119:
    Couldn't match expected type `TS''
                                    (Cons Bool (Cons Char (Cons t (Cons [Char] Nil))))'
           against inferred type `OS''
                                    (Cons Char (Cons t1 (Cons [Char] Nil)))'
    In the second argument of `foo''', namely `ts'
    In the expression:
        let ts = mkOS'' (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))
        in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts
    In the definition of `it':
        it = let ts = mkOS'' (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))
             in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts

Further, it is *impossible* to define mkTS'' for the extra
instance "instance (OneStep'' a) => OneStep'' (OS'' a) where" as to do
so would demand unwrapping the supplied (OS'' a) which can't be done -
if you try to add unwrop :: OS'' a -> a to the class OneStep'' then try
to define it for the Cons instance - I've thrown away v so how are you
going to get it back? undefined?

Matthew
--
Matthew Sackman
http://www.wellquite.org/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Matthew Sackman-2
On Mon, May 21, 2007 at 02:08:13PM +0100, Matthew Sackman wrote:
> Further, it is *impossible* to define mkTS'' for the extra
                                        ^^^^ -- should be mkOS''

But actually, in that code, the data declaration was never even used
either - all that is needed is:
instance (OneStep'' a) => OneStep'' (OS'' a)

But it does rather leave a mess in the code.

Matthew
--
Matthew Sackman
http://www.wellquite.org/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Bertram Felgenhauer-2
In reply to this post by Matthew Sackman-2
Matthew Sackman wrote:
> >         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:

How does

  class F a where
      data B a :: *
      data E a :: *
      wrap :: B a -> E a
      unwrap :: E a -> B a

sound? 'B a' would represent the 'b' in your previous attempt,

  class F a b | a -> b where
  ...

Bertram
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Matthew Brecknell
Bertram Felgenhauer:

> How does
>
>   class F a where
>       data B a :: *
>       data E a :: *
>       wrap :: B a -> E a
>       unwrap :: E a -> B a
>
> sound? 'B a' would represent the 'b' in your previous attempt,
>
>   class F a b | a -> b where
>   ...
>

I'm with Simon in thinking that this code is suspicious.

For any given call to "wrap" or "unwrap", how is the compiler supposed
to determine which instance to use, given that "a" cannot be uniquely
determined from the type of the function? The same question also applies
to Matthew's original formulation using functional dependencies:

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

Simon's reformulation doesn't have this problem:

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Bertram Felgenhauer-2
Matthew Brecknell wrote:

> Bertram Felgenhauer:
> > How does
> >
> >   class F a where
> >       data B a :: *
> >       data E a :: *
> >       wrap :: B a -> E a
> >       unwrap :: E a -> B a
> >
> > sound? 'B a' would represent the 'b' in your previous attempt,
> >
> >   class F a b | a -> b where
> >   ...
> >
>
> I'm with Simon in thinking that this code is suspicious.

It wasn't my code Simon was replying to.

> For any given call to "wrap" or "unwrap", how is the compiler supposed
> to determine which instance to use, given that "a" cannot be uniquely
> determined from the type of the function?

As far as my limited understanding goes this should work, because we
are using an associated *data* type here. This means we can't have
instances saying 'type B a = Int', we have to use either a newtype
or a data declaration for that. As a side effect, the compiler can
determine 'a' from 'B a'.

This wouldn't be possible for associated type synonyms, but those
aren't completely implemented yet anyway (again, as far as I know).

Bertram
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Matthew Sackman-2
In reply to this post by Matthew Brecknell
"Matthew Brecknell" <[hidden email]> wrote:

> Bertram Felgenhauer:
> > How does
> >
> >   class F a where
> >       data B a :: *
> >       data E a :: *
> >       wrap :: B a -> E a
> >       unwrap :: E a -> B a
> >
> For any given call to "wrap" or "unwrap", how is the compiler supposed
> to determine which instance to use, given that "a" cannot be uniquely
> determined from the type of the function?

If it can't be uniquely determined then it blows up, as always. As far
as my understanding of type classes goes, for any call to a function in
a type class, the compiler must be able to determine a single instance
to call. So if all we know is that we have a "B a" then all we can do is
hope there's an instance "F a".

> The same question also applies
> to Matthew's original formulation using functional dependencies:
>
> > class G a b | a -> b where
> >     data E a :: *
> >     wrap :: b -> E a
> >     unwrap :: E a -> b

Well here you certainly have less information, but you can still
determine the instance - in both wrap and unwrap you have an "E a" which
means the compiler will be able to work out some constraints on "a".
There's also a "b" so it can also check that the fundep is respected, or
incorporate the extra information into its decision making process.

Note that both the above do type check and compile, and I have working
instances of the latter:

class CellBuilder c t n | c -> t n where
    data Cell c :: *
    makeCell :: t -> (MVar (Cell n)) -> Cell c
    unpackCell :: Cell c -> (t, (MVar (Cell n)))

instance CellBuilder (Cons t n) t n where
    data Cell (Cons t n) = CellCons t (MVar (Cell n))
    makeCell v mvar = CellCons v mvar
    unpackCell (CellCons v mvar) = (v, mvar)

Matthew
--
Matthew Sackman
http://www.wellquite.org/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Scope of type variables in associated types

Manuel M T Chakravarty
In reply to this post by Matthew Sackman-2
Matthew Sackman wrote:

> Andres Loeh <[hidden email]> wrote:
>>> class OneStep a
>>>     data OS a :: *
>>> instance OneStep (Cons v t)
>>>     data OS (Cons v t) = t
>>>
>>> class TwoStep a
>>>     data TS a :: *
>>> instance (OneStep a, OneStep b) => TwoStep a
>> instance (OneStep a, OneStep (OS a)) => TwoStep a
>> ?
>
> Doesn't seem to work. Ok, my original was wrong as I had no constructor
> on the associated type. So below are 2 versions, one with fundeps, which
> works, one with associated type synonynms which doesn't work, which
> made me remember the warnings about how type synonynms aren't fully
> implemented yet, and so I wrote a third version with indexed types, but
> whilst I can make it work, wrapping up values in indexed types gets
> really really messy.

Yes, it's messy with indexed data families as they force you to introduce all
these new constructors and the corresponding wrapping and unwrapping code.  As
Tom wrote in another message in this thread, you really do want to use indexed
synonyms families (aka associated type synonyms) here.  They will do what you
want.  We are currently working on completing the implementation of
synonym families.[1]

Manuel

[1] For those who wonder why this is taking so long, we are working on a system
     that is actually significantly more general than what we described in the
     ICFP05 paper.  In particular, we want synonym families to play nice with
     GADTs.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe