diff --git a/docs/eager-inference-annotations-for-polymorphic-types.md b/docs/eager-inference-annotations-for-polymorphic-types.md
index 9815f03..73aace0 100644
--- a/docs/eager-inference-annotations-for-polymorphic-types.md
+++ b/docs/eager-inference-annotations-for-polymorphic-types.md
@@ -2,46 +2,50 @@
 
 ## Summary  
 
-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. 
+The RFC introduces a feature to annotate polymorphic function types to express that the first instantiation of a polymorphic type T is the one that sticks. 
 
 ## Motivation  
 
-The purpose of this feature is to prevent polymorphic types from widening into (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. 
+The purpose of this feature is to dvelop syntax to prevent polymorphic types from widening into (e.g., number | string) when a function is implicitly instantiated with different argument types. E.g., `test(1, "a")`. In the following code, Luau's current solver infers `T` to be of a union type:
 
 ```luau
 function test<T>(a: T, b: T): T
     return a
 end
 
-local result = test(1, "string") -- inferred type: number | string"
+local result = test(1, "string") -- inferred type `T`: number | string"
 ```
 
-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`.  
+This behaviour can be useful in some cases but is undesirable when a polymorphic function is intended to constrain the input types to be consistent.
 
 ## Design  
 
-We propose adding some symbol as a suffix (or prefix) that annotates the inference behaviour for the polymorphic type.
+We propose adding some symbol as a suffix (or prefix) that annotates the "eager" inference behaviour for a polymorphic type.
+Subsequent usages of type `T` where `T` is "eager" would be ignored during instantiation.
 
-### New Syntax  
+### New Syntax
 
-The `T!` syntax would would enforce an eager inference behaviour for `T`.
+The `!` syntax modifier would would enforce an eager inference behaviour for `T!`:
 
 ```luau
-function test<T!>(a: T, b: T)
+function test<T!>(a: T, b: T): T
+    return a
 end
 
-test(1, "string") -- Type error: Expected `number`, got `string`
+test(1, "string") -- TypeError: Expected `number`, got `string`
 ```
 
 ## Drawbacks  
 
 - Introduces a new syntax modifier (`T!`), which may lead to a symbol soup, but it doesn't seem too shabby next to `T?`.
+- Introduces a simple change to luau's parser, marginally increasing parsing complexity.
 
 ## 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 a uniform syntax.
+Flip the relationship being declarared per-type-parameter to per-function-argument which provides more control in expressing the inference, and could allow both instantiation behaviours of polymorphic types under a uniform syntax.
+
+A polymorphic function's arguments marked with type `T!` will not contribute to the instantiation of type `T` in the function. Instead, `T` should be inferred on the arguments without the annotation:
 
-A polymorphic function's arguments marked with type `T!` will not contribute to the instantiation of type `T` in the function. Instead, `T` should be inferred on the arguments without the annotation.
 ```luau
 function test<T>(first: T, second: T, third: T!): T
 end
@@ -49,12 +53,11 @@ end
 test(1, "string", true) -- TypeError: Type `boolean` could not be converted into `number | string`
 ```
 
-
-### 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.
+This has the added drawback that the `!` syntax modifier would need to be barred from return types, as the return type holds no relevance to implicit instantiation.
 
 
 ### Keywords
 Something like `<greedy T>` or `<strict T>` should also be considered if we want to reduce symbols. This idea has merit when considering the potential complexity of type aliases combined with `T!?`
 
-
+### Type Function Constraint
+Provide a `types.monomorphic<T>` function accessible in luau's type runtime to enforce monomorphism dynamically. This could be implemented separately at a later date.