(* Polymorphic: A Lying Dynamic Promotion (like ex8.aff -- blame inc(:>)) *)

let ap : all 'a. ('a -> 'a) -> 'a -> 'a =
  fun 'a ->
    fun f: ('a -> 'a) ->
      fun x: 'a ->
        f (f x)    (* f is used twice here, despite what iap2 claims *)

let inc : int -> int =
  fun y: int ->
    (fun g: (int -o int) ->
       (ap[int] :  (int -> int) -> int -> int   (* This cast goes bad *)
                :> (int -o int) -> int -o int) g y)
    (fun z: int -> z + 1)

in print[int] (inc 5)