Dear Haskell users, I am playing around with a variation of the Church numerals and it is giving me grief. Usually the definitions for Church numerals appear as follows. zero = \s z -> z succ x = \s z -> s (x s z) But what I would like to do is define them this way. zero = \s z ->z succ x = \s z -> s x (x s z). I don't think it's important that I explain why I want the extra occurrence of x there. Just typing this in hugs or ghci gives problems. In ghci the error message is Occurs check: cannot construct the infinite type: t = (t -> t3 -> t2) -> t2 -> t1 Expected type: t Inferred type: (t -> t3 -> t2) -> t2 -> t1 In the first argument of `x', namely `s' In the second argument of `s', namely `(x s z)' I know about rank-2 polymorphic types. (I don't really understand it but I have used them). I attempted to create a type with the following declaration. data Church = Ch (forall a.(a -> a -> a) -> a -> a) I declared an unCh unCh (Ch a) = a I then declared succ as succ x = Ch(\s z -> s x (unCh x s z) which gives the strange typing error: Inferred type is less polymorphic than expected Quantified type variable `a' is unified with `Church' Signature type: forall a. (a -> a -> a) -> a -> a Type to generalise: (Church -> Church -> Church) -> Church -> Church When checking an expression type signature In the first argument of `Ch', namely `(\ s z -> s x (unCh x s z))' in the definition of function `succ': Ch (\ s z -> s x (unCh x s z)) Doesn't the "type to generalise" fit within the framework of forall a.(a->a->a) ->a ->a. Why should it matter if something is _less_ polymorphic than expected. This is something I do not understand. Now, if I modify the definition to succ = \s z -> s x (unCh x s z) I can at least load the file. succ zero gives me _no_ typing errors. However succ (succ zero) gives me a typing error again. (And I know why) Because the type of succ zero is "(Church -> Church -> Church) -> Church -> Church" and not just simply "Church". (that is what the constructor Ch is supposed to do but it complains of the typing being less polymorphic than expected). Is this sort of typing possible within Haskell. I realise that it is sort of an infinite data type but in my opinion these sorts of things should be able to be typed. Thanks in advance. Sean Seefried.