# Polymorphic Recursive Type Errors

**URL:** <https://discuss.ocaml.org/t/polymorphic-recursive-type-errors/2058>\
**Category:** Learning\
**Created:** [May 29, 2018, 2:56pm UTC](https://discuss.ocaml.org/t/polymorphic-recursive-type-errors/2058 "2018-05-29T14:56:39Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![Erik\_Lott](https://avatars.discourse-cdn.com/v4/letter/e/aeb1de/32.png) [@Erik\_Lott](https://discuss.ocaml.org/u/Erik_Lott)\
**Post date:** [May 29, 2018, 2:56pm UTC](https://discuss.ocaml.org/t/polymorphic-recursive-type-errors/2058/1 "2018-05-29T14:56:39Z")

</div>

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

```

I’ve only been working in OCaml for a few months now, and 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 for evaluating the GADT types. I haven’t had any luck using a helper type to solve this issue, so I’m starting to wonder if I’m attempting to do something impossible with the type system.

Can anyone shed light on this error? Many Thanks!

---

<div class="post-metadata">

**Author:** ![c-cube](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/c-cube/32/1727_2.png) [@c-cube](https://discuss.ocaml.org/u/c-cube)\
**Post date:** [May 29, 2018, 3:11pm UTC](https://discuss.ocaml.org/t/polymorphic-recursive-type-errors/2058/2 "2018-05-29T15:11:29Z")

</div>

You may need to annotate `step` with a universal type such as `type a. a stack -> something`.

---

<div class="post-metadata">

**Author:** ![schrodibear](https://avatars.discourse-cdn.com/v4/letter/s/958977/32.png) [@schrodibear](https://discuss.ocaml.org/u/schrodibear)\
**Post date:** [May 29, 2018, 4:12pm UTC](https://discuss.ocaml.org/t/polymorphic-recursive-type-errors/2058/3 "2018-05-29T16:12:02Z")

</div>

I tried to succeed with the example and it seems the error is not spurious, mere type annotations won’t help and you need to change the type definitions to consider success and error result types separately:

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

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

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

let rec loop : type a b. (a, b) process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step : 'b. (a, 'b) 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, b) 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)};;

```

Example usage (as I understand it from the code):

```ocaml
loop {root =
        AndThen ((fun s ->
                    Printf.eprintf "I finished with %s!\n" s;
                    Success ()),
        OnError ((fun s ->
                    Printf.eprintf "Error: %s\n" s;
                    Success "error"),
        AndThen ((fun i ->
                    Printf.eprintf "Success: %d\n" i;
                    Success "success"),
        Binding (fun cnt ->
                      cnt
                      (AndThen
                        ((fun i ->
                          if i <= 0 then Fail (string_of_int i)
                                      else Success (i - 1)),
        Success ~-1))))));
        stack = NoStack };;
loop {root = AndThen ((fun s -> Printf.eprintf "I finished with %s!\n" s; Success ()), OnError ((fun s -> Printf.eprintf "Error: %s\n" s; Success "error"), AndThen ((fun i -> Printf.eprintf "Success: %d\n" i; Success "success"), Binding (fun cnt -> cnt (AndThen ((fun i -> if i <= 0 then Fail (string_of_int i) else Success (i - 1)), Success ~-1)))))); stack = NoStack };;

```

---

<div class="post-metadata">

**Author:** ![Erik\_Lott](https://avatars.discourse-cdn.com/v4/letter/e/aeb1de/32.png) [@Erik\_Lott](https://discuss.ocaml.org/u/Erik_Lott)\
**Post date:** [May 29, 2018, 5:14pm UTC](https://discuss.ocaml.org/t/polymorphic-recursive-type-errors/2058/4 "2018-05-29T17:14:32Z")

</div>

> [@schrodibear](#):
>
> | Fail value -\> let rec step : 'a. ('a, b) stack -\> unit = function | NoStack -\> () | AndThenStack (\_callback, rest) -\> step rest | OnErrorStack (callback, rest) -\> loop {root = callback value; stack = rest } in step proc.stack

Amazing. I actually have a full example with 2 variable types (type (a,x) task), but I was still getting errors , so I wasn’t sure if it was the right direction.

These annotations…

```
let rec loop : type a x. (a, x) process -> unit = fun proc ->...

let rec step : 'x. (a, 'x) stack -> unit = function...

let rec step : 'a. ('a, x) stack -> unit = function...

```

… clearly describe what is happening in those recursive functions, but I can’t say I would have come to those annotation on my own. While I was digging around the web searching for solutions, I got the impression that the following 2 annotations could be used interchangeably, which is clearly not the case.

```
    let rec loop : type a x. (a, x) process -> ....

    let rec loop : 'a 'x. ('a, 'x) process -> ....

```

Now I see exactly what is going on, and how these types are being used. Thank You!

---

<div class="post-metadata">

**Author:** ![schrodibear](https://avatars.discourse-cdn.com/v4/letter/s/958977/32.png) [@schrodibear](https://discuss.ocaml.org/u/schrodibear)\
**Post date:** [May 29, 2018, 6:38pm UTC](https://discuss.ocaml.org/t/polymorphic-recursive-type-errors/2058/5 "2018-05-29T18:38:37Z")

</div>

Actually in this particular case the annotations can indeed be used interchangeably:

```ocaml
let rec loop : 'a 'b. ('a, 'b) process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step : 'b. (_, 'b) 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, _) 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)};;

```

This is also typechecked without error.  
In general, the difference is that the “rigid”, or locally abstract type (`type a`) is refined _separately in each branch_ of a match on the annotated value, but the polymorphic type annotation (`'a.`) only allows to use the annotated function polymorphically in its own body. For example:

```ocaml
type _ t = A : int * 'a t -> < k : int * 'a > t | B : string * 'b t-> < k : string * 'b> t;;
let rec cycle = A (1, B ("2", cycle));;
let rec print : 'a. 'a t -> unit =
  function
  | A (i, t) -> Printf.eprintf "%d" i; print t
  | B (s, t) -> Printf.eprintf "%s" s; print t;;

```

Will give an error, because the types in different branches cannot be unified. Using a local abstract type fixes this:

```ocaml
let rec print =
  fun (type a) ->
  function
  | (A (i, t) : a t) -> Printf.eprintf "%d" i; print t
  | (B (s, t) : a t) -> Printf.eprintf "%s" s; print t;;

```

But now the existential type from the branch escapes into the type of the function because of lack of polymorphism. So in this example both annotations are needed:

```ocaml
let rec print : 'a. 'a t -> _ =
  fun (type a) ->
  function
  | (A (i, t) : a t) -> Printf.eprintf "%d" i; print t
  | (B (s, t) : a t) -> Printf.eprintf "%s" s; print t;;

```

The form `type a.` is just a shortcut for this combination (see [section on polymorphic syntax](http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec242)), so the above is equivalent to:

```ocaml
let rec print : type a. a t -> _ =
  function
  | A (i, t) -> Printf.eprintf "%d" i; print t
  | B (s, t) -> Printf.eprintf "%s" s; print t;;

```

There is also one tricky issue explained [here](https://caml.inria.fr/mantis/view.php?id=7483). It’s the reason why the following:

```ocaml
let rec loop : 'a 'b. ('a, 'b) process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step : 'b. ('a, 'b) 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, 'b) 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)};;

```

gives very surprising error message about less general type. To put it shortly, the two _different_ unification variables named `'a` here have different scopes, and the scope of the second (in `('a, 'b) stack)`) variable starts _earlier_ than the scope of the first (in `'a 'b. ('a, 'b) process`). The error message says nothing about the scope and so looks confusing.

---

<div class="post-metadata">

**Author:** ![Erik\_Lott](https://avatars.discourse-cdn.com/v4/letter/e/aeb1de/32.png) [@Erik\_Lott](https://discuss.ocaml.org/u/Erik_Lott)\
**Post date:** [June 1, 2018, 7:52pm UTC](https://discuss.ocaml.org/t/polymorphic-recursive-type-errors/2058/6 "2018-06-01T19:52:55Z")

</div>

I’ve used your examples so many times in the past few days that I’ve actually made a note to come back and thank you again for your explanation. If only all of the document explained concepts as clearly as this…

Huge thumbs-up.