I'm sure anyone who's used Haskell for any significant length of time has received this error message: Occurs check: cannot construct the infinite type: t = t -> t1 I for one took that as a challenge, and have implemented a type inference engine for infinite types. Expr> s (a -> b -> c) -> (a -> b) -> a -> c Expr> skk a -> a Expr> s(skk)(skk) (fix a . (a -> b)) Expr> Points of interest: * There are NO error conditions. it-unifier can assign a type to every syntactically valid expression of combinatory logic. * Typechecking is guaranteed to terminate in a linear number of steps, an (apparently) stronger guarantee than that provided by DHM. * (Mostly theoretical, since it-unify does not yet support sums or products): Fixpoint types subsume declared recursive datatypes. e.g: type List a = fix l . Either () (a,l) darcs get http://members.cox.net/stefanor/fixtypes/