Comment author: @gasche

Looks very reasonable to me.

Comment author: @alainfrisch

I like it too, it's very coherent with "let x : t = e" or "module X : S = E".

Comment author: @sliquister

(as a side effect of reusing the "type_constraint" nonterminal, the patch also adds the other forms { a :> int } and { a : int :> int }, which are also allowed on let bindings:

let x :> [ A | B ] = (A : [ A ]);;

val x : [ A | B ] = `A

let x : [ A ] :> [ A | B ] = A;;

val x : [ A | B ] = `A
)

Comment author: @garrigue

I have mixed feelings on this one.
On the one hand, this is coherent with the rest of the language, in particular labeled arguments.
On the other hand, records are defined, so usually there is no need for type annotations there...
Also, the patch is only for expressions. One would expect the same behavior in patterns (should be easy).

Comment author: @sliquister

You're right, I attached a new patch:

fun { contents : int } -> contents;;

• : int ref -> int =

And yes I agree type annotations are not super useful on records in general, that's why I explained why I wanted this piece of syntax. There could be cases like with references where the record is polymorphic in some fields but that's not too common.

While I was there I tried adding a type annotation before the "->" of "fun" (as mentioned in some other issue), but there is a conflict between the arrow in the construct and the one in types ("fun x : int -> int"), so I stopped there instead of figuring out how to convince the parser to reduce.

Comment author: @gasche

It's very nice of you to work on this. You should use the class 'simple_core_type' (which does not allow "foo -> bar" unparenthesized) rather than 'core_type'.

Comment author: @sliquister

Fair enough, I added it (in the same patch as the other changes but the one line could be extracted).

Comment author: @sliquister

Any chance the patch can go in, in the end?

Comment author: @gasche

Thanks for the reminder.

I think these are two separate changes that should go in two separate patches.

Besides, I would like to see the new syntax introduced exercised somewhere in the testsuite. Could you convert some, but not all, uses of (fun .. -> (x : ..)) to the new syntax (for example the one in typing-warnings/coercions.ml), and add the record syntax to tests/exotic-syntax/exotic.ml?

Comment author: @garrigue

Honestly, I'm not yet convinced of how much useful it is.
Did we have a discussion about the need to be able to write type annotations in every special compact form? Particularly when the type can actually be inferred?
For records usually the type annotation would go on the whole record, not on a specific field.

Note that some people already have preprocessors that work after type-checking, and eventually we will probably have a standard way to do that.

Comment author: @gasche

On the other hand, it serves a clearly expressed user purpose now (whereas there is no time estimation for when typedtree will be usable enough for non-experts to process), and it is a very simple patch, which does not significantly increase the complexity of the parser -- the only show-stopper would be if it added conflicts, but I assume that sliquister checked and that it did not. I would rather be in favor of merging (why not?).

I am under the impression that there is consensus that the other part of the change that sliquister included in the same patch, (fun x y : foo -> e) as a synonym of (fun x y -> (e : foo)), is very useful. At least there was in the last GADT discussion where this feature was evoked.

Comment author: @lpw25

The difference between let bindings and record field bindings frequently annoys me (the other aspect is not being able to write function field definitions like { f x = x }), so I'm in favour of this change.

It is not hugely useful, but it has a low cost and improves the consistency of the syntax.

Comment author: @sliquister

To be clear, there is no record type corresponding to the record expression. So a post-typing hook wouldn't work, since the code wouldn't type to begin with. Perhaps a hook during typing on uninterpreted extension would work, by synthetizing the record definition, but it comes with the problem of ambiguity, since not all types that unify are serialized the same way.
Not having a record type is most of the interest of the syntax extensions, since they would be one off definitions.

Comment author: @sliquister

I added the tests you suggested and split the two changes.

Comment author: @diml

For records usually the type annotation would go on the whole record, not on a specific field.

Now that type annotations are used for disambiguation I think it's useful to be able to put annotations in more places. I recently wrote some code where I put a type annotation on a specific field in a record pattern. It was possible to put the annotation on the whole record pattern but it was heavier.

On another note the syntax is already relaxed in other places that don't make sense for OCaml but might for ppx rewriters. For instance you can write "for a, b = ..." which is accepted by the parser but later rejected by the typer. This change is useful for both ppx rewriters and regular OCaml, so it's one more reason to accept it.

Unless other objections I'm planning to merge the patches.

Comment author: @gasche

Thanks!

Comment author: @diml

I merged the two patches in trunk:

26657d5
6676784