Add more fluff and detailing.

rfcs/none-and-unknown-types.md

@@ -11,33 +11,8 @@ and type normalization, where it would be useful to have top and
 bottom types. Currently, `any` is filling that role, but it has
 special "switch off the type system" superpowers.
 
-The `never` type comes up whenever type inference infers incompatible types for a variable, for example
-
-```lua
-  function oops(x)
-    print("hi " ++ x)  -- constrains x must be a string
-    print(math.abs(x)) -- constrains x must be a number
-  end
-```
-
-The most general type of `x` is `string & number`, so this code gives
-a type error, but we still need to provide a type for `oops`. With a
-`never` type, we can infer the type `oops : (never) -> ()`.
-
-The `never` type is also useful in cases such as tagged unions where
-some of the cases are impossible. For example:
-
-```lua
-  type Result<T, E> = { err: false, val: T } | { err: true, err: E }
-```
-For code which we know is successful, we would like to be able to
-indicate that the error case is impossible. With a `never` type, we
-can do this with `Result<T, never>`. Similarly, code which cannot succeed
-has type `Result<never, E>`.
-
-The `unknown` case is useful in cases where the user of an API must
-use type casing to use the API safely. For example a function which
-can return any value is:
+Any use of `unknown` must be narrowed by type refinements unless another `unknown` or `any` is expected. For
+example a function which can return any value is:
 
 ```lua
   function anything() : unknown ... end
@@ -47,7 +22,7 @@ and can be used as:
 
 ```lua
   local x = anything()
-  if type(x) == "number"
+  if type(x) == "number" then
     print(x + 1)
   end
 ```
@@ -63,13 +38,64 @@ if the type of `anything` is `() -> any` then the following code typechecks:
 
 This is fine in nonstrict mode, but strict mode should flag this as an error.
 
-These types can be defined in current Luau, but only quite verbosely:
+The `never` type comes up whenever type inference infers incompatible types for a variable, for example
+
+```lua
+  function oops(x)
+    print("hi " .. x)  -- constrains x must be a string
+    print(math.abs(x)) -- constrains x must be a number
+  end
+```
+
+The most general type of `x` is `string & number`, so this code gives
+a type error, but we still need to provide a type for `oops`. With a
+`never` type, we can infer the type `oops : (never) -> ()`.
+
+or when exhaustive type casing is achieved:
+
+```lua
+  function f(x: string | number)
+    if type(x) == "string" then
+      -- x : string
+    elseif type(x) == "number" then
+      -- x : number
+    else
+      -- x : never
+    end
+  end
+```
+
+or even when the type casing is simply nonsensical:
+
+```lua
+  function f(x: string | number)
+    if type(x) == "string" and type(x) == "number" then
+      -- x : string & number which is never
+    end
+  end
+```
+
+The `never` type is also useful in cases such as tagged unions where
+some of the cases are impossible. For example:
+
+```lua
+  type Result<T, E> = { err: false, val: T } | { err: true, err: E }
+```
+
+For code which we know is successful, we would like to be able to
+indicate that the error case is impossible. With a `never` type, we
+can do this with `Result<T, never>`. Similarly, code which cannot succeed
+has type `Result<never, E>`.
+
+These types can _almost_ be defined in current Luau, but only quite verbosely:
 
 ```lua
   type never = number & string
-  type unknown = nil | number | boolean | string | {} | Instance | (never...)->(unknown...)
+  type unknown = nil | number | boolean | string | {} | (...never) -> (...unknown)
 ```
 
+But even for `unknown` it is impossible to include every single data types, e.g. every root class.
+
 Providing `never` and `unknown` as built-in types makes the code for
 type inference simpler, for example we have a way to present a union
 type with no options (as `never`). Otherwise we have to contend with ad hoc
@@ -80,9 +106,28 @@ corner cases.
 Add:
 
 * a type `never`, inhabited by nothing, and
-* a type `unknown`, inhabited everything.
+* a type `unknown`, inhabited by everything.
 
-Use them, rather than `any` where appropriate. Ideally, we would then never infer `any`.
+And under success types (nonstrict mode), `unknown` is exactly equivalent to `any` because `unknown`
+encompasses everything as does `any`.
+
+The interesting thing is that `() -> (never, string)` is equivalent to `() -> never` because all
+values in a pack must be inhabitable in order for the pack itself to also be inhabitable. In fact,
+the type `() -> never` is not completely accurate, it should be `() -> (never, ...never)` to avoid
+cascading type errors. Ditto for when an expression list `f(), g()` where the resulting type pack is
+`(never, string, number)` is still the same as `(never, ...never)`.
+
+```lua
+  function f(): never error() end
+  function g(): string return "" end
+
+  -- no cascading type error where count mismatches, because the expression list f(), g()
+  -- was made to return (never, ...never) due to the presence of a never type in the pack
+  local x, y, z = f(), g()
+  -- x : never
+  -- y : never
+  -- z : never
+```
 
 ## Drawbacks
 
@@ -96,4 +141,4 @@ Replacing `any` with `unknown` is a breaking change: code in strict mode may now
 
 Stick with the current use of `any` for these cases.
 
-Make `never` and `unknown` type aliases rather than built-ins.
+Make `never` and `unknown` type aliases rather than built-ins.