Hi, This is rather off-topic but the audience of this list may be the right one; if there is a more appropriate venue for this question, please let me know. Most descriptions of recursive types state that iso-recursive types (with explicit 'fold' and 'unfold' operators) are easy to typecheck, and that equi-recursive types are much more difficult. My question regards using iso-recursive types (explicitly, not implicitly using algebraic data types) together with type abstraction and application. The usual typing rules for fold and unfold are e :: Fix X. t ----------------------------- Unfold unfold e :: [X := Fix X. t] t e :: [X := Fix X. t] t ----------------------------- Fold fold e : Fix X. t This works ok for the following type: ListInt = Fix L. 1 + Int * L (where "1" is the unit type). If x :: ListInt then unfold x :: 1 + Int * ListInt using the Unfold typing rule. However, this breaks when using type abstraction and application. Consider the polymorphic version of list: List = Fix L. /\A. 1 + A * L A Now if we have x :: List Int we can no longer type unfold x because x does not have type (Fix ..), but ((Fix ..) Int) instead. Of course, we can unroll List Int by first unrolling List, and then re-applying the unrolled type to Int to get (/\A. 1 + A * (Fix L. /\A. 1 * L A) A) Int which can be simplified to 1 + Int * List Int but this is not usually mentioned (that I could find; in particular, TAPL does not mention it) and I'm worried that there are subtleties here that I'm missing--nor do I have an exact definition of what this 'extended' unrolling rule should do. Any hints or pointers to relevant literature would be appreciated! Edsko PS. One way to simplify the problem is to redefine List as List = /\A. Fix L. 1 + A * L so that List Int can easily be simplified to the right form (Fix ..); but that can only be done for regular datatypes. For example, the nested type Perfect = Fix L. /\A. A + Perfect (A, A) cannot be so rewritten because the argument to Perfect in the recursive call is different.