I have a situation in which I have two kinds of trees. The simplified
example is linked lists:

type foo = [`Nil | `Tree of foo]
type bar = [`Nil | `Leaf of int | `Tree of bar]

I have a tree with only shape, and a tree with some information. I want to
be able to distinguish between these.  Here I have functions to assert
types, but these annotations will be part of the signatures of functions
actually doing things in the real code. But I do want to have these static
checks on contests.

let f x : foo = x
let g x : bar = x
let a = `Tree (`Nil)
let b = `Tree (a)
let c = `Tree (f a)
let d = `Tree (`Leaf 1)

As is proper, I can run f on a, b, and c, but not on d. D is not a valid
foo.
But I cannot run g on c. This makes sense, as I have said 'a tree of bars
contains a bars.' But I want to somehow note that a tree of bars MIGHT
contain foo's. Is there any way to annotate this?

I cannot say

type bar = [`Nil | `Leaf of int | `Tree of [bar | foo]] as bar is not fully
defined.
I cannot say
type bar = [`Leaf of int | `Tree of bar | foo] because tree cannot have two
separate types.

The current, icky, non-variant type solution has the equivalent of
type 'a foo = Nil | Tree of foo | F of 'a
With special things filling in for 'a. But I end up putting EVERYTHING in 'a
because I don't have a way to statically guaranteeing that my "leaf foo"'s
are valid "leaf or branch foo's". So I have a weaker system than I want.

Any suggestions? Seems like variant types should work here. I COULD add type
annotations to functions, check them, and then remove the annotations so
that my types are never constrained. I think that might even work. But it
seems rather icky.

-- 
Seth Fogarty             sfogarty@[gmail.com|rice.edu|livejournal]
Neep-neep at large    AIM: Sorrath
"I know there are people in this world who do not love their fellow
human beings - and I hate people like that" --Tom Lehrer.