feat: typechecking in schema

Author: miparnisari

app/best-practices/page.mdx

@@ -170,6 +170,12 @@ One of the big benefits to using a centralized authorization system like SpiceDB
 It can be tempting to define the authorization logic for an endpoint as being the `AND` or `OR` of the checks of other permissions, especially when the alternative is writing a new schema.
 However, this increases the likelihood of drift across your system, hides the authorization logic for a system in that system's codebase, and increases the load on SpiceDB.
 
+### Use Typechecking
+
+Tags: **schema**
+
+Adding [type-checking](https://authzed.com/docs/spicedb/concepts/schema#typechecking) to your schema can turn some silent bugs into failures at `WriteSchema` time.
+
 ### Avoid Cycles in your Schema
 
 Tags: **schema**

app/spicedb/concepts/schema/page.mdx

@@ -444,6 +444,131 @@ definition user {
 But in order to express that a user should be able to view themselves, you'll need to write a corresponding relationship (e.g. `user:alice#viewer@user:alice`)
 for the check to evaluate to true. The `self` keyword requires less DB space and computation to achieve the same result.
 
+### Typechecking
+
+The `use typechecking` feature allows you to explicitly declare and validate the types that permissions can resolve to, providing type safety for your authorization schemas.
+
+Consider this schema:
+
+```zed
+definition user {}
+definition serviceaccount {}
+
+definition document {
+	relation viewer: user
+	relation admin: serviceaccount
+	permission edit = viewer & admin
+}
+```
+
+This schema writes successfully, but a call to `CheckPermission` for `document#edit` will _always_ return false at runtime because no relationship can simultaneously be for a `user` subject and for a `serviceaccount` subject. This is a bug that can go unnoticed for a long period of time, because the API call doesn't return an error.
+
+Adding [type-checking](https://authzed.com/docs/spicedb/concepts/schema#typechecking) will turn that silent bug into a failure:
+
+```zed
+use typechecking
+
+definition user {}
+definition serviceaccount {}
+
+definition document {
+	relation viewer: user
+	relation admin: serviceaccount
+	permission edit: user = viewer & admin
+}
+```
+
+This will fail at `WriteSchema` time because the type annotation provided is incomplete: it needs to be `permission edit: user | serviceaccount = viewer & admin` for the satisfy the type checker. However, the error given by the typechecker is really pointing at the underlying issue: you should fix the permission itself.
+
+- Should the `edit` permission really be an intersection?
+- Is `serviceaccount` the only type that can be an `admin`?
+- Is `user` the only type that can be a `viewer`?
+
+#### Use
+
+Enable type checking by adding `use typechecking` at the top of your schema, and then add the type annotations to the permissions:
+
+```zed
+use typechecking
+
+definition user {}
+
+definition document {
+    relation viewer: user
+    permission view: user = viewer
+}
+```
+
+The syntax for type annotations is:
+
+```zed
+permission <name>: <type1> | <type2> | ... = <expression>
+```
+
+Note that type annotations must be complete: they must include **all** types reachable through the permission expression.
+
+You can also slowly transition into a type-annotated schema by mixing annotated and non-annotated permissions:
+
+```zed
+use typechecking
+
+definition user {}
+
+definition document {
+    relation viewer: user
+    permission view: user = viewer      // Validated
+    permission edit = viewer            // Not validated (no annotation)
+}
+```
+
+#### Examples
+
+- Single Type
+
+```zed
+use typechecking
+
+definition user {}
+
+definition document {
+    relation viewer: user
+    permission view: user = viewer
+}
+```
+
+- Multiple Types
+
+```zed
+use typechecking
+
+definition user {}
+definition team {}
+
+definition document {
+    relation viewer: user | team
+    relation owner: user | team
+    permission view: user | team = viewer + owner
+}
+```
+
+- With Arrow Operations: the annotations must be for the types on the right-hand side of the arrow:
+
+```zed
+use typechecking
+
+definition user {}
+definition team {}
+
+definition organization {
+    relation member: user | team
+}
+
+definition document {
+    relation org: organization
+    permission view: user | team = org->member
+}
+```
+
 ### Naming Permissions
 
 Permissions define a set of objects that can perform an action or have some attribute, and thus **permissions should be named as verbs or nouns**, read as `(is/can) {permission name} (the object)`.