I also think its neat that you seem to have found a use for cyclic
unification. This is definitely an impetus to extend the language to
include cyclic types. (I don't expect we'll do this for a while
though. You might consider modifying the Glasgow Haskell compiler to
include this
Lennart Augustsson writes:
I thought there were problems with extending Hindley-Milner type systems
with cyclic types: The type inference can handle type correct programs,
but will loop for certain type incorrect programs, or am I mistaken?
It is absolutely unproblematic to extend
Lennart mentioned this recently; the situation is as follows:
1. semi-unification (the general one) is undecidable
2. it is semi-decidable
3. the semi-decision procedure for semi-unification can be augmented
with heuristics that finds almost all cases in which it fails
(this is a kind of
