Guy,
I agree that the report should be updated to express the restriction we
really have in mind. Simon: as editor, this is your bailiwick!
I also think its neat that you seem to have found a use for cyclic
unification. This is definitely an impetus to extend the language to
include cyclic types. (I don't expect we'll do this for a while
though. You might consider modifying the Glasgow Haskell compiler to
include this yourself -- it may not be too difficult.)
However, I am confused by some of your example. You want to use a data
structure like
data FooTree a = Leaf a | Node (FooTree (Wrapper a)) (FooTree (Wrapper a))
data Wrapper a = Annotation a Int
This seems to add an additional level of annotation at every
Node. Something zero nodes deep has zero annotations, something
five nodes deep has five annotations. Is this really what you
want?
Because of the way type inference works in the Hindley-Milner system,
it is impossible to write a function that will act on values of the
type (FooTree a) as defined above. (This is independent of the
additional complications you mention.) The reason is that every
instance of a function in a recursive definition must have the same
type as the function being defined. But to define a function on
(FooTree a) you need a recursive instance of type (FooTree (Wrapper
a)). Mycroft first suggested a type system that would allow such
functions to be typed, but I think it is still an open question as to
whether an inference algorithm exists for the type system. (There was
a paper published that claimed an algorithm, but it was later withdrawn
as incorrect.)
So I hope you don't really need the types above, because then
we can't help you, even in the monomorphic case!
But would the simpler type perhaps work?
data FooTree a b = Leaf b | Node a (FooTree a b) a (FooTree a b)
where a ranges over annotation, and b over leaf values? Cheers, -- P
