#9148 extension constructor printing discrepancy in REPL

[progman1]

for a type extension constructor with parameterised arguments,
REPL displayed <poly> for each as opposed to the concrete values used.
patch copies over code used for variant constructors.

[gasche]

Context for other people: the issue that details the problem is #9418.

[gasche]

The code looks sensible, thanks, but I would be reassured to see regression tests in the testsuite for this fix. Tests could be written as expect-style tests in a new file testsuite/tests/tool-toplevel/printval.ml -- see tests/tool-toplevel/use_command.ml for an example of expect-style test to reuse.

It would be nice to have first the case that is working well (non-extensible constructor), then the extensible version, and possibly an example with an extensible GADT (if you know how to write those) where there is a difference between the constructor's result type and the type declaration parameters.

[gasche]

Could this logic, which is used in several different places in the module now, be moved to its own auxiliary function?

[gasche]

Could you include a credit line with your preferred name (we have a preference for full names if you are fine with it), and potentially reviewer names?

[progman1]

Ah, the marvel of testing! I hit a snag with the GADT:
type 'a t = ..
type 'a t += T : 'a -> int t

the constructor description of the extension has its cstr_res param set to 'int' rather than a tyvar that corresponds to that in cstr_args, so I don't see how a cstr_arg can get instantiated from a ty_list member (via Ctype.apply).
Indeed this is the variant constructor treatment:
type 'a t = T: 'a -> int t
and gets the same result:
T 'x' : int t = T <poly>
I had hoped that a tydecl.type_params would have the same tyvar as the constructor's cd_args but no! ...different ids which doesn't make sense to me.

[gasche]

I am not sure from your message whether there is a problem with the new implementation or not. In your example with the extensible GADT, getting T <poly> on T 'a', as in the non-extensible case, is perfectly correct, it is the expected behavior. If this is what you observe, the test is right and there is no issue. If you observe a failure instead, we have an issue to fix in the implementation.

Other tests you could use are

type 'a t += Char : char -> int t;;
Char 'a';;

type 'a t += P : 'a * bool -> 'a t;;
P (2, true);;

type 'a t += Q : 'a -> ('a * bool) t;;
Q 2;;

those should be printed without <poly>.

The reason why <poly> is expected with T : 'a -> int t is that GADTs precisely allow to express cases where there is no relation between the type parameters of the type constructor (t) and the types of the parameters of the variant constructor (T) -- we call those existential types. If one of the parameter has an existential type, there is no static information we can extract from the whole value type, so it must be printed <poly>.

[progman1]

thanks for that explanation. then there is no problem after all.
I had imagined only

type 'a t = T: 'b -> int t

entailed an existential type in 'b

so are:

type 'a t = T: 'a -> int t
type 'a t = T: 'b -> int t
type _ t = T: 'b -> int t

equivalent?

[gasche]

Yes, in GADT constructors the type-declaration parameters are not in scope. This is why it is customary to use _ there when defining GADTs (at least when all constructors are GADT).

[gasche]

Actually, could you use type _ t += ... in the GADT-extension cases in the test?

Otherwise the code looks very nice to me now, this is good to merge if/when the CI agrees. Thanks!

[damiendoligez]

ping @gasche

[gasche]

Ah, apologies for dropping the ball on this issue. I need to rebase the PR, but hopefully it is still good to merge.