Explicit type binding and mutual recursion

Learning
1

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.

2

Locally abstract types are defined under: OCaml - Language extensions

You could try:

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:

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.

3

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

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

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

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

which also fails with

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

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.

3 Likes