Puzzling through some GADT errors

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

1 Like

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.

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.

1 Like

Is there a syntax to cover this case ?

One must use the ordinary universal quantification in this case:

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

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.)

1 Like

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.

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.

2 Likes

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?

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>
1 Like

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.

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.

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

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'

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.

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'

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.

4 Likes

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.

1 Like

@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.

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).

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?

Not much better, but it should be enough to connect b with one occurrence.

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

It’s a fun puzzle!

  • (type b) is represented as an argument in the parse tree. So in the same way that fun x y -> r is the same as fun x -> fun y -> r, fun (type a) x -> r is also the same as fun (type a) -> fun x -> r.
  • it’s possible to annotate a fun with the return type by adding a type just before the arrow, such as fun x : string -> ""

You can combine the syntaxes: it’s possible to write the the identity function, monomorphized to ints:

fun (type a) : (int -> int) -> Fun.id

Expand the definition and you’re not far from your example:

fun (type a) : (int -> int) -> fun x -> x

Extra fun fact, you can also write:

fun (type a) -> 1

And it’s just an int.