OCaml polymorphic recursion errors

Question

Given the following types:

type _ task =
| Success : 'a -> 'a task
| Fail : 'a -> 'a task
| Binding : (('a task -> unit) -> unit) -> 'a task
| AndThen : ('a -> 'b task) * 'a task -> 'b task
| OnError : ('a -> 'b task) * 'a task -> 'b task

type _ stack =
| NoStack : 'a stack
| AndThenStack : ('a -> 'b task) * 'b stack -> 'a stack
| OnErrorStack : ('a -> 'b task) * 'b stack -> 'a stack

type 'a process = 
{ root: 'a task 
; stack: 'a stack 
}

let rec loop : 'a. 'a process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest  <-- ERROR HERE
    in
    step proc.stack
| Fail value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (_callback, rest) -> step rest
    | OnErrorStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    in
    step proc.stack
| Binding callback -> callback (fun task -> loop {proc with root = task} )
| AndThen (callback, task) -> loop {root = task; stack = AndThenStack (callback, proc.stack)}
| OnError (callback, task) -> loop {root = task; stack = OnErrorStack (callback, proc.stack)}

I get an error from the compiler:

Error: This expression has type b#1 stack but an expression was expected of type 'a stack The type constructor b#1 would escape its scope

In this line of code:

| Success value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest  <-- ERROR HERE
    in
    step proc.stack

It's taken a while to get this far without running into an obscure error message that is inevitably corrected by using some helper types, but I can't seem to figure out how to correct this issue with a helper, or if I'm attempting to do something silly with my types.

What is the correct way to eliminate this error?

Caudillo

Note that existential type error messages ( all variants of "a#987 is not compatible with b#31, it would escape its scope") have been tremendously improved starting from 4.03. I think it is worth it to switch to a recent OCaml compiler when working on GADTs heavy code. – Maryland

That would be a big help. I'm new to GADT's, and the cryptic errors messages that OCaml v4.02.3 throws aren't helping the learning curve. Sadly, I'm not able to change the version due to bucklescript – Caudillo

Answer 1

A second variable needed to be added to the task type definition to express separate success and failure values. Here is the complete solution:

type (_,_) task =
| Success : 'a -> ('a,_) task
| Fail : 'x -> (_,'x) task
| Binding : ((('a,'x) task -> unit) -> unit) -> ('a,'x) task
| AndThen : ('a -> ('b,'x) task) * ('a,'x) task -> ('b,'x) task
| OnError : ('x -> ('a,'y) task) * ('a,'x) task -> ('a,'y) task

type (_,_) stack =
| NoStack : (_,_) stack
| AndThenStack : ('a -> ('b,'x) task) * ('b,'x) stack -> ('a,'x) stack
| OnErrorStack : ('x -> ('a,'y) task) * ('a,'y) stack -> ('a,'x) stack

type ('a,'x) process = 
{ root: ('a,'x) task 
; stack: ('a,'x) stack 
}

let rec loop : type a x. (a, x) process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step : 'x. (a, 'x) stack -> unit = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest
    in
    step proc.stack
| Fail value -> 
    let rec step : 'a. ('a, x) stack -> unit = function
    | NoStack -> ()
    | AndThenStack (_callback, rest) -> step rest
    | OnErrorStack (callback, rest) -> loop {root = callback value; stack = rest }
    in
    step proc.stack
| Binding callback -> callback (fun task -> loop {proc with root = task})
| AndThen (callback, task) -> loop {root = task; stack = AndThenStack (callback, proc.stack)}
| OnError (callback, task) -> loop {root = task; stack = OnErrorStack (callback, proc.stack)}

Caudillo

Answer 2

I think there is something incoherent in these functions. Adding some annotations and removing irrelevant branches gives:

let rec loop (type s) (proc : s process) =
  match proc.root with
  | Success value -> 
      let rec step (type t) (x : t stack) =
        match x with
        | NoStack -> ()
        | AndThenStack (callback, rest) ->
            loop {proc with root = callback value; stack = rest }
                                          (*^^^^^*)
        | OnErrorStack (callback, rest) -> step rest
      in
      step proc.stack
  | _ -> ()

where the "underlined" variable is the subject of an error message:

Error: This expression has type s but an expression was expected of type t

What is supposed to happen if the first pass through step operates on an (OnErrorStack : unit stack), and then the second pass through step operates on an (AndThenStack : int stack)?

In other words, if the argument to loop is something like:

{ root = Success ();
  stack = OnErrorStack ((fun () -> Success 3),
                        AndThenStack ((fun x -> Success (float_of_int x)),
                                      (NoStack : float stack))) }

While (value : unit) will be compatible with the first step, it seems to me that nothing guarantees its compatibility with the second step, which acts rather on a value of the existential type within the OnErrorStack (int in the counter-example).

Loiretcher

Yeah, you're right. There was a missing concept in the type definition, that once defined, cleaned everything up. – Caudillo