More Polymorphic Recursion

I've been obsessed with polymorphic recursion lately.  I originally just wanted to write a data structure like a list but with efficient insertion on both sides, sometimes called a deque.  The problem is that type inference in the presence of polymorphic recursion is undecidable, in a nice reduction to semi-unification by Herblein.  On the other hand, we don't need type inference.  I'm more than happy to write the type of a function in ML or Haskell, and type checking is decidable with polymorphic recursion. It's sad that SML will never be able to do this.  Apparently OCaml 3.12 will allow it. 

Reading the mailing lists from 1994 when this was being debated on the Haskell mailing list, I found a very interesting example from Mark Jones.  He found that polymorphic recursion would break his implementation of type classes that didn't pass a dictionary at run time.  Without PR, he could statically analyze the whole program and hard code the type class function calls.  He points out with the following that it's no longer possible with PR:

f  :: Eq a => a -> Bool

f x = x==x || f [x]

Note that if I write

data D = D

instance Show D where

_ == _ = False

then calling f D will require infinitely many instances of f. 

I also found a good paper by Kfoury et al. showing lots of examples of polymorphic 

recursion in action, and how many of the cases can be overcome using intersection

types (my friend William Lovas' specialty.)