[Haskell-cafe] OT: Isorecursive types and type abstraction

[Edsko de Vries]

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.