Thanks for this perspctive, and I have been re-thinking about it also. I wonder if the following is a correct way to phrase it (maybe not formally correct, but let me try):
There exist different classes of “variable types”:
- A type variable
'tthat may be replaced by type inference once during compilation with a concrete type or, if not replaced, will be polymorphic. - A weak type variable
'_weak1, which must be replaced by type inference once during compilation with a concrete type. - A quantified type variable
't. 't, which cannot be replaced by type inference and is always polymorphic. - An abstract type
type tor locally abstract type(type t) tthat can be replaced with multiple different types depending on context (usingwith type t = xor pattern matching, respectively). Locally abstract types may also be replaced (once and forever) by type inference with a concrete type (which is a different mechanism) or be polymorphic (like't). - The combination of a quantified type variable with locally abstract types:
A locally abstract type with a polymorphic annotationtype t. t, that can be replaced with multiple different types depending on context when used, like(type t) t, but behaves as polymorphic to the caller of the function, like't. 't. i.e. it cannot be replaced by the type inference mechanism with a single type for all cases.
Did I get this (more or less) right?
Well, if I understand things right, then (type a) allows type inference to replace a with a single type or allow it to be polymorphic:
'tmay be polymorphic'_weak1cannot be polymorphic't. 'tis always polymorphic(type t) tmay be polymorphictype t. tis always polymorphic
Sometimes the compiler needs to know that it is forbidden to apply type inference, which is why you need the explicit 't. or type .t quantifications (examples given in section “Explicitly polymorphic annotations” as also linked in my OP).
If I understand right, then this would mean treating 't. 't the same way as type t. t?