Remove strict mode from documentation

Summary:
Remove all mentions of modes in documentation.
Update `eqwalizer:dynamic()` to `dynamic()`.

Some explanations about bounded dynamic should be added later, tracking here T196497521.

Reviewed By: ilya-klyuchnikov

Differential Revision: D60036860

fbshipit-source-id: b02f46ea83dec23ffaf777f0b276368836356da1

Author: VLanvin

docs/reference.md

@@ -2,7 +2,7 @@
 
 - ### [Syntax of types and specs in eqWAlizer](./reference/types.md)
 
-- ### [Gradual and strict modes](./reference/modes.md)
+- ### [Gradual typing](./reference/gradual.md)
 
 - ### [Narrowing and occurrence typing](./reference/narrowing.md)
 

docs/reference/advanced.md

@@ -92,13 +92,8 @@ eqWAlizer in most settings. For example, consider the following code:
 apply_neg(B) -> negb(B).
 ```
 Since `B` has type `boolean()`, eqWAlizer cannot decide which sub-spec of
-`negb` to use to decide the type of `negb(B)`. Its behaviour depends on
-which setting is in use:
-
-- in strict mode, eqWAlizer will report an error stating it does not have
-enough info to branch;
-- in gradual mode, eqWAlizer will simply assume type `eqwalizer:dynamic()`
-for the result of `negb(B)`, disregarding the spec.
+`negb` to use to decide the type of `negb(B)`. eqWAlizer will simply assume
+type `eqwalizer:dynamic()` for the result of `negb(B)`, disregarding the spec.
 
 Hence, to get better signal in this case, `negb` should simply be
 specced as `(boolean()) -> boolean()`.
@@ -151,11 +146,6 @@ or not meant for casual use. They can be enabled by setting the corresponding
 environment variable when calling `elp eqwalize`, e.g.,
 `EQWALIZER_CHECK_REDUNDANT_GUARDS=1 elp eqwalize-all`.
 
-### Gradual and strict mode
-
-Enable strict mode with `EQWALIZER_GRADUAL_TYPING=false`. By default, eqWAlizer
-uses gradual mode. See [gradual and strict typing modes](./modes.md).
-
 ### Occurrence typing
 
 Disable occurrence typing with `EQWALIZER_EQWATER=false`. By default, eqWAlizer

docs/reference/escape.md

@@ -4,11 +4,11 @@ To make eqWAlizer adoption practical, it features several mechanisms to make
 the type checker less strict, or to bypass it entirely.
 
 
-### Type `eqwalizer:dynamic()`
+### Type `dynamic()`
 
-Gradual mode and the type `eqwalizer:dynamic()` (provided in app `eqwalizer_support`
+The built-in type `dynamic()` as well as `eqwalizer:dynamic/1` (provided in app `eqwalizer_support`
 for the open source release) are a good way to make the type-checker more lenient
-while still providing some signal. See [gradual and strict modes](./modes.md).
+while still providing some signal. See [gradual typing](./gradual.md).
 
 
 ### Ignoring errors for a function completely

docs/reference/generics.md

@@ -135,7 +135,7 @@ Reversed = lists:foldl(Lambda, [], [1, 2, 3])
 ```
 In such a setting, eqWAlizer will not be able to use information such as the
 spec of `foldl` to infer the type of `Lambda`, and will perform much more
-optimistic type-checking. In gradual mode, it will simply assume for `Lambda`
+optimistic type-checking. It will simply assume for `Lambda`
 the type `(dynamic(), dynamic()) -> dynamic()`. Therefore, the type-checking
 of `foldl` will be very optimistic, and eqWAlizer will deduce for `Reversed`
 the type `dynamic()`, which is much less precise than `[number()]`.

docs/reference/modes.md docs/reference/gradual.md

@@ -1,21 +1,18 @@
-# Gradual and strict typing modes
+# Gradual typing
 
-EqWAlizer features two different modes: gradual mode, and strict mode. They differ in how
-unannotated functions are handled, and how the builtin constant `eqwalizer:dynamic()` behaves.
-Strict mode offer stronger type-checking guarantees, while gradual mode favours ease-of-use
-and better signal-to-noise.
-Strict mode is kept sound, however, current development of eqWAlizer focuses on optimising for
-gradual mode. The current distribution of eqWAlizer uses gradual mode by default.
+EqWAlizer features gradual typing, a typing discipline built on type `dynamic()`,
+that allows smooth migration of untyped code to typed code, and precise management
+of the signal-to-noise ratio of type errors.
 
 
-### Type `eqwalizer:dynamic()`
+### Type `dynamic()`
 
-`eqwalizer:dynamic()` (later abbreviated to `dynamic()`) is a special type which,
-in gradual mode, "slips through the fingers" of the type-checker. It is similar to
+Erlang's built-in type `dynamic()` is considered by eqWAlizer as a special type which
+"slips through the fingers" of the type-checker. It is similar to
 [any in TypeScript](https://www.typescriptlang.org/docs/handbook/basic-types.html#any),
 [dynamic in Hack](https://docs.hhvm.com/hack/built-in-types/dynamic),
 [untyped in Sorbet](https://sorbet.org/docs/untyped).
-Formally, in gradual mode, `dynamic()` is compatible with every type (and, conversely,
+Formally, `dynamic()` is compatible with every type (and, conversely,
 every type is compatible with `dynamic()`). This
 means that a function that expects an argument of type `dynamic()` can be used with any
 value, and a result of type `dynamic()` can be used anywhere.
@@ -27,35 +24,23 @@ This value can in particular be passed to a function expecting, say, an argument
 `{integer(), boolean()}`, but not to a function expecting an argument of type
 `{integer(), boolean(), atom()}`.
 
-In strict mode, eqWAlizer considers `dynamic()` to be equivalent to `term()`. This is a
-completely different, stricter, behaviour. In strict mode, a function that accepts arguments
-of type `dynamic()` is considered by eqWAlizer as accepting arguments of type `term()`. Hence,
-this function can be applied to values of any type, which is basically the same behaviour as in
-gradual mode. However, in strict mode, a value of type `dynamic()` **cannot** be used in every
-context. It can only be used in contexts expecting a value of type `term()`, since
-the only supertype of `dynamic()` in strict mode is `term()`. As an example, consider the
-following function:
+As an example, consider the following function:
 ```Erlang
--spec dyn_to_int(eqwalizer:dynamic()) -> integer().
+-spec dyn_to_int(dynamic()) -> integer().
 dyn_to_int(X) -> X.
 ```
-This function is accepted by eqWAlizer in gradual mode: `X` is of type `eqwalizer:dynamic()`
-which, in gradual mode, is compatible with every type, in particular `integer()`. However, in
-strict mode, `X` is considered to be of type `term()` which is not compatible with `integer()`.
+This function is accepted by eqWAlizer: `X` is of type `dynamic()`
+which is compatible with every type, in particular `integer()`.
 
-The type `eqwalizer:dynamic()` is provided in the module `eqwalizer.erl`, which should be
-made available during analysis. This module is present in the open-source library
-[eqwalizer_support](https://github.com/WhatsApp/eqwalizer/tree/main/eqwalizer_support).
 
-
-### Using `eqwalizer:dynamic()` in gradual mode
+### Using `dynamic()`
 
 The purpose of `dynamic()` is twofold:
 
 - provide signal for unspecced functions;
 - handle mixtures of specced and unspecced code gracefully without much noise.
 
-While it is possible to manually introduce the constant `eqwalizer:dynamic()`, the dynamic
+While it is possible to manually introduce the constant `dynamic()`, the dynamic
 type is introduced automatically by eqWAlizer in gradual mode in certain cases:
 
 - as parameter types and result types of unspecced functions, both when type-checking their
@@ -124,10 +109,8 @@ truly be well-typed.
 
 #### Example 2: less noise for invocations of unspecced functions
 
-Consider an unspecced function `unspecced/1`. When invoking it and running eqWAlizer in
-strict mode, it would simply report that it does not know the spec of `unspecced/1` and
-give up. In gradual mode, eqWAlizer instead supposes that `unspecced/1` actually has the
-spec `dynamic() -> dynamic()` and uses this to report some actual
+Consider an unspecced function `unspecced/1`. To provide some signal, eqWAlizer supposes that
+`unspecced/1` actually has the spec `dynamic() -> dynamic()` and uses this to report some actual
 type errors:
 ```Erlang
 -spec call_unspecced() -> binary().

docs/reference/subtyping.md

@@ -42,7 +42,7 @@ In this case, the refined record type `#bar{a :: number()}` is a subtype of `#ba
 
 ### Dynamic
 
-In gradual mode, the dynamic type `eqwalizer:dynamic()` is, in essence, both a subtype
+The dynamic type `dynamic()` is, in essence, both a subtype
 and a supertype of every other type. That is, a value of type `dynamic()` can be used
 in any context, and a function whose return type is `dynamic()` can return anything.
 This differs from the interpretation of `term()`, which is a supertype but not a
@@ -69,6 +69,8 @@ specifies that `get_a(M)` *can* return `err`, which is not of type `binary()` an
 cannot be passed to `binary_to_atom`. In this case, it is necessary to perform
 some kind of check (e.g., pattern-matching) to handle the `err` case separately.
 
+More info can be [found here](./gradual.md).
+
 
 ### Opaque types
 

docs/reference/types.md

@@ -59,8 +59,7 @@ must contain a mapping *for every* atomic key, or *at least one* mapping with
 an atomic key. Similarly, one can define heterogeneous maps such as
 `#{a => binary(), atom() => atom()}`, in which case it is not clear what can
 be stated about a map such as `#{a => ok}`. To avoid such questions, eqWAlizer
-interprets all such maps as the dictionary `#D{term() => term()}` in strict mode,
-or `#D{dynamic() => dynamic()}` in gradual mode.
+interprets all such maps as the dictionary `#D{dynamic() => dynamic()}`.
 
 
 ### List types