[Haskell] Polymorphic types without type constructors?

[Shin-Cheng Mu]

Hi,

I have been thinking about using Haskell (extended with
higher ranked polymorphism) to demonstrate to my colleagues
some ideas in second-order lambda calculus. It turned out,
however, I am puzzled by the type system myself. So I've
written to seek for help. :)

I started with define Church numerals as

 > type N = forall a . (a -> a) -> a -> a

(The syntax above works only for GHC. In Hugs I would have to write
    type N a = (a -> a) -> a -> a
  and replace every N below with (forall a. N a))
I should have used newtype or data instead of a type synonym,
but I wanted it to look more like seond-order lambda calculus
so I tried to omit the constructor if possible.

I could define addition and multiplication smoothly.

 > zero :: N
 > zero = \f -> \a ->  a

 > succ :: N -> N
 > succ n = \f -> \a -> f (n f a)

 > add, mul :: N -> N -> N
 > add m n = \f -> \a -> m f (n f a)
 > mul m n = \f -> \a -> m (n f) a

But when it comes to exponential, GHCi complained about type
being not polymorphic enough.

 > exp :: N -> N -> N
 > exp m n = n (mul m) one

GHC said:
     Inferred type is less polymorphic than expected
         Quantified type variable `a' escapes
         Expected type: ((a -> a) -> a -> a) -> (a -> a) -> a -> a
         Inferred type: (forall a2. (a2 -> a2) -> a2 -> a2)
                        -> (a1 -> a1) -> a1 -> a1
     In the application `mul m'
     In the first argument of `n', namely `(mul m)'

On the other hand, there is another definition of exp

 > exp2 :: N -> N -> N
 > exp2 m n = n m

which would type check.

It seems to me that the difference is: in the case of the second
definition of exp, the type variable in N can be instantiated to
a monomorphic type (the same with add and mul).

  exp2 = \m::N -> \n::N -> \f::(b -> b) -> \b::b ->
            n [b->b] (m[b]) f b

(where square brackets denote type application)
while in the first exp, n::N is instantiated to a polymorphic type
(another N):

  exp = \m::N -> \n::N -> \f::(b -> b) -> \b::b ->
           (n[N] (mul m) one)[b] f b

I tried to add more type signatures to inform GHC of the fact
that n::N is to be instantiated to a polymorphic type. However
none of the attempts worked so far. I then noticed that in the
GHC User's Guide (Sec 7.4.9) it was written

   "There is one place you cannot put a forall: you cannot
    instantiate a type variable with a forall-type. So you cannot
    make a forall-type the argument of a type constructor."

The examples followed are all about type constructors (for example
[forall a. a->a], a list of for-all's, is illegal). But is this
the reason why exp cannot be typed?

If so, is there a reason for such a restriction?

Thank you very much!

sincerely,
Shin-Cheng Mu