# Explicit type binding and mutual recursion

**URL:** <https://discuss.ocaml.org/t/explicit-type-binding-and-mutual-recursion/9973>\
**Category:** Learning\
**Created:** [June 4, 2022, 3:57pm UTC](https://discuss.ocaml.org/t/explicit-type-binding-and-mutual-recursion/9973 "2022-06-04T15:57:05Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![kcrary](https://avatars.discourse-cdn.com/v4/letter/k/9fc348/32.png) [@kcrary](https://discuss.ocaml.org/u/kcrary)\
**Post date:** [June 4, 2022, 3:57pm UTC](https://discuss.ocaml.org/t/explicit-type-binding-and-mutual-recursion/9973/1 "2022-06-04T15:57:05Z")

</div>

Hello!

Explicit binding of type variables seems to interact with mutual recursion in a way I did not expect. Consider the following code:

let rec foo (type a) (x : a) : a = x  
and bar (type a) (x : a) : a = foo x

OCaml (4.10.0) gives me this error:

```
File "foo.ml", line 2, characters 35-36:
2 | and bar (type a) (x : a) : a = foo x
                                       ^
Error: This expression has type a but an expression was expected of type 'a
       The type constructor a would escape its scope
```

Is this a bug, or am I just misunderstanding how this feature is supposed to work?

Breaking the code into separate bindings fixes the problem, but that doesn’t help because my full code cannot be simplified this way.

On a related note, is this feature documented anywhere? The “(type a)” form doesn’t seem to appear in the grammar for parameters in the OCaml language document.

---

<div class="post-metadata">

**Author:** ![Gopiandcode](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/gopiandcode/32/5346_2.png) [@Gopiandcode](https://discuss.ocaml.org/u/Gopiandcode)\
**Post date:** [June 4, 2022, 4:52pm UTC](https://discuss.ocaml.org/t/explicit-type-binding-and-mutual-recursion/9973/2 "2022-06-04T16:52:51Z")

</div>

Locally abstract types are defined under: [OCaml - Language extensions](https://v2.ocaml.org/manual/locallyabstract.html)

You could try:

```auto
let rec foo : 'a . 'a -> 'a = fun (type a) (x: a) : a -> x
and bar : 'a . 'a -> 'a = fun (type a) (x: a) : a -> foo x

```

or:

```auto
let foo, bar = fun (type a) ->
  let rec foo (x: a) : a = x
  and bar (x: a) : a = foo x in
  foo, bar

```

instead, maybe.

---

<div class="post-metadata">

**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\
**Post date:** [June 4, 2022, 5:04pm UTC](https://discuss.ocaml.org/t/explicit-type-binding-and-mutual-recursion/9973/3 "2022-06-04T17:04:37Z")

</div>

For most use cases, if you want an explicit annotation for recursive function, it will be much simpler to use the `type a. ...` form:

```ocaml
let rec foo: type a. a -> a = fun x -> x
and bar: type a. a -> a = fun x -> foo x

```

This form is a shortcut for both adding an explicit universal quantified and and a corresponding locally abstract type (in other words `let f : 'a . .... = fun (type a) -> ... `).

The root issue with

```ocaml
let rec f (type a) (x:a) = f x

```

is that the locally abstract type `a` is introduced after `f`. Moreover, without an explicit type annotation, a recursive function like `f` is monomorphic in its body and a monorphic function cannot be called on a type that was defined after the function.

In other words, the issue is that in term of type scopes, the function `f` is equivalent to

```ocaml
let f = ref Fun.id
type t = A
let x = !f A

```

which also fails with

```auto
Error: This expression has type t but an expression was expected of type 'a
       The type constructor t would escape its scope

```

This is why the second solution proposed by @Gopiandcode works. Indeed, in

```ocaml
let foo, bar = fun (type a) ->
  let rec foo (x: a) : a = x
  and bar (x: a) : a = foo x in
  foo, bar

```

the type `a` is defined before the recursive functions `foo` and `bar`, thus `foo a` does not break any scope constraint.
