Puzzling through some GADT errors

[Yaron_Minsky]

I’m playing around with GADTs and running in to some puzzling errors I’m trying to understand better. Here’s a simple, working example of a function that uses GADTs as a way of controlling its return type.

module If_nothing_chosen = struct
  type (_, _) t =
    | Default_to : 'a -> ('a, 'a) t
    | Raise : ('a, 'a) t
    | Return_none : ('a, 'a option) t
end

let choose_one (type a b) test things (if_nothing_chosen : (a, b) If_nothing_chosen.t) =
  let rec loop (things : a list) : b =
    match things with
    | [] ->
      (match if_nothing_chosen with
      | Raise -> failwith "No matching item found"
      | Return_none -> None
      | Default_to x -> x)
    | thing :: rest ->
      if test thing
      then (
        match if_nothing_chosen with
        | Default_to _ -> thing
        | Raise -> thing
        | Return_none -> Some thing)
      else loop rest
  in
  loop things
;;

This compiles just fine, but if I want to define choose_one itself as a recursive function, it doesn’t compile.

let rec choose_one
    (type a b)
    (test : a -> bool)
    (things : a list)
    (if_nothing_chosen : (a, b) If_nothing_chosen.t)
    : b
  =
  match things with
  | [] ->
    (match if_nothing_chosen with
    | Raise -> failwith "No matching item found"
    | Return_none -> None
    | Default_to x -> x)
  | thing :: rest ->
    if test thing
    then (
      match if_nothing_chosen with
      | Default_to _ -> thing
      | Raise -> thing
      | Return_none -> Some thing)
    else choose_one test rest if_nothing_chosen
;;

The error message I get is:

File "src/w.ml", line 104, characters 20-24:
104 |     else choose_one test rest if_nothing_chosen
                          ^^^^
Error: This expression has type a -> bool
       but an expression was expected of type 'a
       The type constructor a would escape its scope

which I find pretty confusing! Given that there’s a recursive use of the function, I thought doing explicit polymorphic recursion might fix things, and indeed it did.

let rec choose_one : type a b. (a -> bool) -> a list -> (a, b) If_nothing_chosen.t -> b =
 fun test things if_nothing_chosen ->
  match things with
  | [] ->
    (match if_nothing_chosen with
    | Raise -> failwith "No matching item found"
    | Return_none -> None
    | Default_to x -> x)
  | thing :: rest ->
    if test thing
    then (
      match if_nothing_chosen with
      | Default_to _ -> thing
      | Raise -> thing
      | Return_none -> Some thing)
    else choose_one test rest if_nothing_chosen
;;

But I don’t really understand why it was necessary, given that the recursive call is happening at the same type. Also, I don’t fully understand why there’s a “type constructor would escape its scope” error in the first place.

y

[CraigFe]

(Disclaimer: I’m not an expert on the OCaml type system. What follows is remembered conversation from @let-def; any mistakes my own.)

Firstly, it’s worth noting that this behaviour isn’t to do with GADTs, but can apply wherever recursion and locally-abstract types mix:

let rec find (type a) (f : a -> bool) : a list -> a option = function
  | [] -> None
  | x :: xs -> if f x then Some x else find f xs
(*                                          ^
 * Error: This expression has type a -> bool
 *        but an expression was expected of type 'a
 *        The type constructor a would escape its scope
 *)

This is a particularly interesting example, because this function will be correctly typed if there are no annotations whatsoever. AFAIK, it has partly to do with the order of introduction of type bindings, and partly that OCaml’s heuristic for typing polymorphic recursion is aborted when it sees a type binder.

In the case of (type a b), the bindings for the locally abstract types occur at the term level: inside the binding for choose_one and after it has entered the typing environment. If we consider what the typing environment looks like at the moment of typing the recursive call:

let rec choose_one (type a b) test ... =
  ...
  choose_one test ...  (* HERE *)

We have something like this, from outermost to innermost bindings

• choose_one : '_choose_one (there is a symbol choose_one, with no inferred type)
• type a b (there are local types a and b)
• test : a -> bool

On observing the recursive call, we attempt to unify '_choose_one with (a -> bool) -> _. However, a was introduced after choose_one: if we complete this unification then we end up with choose_one : (a -> bool) -> '_rest, where a is not yet bound. a would escape its scope! So we reject the program for this reason.

If we add an explicitly-polymorphic type annotation, we fix the problem by letting the type-checker take a fresh instance of the polymorphic variable in order to type the recursive call:

let rec choose_one : 'a 'b. ('a -> bool) -> ... =
  fun (type a b) test ... ->
    ...
    choose_one test ...  (* HERE *)

(This variation is what the type a b. syntax expands to. The expaded form is a little clearer here at showing that this syntax introduces both type-level type bindings and term level type bindings.)

This time around, we get a typing environment that looks like:

• choose_one : 'a. 'b. ('a -> bool) -> .... (No need to approximate the type, as it’s been given directly.)
• type a b
• test : a -> bool (Don’t need to take an instance of the outer polymorphic constraint: we can propagate the abstract type specification directly.)

Now the unification implied by the recursive call succeeds: we can lookup choose_one in the type environment and instantiate a fresh instance with the specific abstract type a, without a escaping its scope.

[Yaron_Minsky]

Hmm. I think I roughly understand the description here, but it’s pretty unsatisfying. It feels very implementation driven, and I’m not sure how to tell someone how to know which annotations will work and which won’t.

I’m curious if anyone knows if this is a case where there are plans to make this simpler and more intuitive by improving the type inference, or if this is kind of as good as it gets.

y

[EduardoRFS]

I feel like there is no principal way to allow your code tho, as let rec f p = f p is just sugar to let rec f = fun p -> f p, which makes the problem a lot clearer.

A principal’ish way that I could think of is let v = (expr: typ) being a special case where we look a head and improve the type constraint, and make so that fun (a: int) -> a is actually sugar to (fun a -> a): int -> _. This would solve the problem, and it’s possible to even transform the let v: typ = expr be sugar to let v = (expr: typ), making it slightly more principal the let case is a Ppat_constraint.

Not sure if we do this kind of “lookahead” at any point in the typer, but it’s definitely not hard to implement, besides breaking a lot of PPX or making the AST be redundant.

edit:

After checking code, type_approx is already a thing so we do the lookahead, I wonder why it’s not handling this case then, still trying to implement it.

edit2:

Was able to infer the type correctly, just need to clean a bit to ensure that the level + scope is all right.

edit3:

Will try to ensure that everything is working, I broke some warnings, and if I can do it, will open a PR. Mostly do basic approximation of patterns, and add approximation of pexp_newtype.

[octachron]

@Yaron_Minsky

ow to tell someone how to know which annotations will work and which won’t.

One solution is to always use let rec f: type x y ... which works in most cases, and consider that (type a b) is only useful for showing off one understanding of the precise typing rule of the OCaml typechecker. With this type a ... . ... syntax, the only corner case which is not covered by this syntax is universal quantification over row type variables.

[EmileTrotignon]

Is there a syntax to cover this case ?

[octachron]

One must use the ordinary universal quantification in this case:

let rec f: 'a. ([> `X] as 'a) -> unit = function
  | `X -> f `Y
  | _ -> ()

[gasche]

Not exactly what you are asking for, but @Octachron wrote an excellent chapter on GADTs in the OCaml manual, which could be recommended to people starting GADT programming. It explains why recursive functions on GADT need “explicit polymorphic annotations” in less “implementation driven” terms.

(The chapter also demonstrates the new naming scheme for existential type variables introduced by GADT constructors, which can help a lot working through type errors, but are still a bit heavy and deserve a gentle introduction.)

[octachron]

I have only written the nomenclature part and a bit of the explanation for recursive functions in this chapter, @garrigue is the author of most of this chapter.

[garrigue]

I see lots of good replies. This essentially boils down to: if you want to use both GADT refinement and recursion, use type a. .... annotations.
Actually, I would even suggest to use them for all functions involving GADTs, as both the notation and behavior are more intuitive.

As for why (type a) doesn’t play well with recursion, @CraigFe is basically correct, except that there are no heuristics involved. Namely polymorphic recursion in OCaml is always explicit, using either annotations of the form 'a. ... or type a. ... (the latter being actually syntactic sugar for the former). Using (type a) with normal (monomorphic) recursion is bound to fail because it tries to unify the internal type a, which is a locally abstract type, with the external type, which is a type variable outside of the scope of a, hence the error.

[EduardoRFS]

Any particular reason we couldn’t have a better type approximation from it? Seems explicitly enough to me that
fun (type a) (f: a t): a -> would always have the same signature as 'a. 'a t -> 'a.

Is that wrong?

[garrigue]

FIrst, to clarify, there is no connection between (type a) and 'a. ..., and 'a. 'a t -> 'a can only be used on let-definitions, so what you must be asking for is that let g (type a) (f : a t) : a = ... be interpreted as let g : type a. a t -> a = fun f -> ...

While this is certainly doable, this would be a pain to implement: one has to collect all the components of the type from separate annotations, and redo all the processing after that.

Moreover this creates the question of where we stop. If this is accepted when all annotations are provided, then people would start asking why
let g (type a) (f : a t) = ... is not interpreted as
let g : type a. a t -> _ = fun f -> ...
which creates the question of whether this interpretation would not break backward compatibility.
And people might even ask for more exotic stuff where it is no longer trivial to see which annotations participate to the definition.

The advantage of the current approach is precisely that we don’t play heuristics: we are not reusing an existing syntax to do something else, but introduce a new syntax that does something specific.

By the way, there are indeed situations where (type a) does not create a polymorphic type:

let f : int -> int = fun (type a) (x : a) : a -> x;;
val f : int -> int = <fun>

[garrigue]

I could easily find an example that types with the original annotation, but breaks if we combine it:

let g (type a) (x : a) : _ = x;;
val g : 'a -> 'a = <fun>
let g : type a. a -> _ = fun x -> x;;
Error: This definition has type 'b -> 'b which is less general than
         'a. 'a -> 'c

So, we could only do this transformation when the combined annotation is closed, i.e. contains no unification variable. We do that for subtyping, but I’m afraid that here this would just add to the confusion.

[EduardoRFS]

@garrigue

By the way, there are indeed situations where (type a) does not create a polymorphic type:

let f : int -> int = fun (type a) (x : a) : a -> x;;
(* is essentially *)
let f = fun (type a) (x: a): a -> x;;
let f: int -> int = f

Which seems to me that It creates a polymorphic type you’re just constraining it in sequence.

@garrigue

I could easily find an example that types with the original annotation, but breaks if we combine it:

Oh, good job on this, it definitely shows that my transformation doesn’t work for all cases, so I will try to understand, why is that the case? From what I understand is because 'a cannot be unified with 'c' which doesn’t make a ton of sense in my head and is probably related to how this Tpoly stuff works.

But even then, on my current implementation which I believe to not be sound, the following works as the approximation added is the generalized one, so it’s not fully equivalent to 'a. 'a -> _ but more like 'a -> _, where 'a is generalized and _ is not, my assumption is that is safe as it is safe to allows unify 'a _ to work.

And the only change made here is improving the type approximation. to approximate the following type.

let rec id (type a) (x: a): _ =
  let x' = id x in
  assert (x = x');
  x

[garrigue]

I’m not sure I understand what you are doing, but to me it looks like it’s potentially unsound.
If you assume that the type of id is 'a -> _ with 'a generalized (which I would certainly write 'a. 'a -> _, but you seem to make a distinction), then it means that occurrences of id in the body ignore the type of their argument. Wouldn’t then the following function be accepted in your system?

let rec id (type a) (x: a): _ =
  let x' = id 1 in
  ignore (x = x');
  x'

[EduardoRFS]

@garrigue

but you seem to make a distinction

Mostly because I see 'a. 'a -> _ as a Tpoly('a → _) which doesn’t unify with 'a -> _. Will use the '_weak convention for weak vars so that it’s clear.

@garrigue

Wouldn’t then the following function be accepted

At first my thought was that it should be allowed as this function is infinitely recursive, but this function is rejected, which is also nice.

As _ is a weak variable introduced by the approximation, the following is how this function that you sent will be typed, it will be rejected on the ignore (x = x') as otherwise a would escape its scope.

(* this reference was added just to have a weak variable *)
let v = ref (assert false)
(* this is the approximated type, 'a -> '_weak *)
let id_approx (type a) (x: a): _ = !v
let id (type a) (x: a): _ =
  let x' = id_approx 1 in
  ignore (x = x');
  x'

[ivg]

@Yaron_Minsky

Also, I don’t fully understand why there’s a “type constructor would escape its scope” error in the first place.

There is an excellent post by Oleg Kiselyov, which I personally found very insightful in understanding the scope part of the error. It will also answer why is recursion another scope.

In summary, the main idea is that types in OCaml have a lifetime much like the values (indeed OCaml can create new types in runtime). And to ensure soundness we have to guarantee that no value can outlive its type, i.e., imagine if we have a value that has no type - unsoundness. Besides, the simplest example, that doesn’t involve any GADT is,

let x = ref None
type t = T
let () = x := Some T

Functions and let expressions, all create scopes for types. And if the type is created inside of the function and there is a value that somehow escapes out of the scope of this function (either via a closure a directly as the returned value) that is unified with this local to the function type, then we have the soundness breach. The only option is to guarantee that the type existed before the application of the function, i.e., to unify the type with a parameter (because OCaml is strict and the value has to exist before the application and if the value exists then it has type). That is why we need a locally abstract type, which we can unify with some of the input parameters.

Finally, the recursive part. Each invocation of a function, recursive or not, creates a new scope, so we have to prove that values from the inner scope do not escape to the outer scope (via unification). The easiest option is to disjoin them by annotating them as explicitly polymorphic.

With that said, I believe that the reference to scope in the error message is confusing, as it refers to a notion that is not really defined in the manual and neither is a part of the programmer’s common knowledge. Yes, we commonly know about the scope of variables, but not that types also have scopes and that those scopes could be dynamic. So this error message is a leaking abstraction of the type checker implementation.

[ivg]

@Yaron_Minsky

Error: This expression has type a -> bool
       but an expression was expected of type 'a
       The type constructor a would escape its scope

Also, I wasn’t able to reproduce this error message in the range of OCaml compilers starting from 4.09 til 4.13~alpha, all of them report,

This expression has type 'a but an expression was expected of type b
The type constructor b would escape its scope

So there is no unification between the test and the thing.

[EduardoRFS]

@garrigue I believe the following code is close to the idea, it’s just a piece of code hacked together as essentially I wanted a instance_poly but in place.

this code is bad, but hopefully sound?

It can type the example that started this thread and also fails to type all the unsound examples that you sent to me up to now.

It also rejects the example that I gave, so effectively any usage of the local type variable needs to be explicitly annotated as always but at least the syntax for named parameters is not terrible.

(* fails *)
let rec id (type a) (x: a): _ = ...

I believe the implementation is unsound because the way it set the levels of everything, but there is anything fundamentally unsound on the idea?

It is essentially improving the type approximation and dealing with the problem that the pattern will be typed as '_a and the approximation will be 'a -> 'a but when unified with '_a it leads to '_a -> '_a which seems just an artifact and nothing meaningful as in reality the ident is not constraining the type at all, so in this code I fix the variables levels and the types levels to generic which definitely leads to bugs(as it fails even to compile the stdlib fully).

[viritrilbia]

@octachron

With this type a ... . ... syntax, the only corner case which is not covered by this syntax is universal quantification over row type variables.

@octachron

One must use the ordinary universal quantification in this case

I recently had a situation where one function was universally quantified over multiple types, some of which were row type variables and others of which needed to be locally abstract. I wanted to write something like 'a. type b. but OCaml wouldn’t accept it (I guess only one dot is allowed?). The only way I was able to figure out to annotate such a function was to manually expand out what the manual says the type a. syntax is automatically expanded into. This required the type of the function to be written twice, once with the locally abstract type quoted and once not:

let f : 'a 'b. ([> `Foo] as 'a) -> 'b -> 'a * 'b =
  fun (type b) -> 
  (fun x y -> (x,y) 
    : ([> `Foo] as 'a) -> b -> 'a * b);;

Ocamlformat then rewrote this into

let f : 'a 'b. ([> `Foo ] as 'a) -> 'b -> 'a * 'b =
  fun (type b) : (([> `Foo ] as 'a) -> b -> 'a * b) -> fun x y -> (x, y)

which also compiles, but which I find even more puzzling to parse in my head (why does the type of the function come after the fun (type b) but before the -> ?).

Is there a better way to annotate the type of such a function?