[tree_of_item]

I'm not gonna read all your code, and I'm not even sure if this is your problem, but just as a pattern match based on what you said: for System F, only the first and second ranks have decidable inference, not the whole thing. Inference in the first rank is often referred to as the "Hindley-Milner" algorithm; you can infer types for the second fragment but I'm not aware of an implementation. After that it's undecidable.

To put that another way, if `forall a.` introduces types (it's like the big lambda), then you can only have a type with `forall`s on the left on the outside. So:

`forall a. forall b. a + b` is a type but

`forall a. a -> forall b. b -> c` is not a type since that `forall` isn't all the way on the left in a chain like the first one.

If you're not in that fragment, and you're trying to infer types, you're gonna have a bad time unless you've got something exceedingly clever up your sleeve.

So `ForAll` should not be one of the "Type" type constructors. It should be its own type, like

    # The int is the number of variables bound, then the type is the type that uses them
    data Scheme = Int Type
    data Type = 0 | 1 | Var Int | Product Type Type | ...