[TYPES] Isorecursive types and type abstraction

[Edsko de Vries]

Hi Stephanie,

> What you need is a higher-kinded version of Fix (parameterized  
> recursive type), with the associated fold and unfold rules. You can  
> find these rules in the paper:
> 
>    Flexible Type Analysis, Karl Crary and Stephanie Weirich, ICFP 99
> 
>    http://www.seas.upenn.edu/~sweirich/papers/lx/lxpaper.pdf

Thank you for your answer. The paper looks interesting and I will study
it. Do I understand correctly that it will give me a fix operator that
allows me to rewrite Perfect and lift the /\A over the Fix operator,
just like for List?

In a way though that circumvents the problem I'm having rather than
solving it. That is ok, but it does mean having to introduce a more
complicated Fix operator, and it seems to me that there should be
simpler solution. But perhaps there isn't.

Either, I appreciate the pointer. Thanks!

Edsko