Hello, (Apologies for the two emails, I accidentally hit the send button on my client before I had finished the first e-mail...) * Rank-2 vs Rank-n types. I think that this is the most important issue that we need to resolve which is why I am placing it first :-) Our options (please feel free to suggest others) - option 1: Hugs style rank-2 types (what I described , very briefly, on the ticket) * Based on "From Hindley Milner Types to First-Class Structures" * Predicative * Requires function with rank-2 types to be applied to all their polymorphic arguments. - option 2: GHC 6.4 style rank-N types. As far as I understand, these are the details: * Based on "Putting Type Annotations to Work". * Predicative * We do not compare schemes for equality but, rather, for generality, using a kind of sub-typing. * Function type constructors are special (there are two of them) because of co/contra variance issues. - option 3: GHC 6.6 style rank-N types. This one I am less familiar with but here is my understanding: * Based on "Boxy types: type inference for higher-rank types and impredicativity" * Impredicative (type variables may be bound to schemes) * Sometimes we compare schemes for equality (this is demonstrated by the example on ticket 57) and we also use the sub-typing by generality on schemes * Again, function types are special So far, Andres and Stephanie prefer a system based on rank-N types (which flavor?), and I prefer the rank-2 design. Atze would like a more expressive system that accepts the example presented on the ticket. I think this is all. -Iavor