Update eager-inference-annotations-for-polymorphic-types.md

docs/eager-inference-annotations-for-polymorphic-types.md

@@ -2,21 +2,29 @@
 
 ## Summary  
 
-Introduce a way to annotate a polymorphic function signature to express that it will only allow the first usage of a polymorphic type to interact with implicit instantiation.
+The RFC introduces a feature to annotate a polymorphic function signature to express that the first instantiation of a polymorphic type T is the one that sticks. 
 
 ## Motivation  
 
-Currently, Luau's type solver allows polymorphic types to widen into unions when they are instantiated with multiple types. For example:  
+The purpose of this feature is to prevent polymorphic types from widening into a union (e.g., number | string) when the function is called with different arguments, like in the case of `test(1, "a")`. Without the `!` annotation, the solver would infer `T` to be `number | string`, which is undesirable when the intention is to enforce strict type consistency across the function. 
 
 ```luau
 function test<T>(a: T, b: T): T
     return a
 end
 
-local result = test(1, "string") -- inferred type: 1 | "string"
+local result = test(1, "string") -- inferred type: number | string"
 ```
 
-This behaviour can be useful in some cases but is undesirable when a function is intended to enforce strict monomorphism. A monomorphic binding would prevent `T` from being instantiated with different types and instead produce a type error if `b` does not match `a`.  
+This behaviour can be useful in some cases but is undesirable when a function is intended to constrain the type to. An eager binding would prevent `T` from being instantiated with different types and instead produce a type error if `b` does not match `a`.  
+
+## Design  
+
+We propose adding some symbol as a suffix (or prefix) that annotates the inference behaviour for the polymorphic type.
+
+### New Syntax  
+
+The `T!` syntax would would enforce an eager inference behaviour for `T`.
 
 ```luau
 function test<T!>(a: T, b: T)
@@ -25,13 +33,6 @@ end
 test(1, "string") -- Type error: Expected `number`, got `string`
 ```
 
-## Design  
-
-This RFC proposes adding some symbol as a suffix (or prefix) that annotates the inference behaviour for the polymorphic type.
-
-### New Syntax  
-
-The `T!` syntax would indicate a that the type binding for `T` is monomorphic.
 
 ### Type Checking Rules  
 
@@ -41,7 +42,7 @@ The `T!` syntax would indicate a that the type binding for `T` is monomorphic.
    - If a different type is encountered, a **type error** is raised.
    - `T` will not expand into a union.
 
-2. **Behavior in Unions**  
+2. **Behaviour in Unions**  
    - A function or type with `T!` cannot instantiate `T` with a union.
    - If `T` is already a union, it must remain a union as new types cannot be added to it.
 
@@ -50,7 +51,19 @@ The `T!` syntax would indicate a that the type binding for `T` is monomorphic.
 - Introduces a new syntax modifier (`T!`), which may lead to a symbol soup, but it doesn't seem too shabby next to `T?`.
 
 ## Alternatives  
+### Function-argument-bindings
+Flip the relationship being declarared per-type-parameter to be per-argument which provides more control in expressing the inference and could allow both instantiation  behaviours of polymorphic types under an uniform syntax.
+
+A polymorphic function has arguments marked with T! will not contribute to the inference of `T`. Instead `T` should be inferred on the arguments without the annotation.
+```luau
+function test<T>(first: T!, second: T!, third: T): T
+end
+
+test(1, "string", true) -- Type error: Expected `boolean`, got `number`
+```
+### Type Function Constraint
+Provide a `types.monomorphic<T>` function in user-defined type functions to enforce monomorphism dynamically. But this would probably require some way to propagate an `*error-type*` to the user.
+### Keywords
+Something like `<greedy T>` or `<strict T>` should also be considered if we want to reduce symbols.
+
 
-- **Type Function Constraint**: Provide a `types.monomorphic<T>` function in user-defined type functions to enforce monomorphism dynamically. But this would probably require some way to propagate an `*error-type*` to the user.
-- **Keywords**: Something like `<greedy T>` or `<strict T>` should also be considered if we want to reduce symbols.
-- **Function-argument-bindings**: Flip the relationship from being declared per-type-parameter to be set per-argument:<br>`function test<T>(a: T, b: T, c: T!)` which provides the user more control, and could allow both instantiation behaviours of polymorphic types under a uniform syntax.