Check for conflicting store capabilities in the initial program.
Check for conflicting store capabilities in a module.
Check for conflicting store capabilities in an expression.
Things that can go wrong with the capabilities in a program.
Conflicting capabilities in program.
A partially applied capability constructor. In the formal semantics, capabilities are atomic, so this isn't a problem. However, as we're representing them with general witness appliction we need to ensure the constructors aren't partially applied.
A capability constructor applied to a non-region handle.