A problem with the typing system.

[Sean Seefried]

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.