Added more documentation about type narrowing and type guards.

docs/internals.md

@@ -41,7 +41,7 @@ Pyright uses an internal type called “Unknown” to represent types that are n
 
 Pyright attempts to infer the types of global (module-level) variables, class variables, instance variables, and local variables. Return and yield types are also inferred. If type annotations are provided in these cases, the type annotation overrides any inferred types.
 
-Pyright supports type narrowing (sometimes called “type guards”) to track assumptions that apply within certain code flow paths. For example, consider the following code:
+Pyright supports type narrowing to track assumptions that apply within certain code flow paths. For example, consider the following code:
 ```python
 def func(a: Optional[Union[str, List[str]]):
     if isinstance(a, str):

docs/type-concepts.md

@@ -90,3 +90,103 @@ my_list_2.append(None)  # Error
 The type error on the second line has now gone away, but a new error is reported on the third line because the `append` operation is not allowed on an immutable Sequence.
 
 For more details about generic types, type parameters, and invariance, refer to [PEP 483 — The Theory of Type Hints](https://www.python.org/dev/peps/pep-0483/).
+
+
+### Type Narrowing
+
+Pyright uses a technique called “type narrowing” to track the type of a symbol based on code flow. Consider the following code:
+
+```python
+val_str: str = "hi"
+val_int: int = 3
+
+def func(val: Union[float, str, complex], test: bool):
+    reveal_type(val) # Union[int, str, complex]
+
+    val = val_int # Type is narrowed to int
+    reveal_type(val) # int
+
+    if test:
+        val = val_str # Type is narrowed to str
+        reveal_type(val) # str
+    
+    reveal_type(val) # Union[int, str]
+
+    if isinstance(val, int):
+        reveal_type(val) # int
+        print(val)
+    else:
+        reveal_type(val) # str
+        print(val)
+```
+
+At the start of this function, the type checker knows nothing about `val` other than that its declared type is `Union[float, str, complex]`. Then it is assigned a value that has a known type of `int`. This is a legal assignment because `int` is considered a subclass of `float`. At the point in the code immediately after the assignment, the type checker knows that the type of `val` is an `int`. This is a “narrower” (more specific) type than `Union[float, str, complex]`. Type narrowing is applied when ever a symbol is assigned a new value.
+
+Another assignment occurs several lines further down, this time within a conditional block. The symbol `val` is assigned a value known to be of type `str`, so the narrowed type of `val` is now `str`. Once the code flow of the conditional block merges with the main body of the function, the narrowed type of `val` becomes `Union[int, str]` because the type checker cannot statically predict whether the conditional block will be executed at runtime.
+
+Another way that types can be narrowed is through the use of conditional code flow statements like `if`, `while`, and `assert`. Type narrowing applies to the block of code that is “guarded” by that condition, so type narrowing in this context is sometimes referred to as a “type guard”. For example, if you see the conditional statement `if x is None:`, the code within that `if` statement can assume that `x` contains `None`. Within the code sample above, we see an example of a type guard involving a call to `isinstance`. The type checker knows that `isinstance(val, int)` will return True only in the case where `val` contains a value of type `int`, not type `str`. So the code within the `if` block can assume that `val` contains a value of type `int`, and the code within the `else` block can assume that `val` contains a value of type `str`. This demonstrates how a type (in this case `Union[int, str]`) can be narrowed in both a positive (`if`) and negative (`else`) test.
+
+### Type Guards
+
+In addition to assignment-based type narrowing, Pyright supports the following type guards.
+
+* `x is None` and `x is not None`
+* `x == None` and `x != None`
+* `type(x) is T` and `type(x) is not T`
+* `x is E` and `x is not E` (where E is an enum value)
+* `x == L` and `x != L` (where L is a literal expression)
+* `x.y == L` and `x.y != L` (where L is a literal expression and x is a type that is distinguished by a field with a literal type)
+* `x in y` (where y is instance of list, set, frozenset, or deque)
+* `S in D` and `S not in D` (where S is a string literal and D is a TypedDict)
+* `isinstance(x, T)` (where T is a type or a tuple of types)
+* `issubclass(x, T)` (where T is a type or a tuple of types)
+* `callable(x)`
+* `f(x)` (where f is a user-defined type guard that is annotated to return a TypeGuard[T] type)
+* x (where x is any expression that is statically verifiable to be truthy or falsy in all cases)
+
+Expressions supported for type guards include simple names, member access chains (e.g. `a.b.c.d`), the unary `not` operator, the binary `and` and `or` operators, and call expressions. Other operators (such as arithmetic operators or subscripts) are not supported.
+
+Some type guards are able to narrow in both the positive and negative cases. Positive cases are used in `if` statements, and negative cases are used in `else` statements. (Positive and negative cases are flipped if the type guard expression is preceded by a `not` operator.) In some cases, the type can be narrowed only in the positive or negative case but not both. Consider the following examples:
+
+```python
+class Foo: pass
+class Bar: pass
+
+def func1(val: Union[Foo, Bar]):
+    if isinstance(Bar):
+        reveal_type(val) # Bar
+    else:
+        reveal_type(val) # Foo
+
+def func2(val: Optional[int]):
+    if val:
+        reveal_type(val) # int
+    else:
+        reveal_type(val) # Optional[int]
+```
+
+In the example of `func1`, the type was narrowed in both the positive and negative cases. In the example of `func2`, the type was narrowed only the positive case because the type of `val` might be either `int` (specifically, a value of 0) or `None` in the negative case.
+
+### Narrowing Any
+
+In general, the type `Any` is not narrowed. The only exceptions to this rule are the built-in `isinstance` and `issubclass` type guards plus user-defined type guards. In all other cases, `Any` is left as is, even for assignments.
+
+```python
+a: Any = 3
+reveal_type(a) # Any
+
+a = "hi"
+reveal_type(a) # Any
+```
+
+The same applies to `Any` when it is used as a type argument.
+
+```python
+b: Iterable[Any] = [1, 2, 3]
+reveal_type(b) # List[Any]
+
+c: Iterable[str] = [""]
+b = c
+reveal_type(b) # List[Any]
+```
+