Strange type with extension RankNTypes

Question

I am trying to experiment with System-F types in Haskell and have implemented church natural number coding via type .

When loading this code

 {-# OPTIONS_GHC -Wall #-} {-# LANGUAGE RankNTypes #-} type CNat = forall t . (t -> t) -> (t -> t) c0 :: CNat c0 _ x = x type CPair ab = forall t . (a -> b -> t) -> t cpair :: a -> b -> CPair ab cpair abf = fab -- pair3 :: CPair CNat String pair3 = cpair c0 "hello" 

in ghci 7.8.2 I get a warning:

 λ: :l test.hs [1 of 1] Compiling Main ( test.hs, interpreted ) test.hs:29:1: Warning: Top-level binding with no type signature: pair3 :: forall t t1. (((t1 -> t1) -> t1 -> t1) -> [Char] -> t) -> t Ok, modules loaded: Main. λ: 

The question is whether the type should be

 pair3 :: forall t. ((forall t1. (t1 -> t1) -> t1 -> t1) -> [Char] -> t) -> t 

?

UPD: A simple example is given.

Answer 1

But is there a way to specify my type for it, so that when I specify it explicitly (uncomment the line in my code), the compiler does not output it, but simply check the type provided? Now i get an error

If you want to instantiate variables of type a,b that are part of type cpair , you can add the following explicit annotation.

 pair3 :: CPair CNat String pair3 = (cpair :: CNat -> String -> CPair CNat String) c0 "hello" 

Without this, cpair is only instantiated on monomorphic types, I suppose.

Answer 2

This is the ideal type for him ... but this is not the type that Hindley-Milner gives. HM always has a rank-1 type. I believe that rank-2 type inference is indeed decidable, but the GHC is not even trying.