From ba38a41ef1ec41c7fe5cc64a0db89e0b55365973 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Wed, 8 May 2024 22:02:23 -0700 Subject: [PATCH] Shouldn --- docs/negation-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/negation-types.md b/docs/negation-types.md index e51f814..bc0eecf 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -55,7 +55,7 @@ As you can see, since through the series of rewrites `~~any` did not produce a t We currently only support negation of _testable_ types. Intuitively, a testable type is one that can be tested by type refinements at runtime. This includes singleton types, primitive types, and classes. Of course, unions and intersections can be negated as well if and only if all of its constituent types are also testable types, due to the distributivity property of unions and intersections. -Since types like `{ p: P }` and `(T) -> U` are structural types and the runtime offers no way to test for them, they cannot be negated. An attempt to negate this will just turn the negation type into an error suppressed type. This means `~{ p: P }` and `~(T) -> U` are nonsensical. In the event that you negate some non-testable types, you get a type error. +Since types like `{ p: P }` and `(T) -> U` are structural types and the runtime offers no way to test for them, they cannot be negated. An attempt to negate this will just turn the negation type into an error suppressed type. This means `~{ p: P }` and `~(T) -> U` are nonsensical. In the event that you negate some non-testable type, you get a type error. Another restriction is that negation types cannot negate generic types. So `(T) -> ~T` is also not legible.