GADT docs: type variable notation inconsistency

[YawarRaza7349]

In the recently added GADT tutorial, I think it's a little confusing how the last example used the tick type variables 'inputStream and 'callback instead of the type a b. notation used in the rest of the article. I think I figured out the reason it did so. For one, the type a b. notation doesn't seem to be supported on externals, at least when I tried it in the online playground, so it couldn't have been used in the last example.

In the other direction, tick type variables couldn't work in the earlier examples because OCaml (unlike every other language 🙄) will unify the type variable with its later use to make it monomorphic.

However, this doesn't happen in the Streams example because of the module boundary. Adding a module boundary appears to remove the issue from other examples as well (one example).

You might consider changing the doc's examples to include the module boundary and use the tick type variables throughout the doc, given that, in practice, GADTs are likely to be separated by such a module boundary from their uses. In support of this claim, note that the motivating examples in the OCaml docs seem to focus on higher-rank positions (like how the Closure example puts the type a quantification on the inside, at the parameter itself), suggesting less anticipation of the monomorphization motivation.

If you do think the lack of module boundary is a common realistic scenario, and thus want to keep the examples as they are, you might still want to, in some way, address the discrepancy between the last example and the earlier ones, though you likely don't want to explain all the above esoteric minutiae. I don't personally know what you'd say instead.

Of course, the other alternative is ReScript adding support for type a b. notation to externals and then using type a b. in the last example. This also depends on whether this is more or less idiomatic than using tick type variables instead.

[fhammerschmidt]

@Josef-Thorne-A What do you think?

[Josef-Thorne-A]

I'm told that type variables in external are already universally quantified, so using the explicitly polymorphic, universally quantified syntax to them doesn't do anything. Since they can't be recursive and are opaque to the type checker, I don't think the kinds of refinement that cause issues can really happen anyways. They don't have a function body. This looks to be true as the code using on with different constructors of the GADT works irrespective of the module boundary.

I suspect that the module boundary here could be a bug, but it might not be. If I try to recreate similar behavior in OCaml, the module boundary makes no difference. It could be we are implicitly universally quantifying the type variable in ReScript only when we look at the type externally to the module.

If we have a recursive function, defining these types like this also typically necessary, whether you have the module boundary or not. I didn't go into that in the tutorial although perhaps it should be added as a footnote or a warning box.

There are a couple other ways afaict to avoid using the locally abstract type syntax. Using open polymorphic variant types as type parameters is a neat trick I frequently use but has too many gotchas to introduce in the span of an introductory tutorial.