Clarify docs

Author: josevalim

lib/elixir/pages/references/gradual-set-theoretic-types.md

@@ -90,17 +90,9 @@ Inferring type signatures comes with a series of trade-offs:
 
   * Cascading errors - when a user accidentally makes type errors or the code has conflicting assumptions, type inference may lead to less clear error messages as the type system tries to reconcile diverging type assumptions across code paths.
 
-On the other hand, type inference offers the benefit of enabling type checking for functions and codebases without requiring the user to add type annotations. To balance these trade-offs, Elixir’s type system provides the following type reconstruction capabilities:
+On the other hand, type inference offers the benefit of enabling type checking for functions and codebases without requiring the user to add type annotations. To balance these trade-offs, Elixir performs module-local inference: the arguments, returns types, and all variables in a function are computed considering all of the function calls to the same module and to Elixir's standard library. Any call to a function in another module is conservatively assumed to return `dynamic()` during inference. Our goal is to provide an efficient type reconstruction algorithm that can detect definite bugs in dynamic codebases, even in the absence of explicit type annotations.
 
-  * Local type inference - the type system automatically infer the types of variables, at the place those variables are defined.
-
-  * Type inference of patterns (and guards in future releases) - the argument types of a function are automatically inferred based on patterns and guards, which capture and narrow types based on common Elixir constructs.
-
-  * Module-local inference of return types - the gradual return types of functions are computed considering all of the functions within the module itself. Any call to a function in another module is conservatively assumed to return `dynamic()` during inference.
-
-The last two items offer gradual reconstruction of type signatures. Our goal is to provide an efficient type reconstruction algorithm that can detect definite bugs in dynamic codebases, even in the absence of explicit type annotations. The gradual system focuses on proving cases where all combinations of a type *will* fail, rather than issuing warnings for cases where some combinations *might* error.
-
-Once Elixir introduces typed function signatures (see "Roadmap"), any function with an explicit type signature will be checked against the user-provided type, as in other statically typed languages, without performing type inference of the function signature.
+The gradual system focuses on proving cases where all combinations of a type *will* fail, rather than issuing warnings for cases where some combinations *might* error. Once Elixir introduces typed function signatures (see "Roadmap"), any function with an explicit type signature will be checked against the user-provided type, as in other statically typed languages, without performing type inference.
 
 ## Roadmap