Unusual interaction with (polymorphic) recursion

[chaudhuri]

trafficstars

In the following, grow1 (the most natural) and grow2 don't work, with the error messages in comments, while grow3 works. This is using the HEAD from 2014-09-12T09:30:00+0200 or thereabouts, probably commit 1d7f380b.

module type SHOW =
sig
  type t
  val show : t -> string
end

implicit functor ShowPair (Show1 : SHOW) (Show2 : SHOW) =
struct
  type t = Show1.t * Show2.t
  let show (x, y) = "(" ^ Show1.show x ^ ", " ^ Show2.show y ^ ")"
end

let rec grow1 : (implicit Show : SHOW) -> Show.t -> 'a =
  fun (implicit Show : SHOW) x -> grow1 (x, x)
(*
    fun (implicit Show : SHOW) x -> grow1 (x, x);;
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type (implicit Show : SHOW) -> 'b -> 'a
       but an expression was expected of type
         (implicit Show : SHOW) -> Show.t -> 'a
       This instance of Show.t is ambiguous:
       it would escape the scope of its equation
 *)

let rec grow2 : 'a. (implicit Show : SHOW with type t = 'a) -> 'a -> 'b =
  fun (type a) (implicit Show : SHOW with type t = a) x ->
  let module Show2 = ShowPair (Show) (Show) in
  grow2 (implicit Show2) (x, x)
(*
Error: This expression has type
         (implicit Show : SHOW with type t = 'a) -> Show.t -> 'b
       but an expression was expected of type
         (implicit Show : SHOW with type t = 'a) -> 'a -> 'b
       The type variable 'a occurs inside 'a
 *)

let rec grow3 : 'a. (implicit Show : SHOW with type t = 'a) -> Show.t -> 'b =
  fun (type a) (implicit Show : SHOW with type t = a) x ->
  let module Show2 = ShowPair (Show) (Show) in
  grow3 (implicit Show2) (x, x)

[let-def]

Both examples work (on my branch) when annotating x:

let rec grow1 : (implicit Show : SHOW) -> Show.t -> 'a =
  fun (implicit Show : SHOW) (x : Show.t) -> grow1 (x, x)

let rec grow2 : 'a. (implicit Show : SHOW with type t = 'a) -> 'a -> 'b =
  fun (type a) (implicit Show : SHOW with type t = a) (x : a) ->
  let module Show2 = ShowPair (Show) (Show) in
  grow2 (implicit Show2) (x, x)

So this is related to inference in presence of polymorphic recursion, like #5 . I don't know what an acceptable approximation should be in this case (beside providing better error messages :)).

[lpw25]

grow1 is fixed by the addition of forward type propagation (#19)