# Equal existential types are not printed equally by the top-level?

Below is a small interaction with the top-level.

• Fisrt define a witness for the integer type.
• Then define the type for dynamically typed values.
• Next provide a dynamically typed integer for evaluation.
``````# type _ ty = Int : int ty;;
# type dyn = Dyn : 'a ty * 'a -> dyn;;
# Dyn (Int, 3);;
- : dyn = Dyn (Int, <poly>)
``````

The constructor `Dyn` has one existential type that occurs twice, as`'a` in `'a ty * 'a`. Why the top-level prints `Int` but fails to print `3`?

`'a ty` and `'a` are not at all the same types! You cannot show anything about a value of type `'a` without knowing the type. On the other hand, with your current definition of `'a ty`, you don’t need to know `'a` to print the values of type `'a ty`. If you had, say,

``````type 'a ty = Int : int ty | Weird : 'a list -> 'a ty
``````

then printing `Dyn (Weird [2; 3], 4)` would probably show something like `Weird [<poly>; <poly>]` in the first argument.

It seems that the top-level does not do any type inference before printing. Otherwise, when printing `Dyn(Int, 3)` it would first determine that the first argument of `Dyn` is `Int`, which has type `int ty`; then from the type of `Dyn` it infers that the second argument of `Dyn` has type `int`.

The toplevel performs a limited form of type inference, propagating type information from a constructor to each of its argument – a simple form of (bi)directional type inference. Your idea requires a more sophisticated form of inference indeed.

How would it work in the case `Dyn : 'a * 'a ty -> dyn`, where the type-information-providing tag comes after the value? I guess one could first traverse the value in full, to compute a (bottom-up) type derivation with general unification, and then print it.

This sounds doable, but also a complex change to the printing logic. Is there evidence that this is important in practice?

A complex printer may not be that important.

My question arose when I was testing functions that process dynamically typed values (e.g. convert between a dynamic product and a list of dynamic values that are the product entries).

I use the top level to observe the result of these functions. Although the printer does not print existential types as expected, I can still do my test in other ways, such as using polymorphic comparison (=) to check if the function output is structurally equal to the expected value, instead of printing the output on the top-level and see if it is the expected value.