Now do users with various level of RBAC, and show me how the type system solves that "very easily".

I'll wait.

It doesn't necessarily solve this completely, but it can be used to significantly reduce the amount of code you have to manually audit. For example, you could use tokens to represent permissions, and arrange your code so that only a small portion of your code can create them. Then you can rely on the presence of that token indicating that a check has been performed in the rest of your code.

The type system is a tool to reduce the space of invalid inputs.

This is also easy. There are different ways to do it.

Here's an example: create a type, such as "RoleAuthorization". Make it a required parameter for access-controlled methods, either through the constructor of the parent object or explicitly in the method.

In order to create a RoleAuthorization, you must first pass the user's Role object in an authorization method.

If a method requires authorization, the compiler will complain if you don't first check the current user's role through the authorization method.

> I'll wait.

If you're sincerely interested in discussing something, antagonizing someone this way (and implying that you are infallible) really doesn't help.

If you just wanted to make what you believe is a statement of fact, just make it.

If you don't want to discuss the issue at all and would instead prefer to be unchallenged on this topic, why write about it in a comments section?

Wouldn't union just work?

authenticate() : role1 | role2

That assumes you know all the roles ahead of time. In many systems they will consist of a large number of variant both in how they authenticate and in what they're allowed to do. It may even depend on environment ideas which cannot be represented in types. (like: user X can issue commands Y, Z in times when they're on call, where "on-call" is a custom operator's rule, not something known earlier)

But you do know every permission in advance, thus static. How a user gets a permission can be dynamic.

This, or a union of access rights in a case where roles may be defined in a database.