Skip to content

Fix bug in untypeast/pprintast for value bindings with polymorphic type annotations - #13845

Merged
Octachron merged 4 commits into
ocaml:trunkfrom
ccasin:untypeast-pprintast-polytype
Mar 5, 2025
Merged

Octachron merged 4 commits into
ocaml:trunkfrom
ccasin:untypeast-pprintast-polytype

Conversation

@ccasin

@ccasin ccasin commented Mar 4, 2025 •

Copy link
Copy Markdown
Contributor

It is expected that you can get back a valid source program if you typecheck a program, then run untypeast on the resulting typedtree, then print it with pprintast (see tests of this in testsuite/tests/compiler-libs/test_untypeast.ml). However, this does not work for the following expression:

let foo : 'a. 'a -> 'a = fun x -> x in foo

The issue is that untypeast turns the pattern in the let binding into a Ppat_constraint node, rather than putting the type annotation in the pvb_constraint field. As a result, this invalid syntax is printed:

let (foo : 'a . 'a -> 'a) = fun x -> x in foo

This PR has two commits. The first demonstrates this issue by adding this testcase to test_untypeast.ml. The second fixes it, by simply having untypeast check whether the pattern in a value binding is a Ppat_constraint, and moving the type annotation to the pvb_constraint field in that case.

Comment thread typing/untypeast.ml Outdated
let pat = sub.pat sub vb.vb_pat in
let pat, value_constraint =
match pat.ppat_desc with
| Ppat_constraint (pat, cty) ->

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would suggest to apply this transformation only in the Ptyp_poly case to make the parsetree -> typedtree -> parsetree transformation idempotent. Otherwise, we are duplicating the constraint on the expression side.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Makes sense - I've specialized the case to apply only when cty is a Ptyp_poly.

(***********************************)
(* Untypeast/pprintast correctly handle value binding type annotations. *)

run {| let foo : 'a. 'a -> 'a = fun x -> x in foo |};;

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The parser also supports let foo : type a . a -> a = fun x -> x, does this work as expected?

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This syntax is elaborated in Typecore to

let (foo: 'a. 'a -> 'a) = fun (type a) -> ( (fun x -> x) : 'a -> 'a)

and it is thus is similar to the first form in the typedtree.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've added this example as a test case. It prints as @Octachron predicts.

@Octachron Octachron left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the fix!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants