A second polymorphism restriction

[yallop]

The README mentions a restriction on polymorphism:

There is one subtle restriction on polymorphism: variables bound in staged programs have monomorphic types in nested [%code ...] expressions.

This specifically refers to quotation-bound variables; the restriction arises from the fact they they're lambda-bound in the translation.

There's a second restriction on polymorhpism (compared to MetaOCaml) that affects escape-bound variables, too. In MetaOCaml the following program

let x = .< fun y -> y >. in
let f = .< fun () -> .~x >. in
(f, f)

receives a type in which type variables are generalized and the type variables in two the components of the pair are distinct:

(unit -> 'a -> 'a) code * (unit -> 'b -> 'b) code =

Here's the equivalent code with ppx_stage:

let x = [%code fun y -> y ] in
let f = [%code fun () -> [%e x]] in
  (f, f)

And here's the ppx_stage type:

(unit -> '_a -> '_a) Ppx_stage.code * (unit -> '_a -> '_a) Ppx_stage.code

The loss of polymorphism this time isn't exactly due to lambda-binding in the translation, but due to the fact that splicing is translated to an application, which is not a syntactic value. The value restriction consequently applies to each splice, causing a loss of polymorphism. Here's a similar example in which the polymorphism is not lost:

let x = [%code [] ] in
let f = [%code fun () -> [%e x]] in
  (f, f)

With this example, the relaxed value restriction applies to the translated expression (since x has type 'a list code, and list is covariant), and so the expression receives a polymorphic type:

(unit -> 'a list) Ppx_stage.code * (unit -> 'b list) Ppx_stage.code

I think it would be worth mentioning this restriction in the README. Let me know if a PR would be of interest.

[stedolan]

You're right!

This is quite annoying, though. I'd much prefer if ppx_stage didn't have this restriction. The only reason it translates [%code ] to an application is to avoid accidental cross-stage-persistence: if the application were inlined, then it would be syntactically a value but values would be in scope that shouldn't be.

Still, a note for the README would be appreciated!

[yallop]

I constructed a simpler example, and submitted a patch (#5).

[yallop]

I'd much prefer if ppx_stage didn't have this restriction.

Agreed. I think avoiding this restriction, if possible, would be a valuable improvement.

[OlivierNicole]

This has been biting when playing with staged_tpf, where I really would like some splices to have polymorphic types. I also hope this restriction can be lifted.