Dear all,
This proposal suggests adding syntax for a general notion of modifiers, like the ones we’ve been talking about lately affecting linearity or matchability of arrows. For example, if linear types and unsaturated families are accepted as they stand, we would have `Int #1 -> @U Bool` (or something like that), whereas with this proposal we would have the more uniform `Int %1 %Unmatchable -> Bool`.
Since the amount of modifiers is likely to increase in the future, I think it’s a great idea to agree and reserve such syntax, instead of coming up with different ways on each proposal. I thus recommend acceptance of this proposal.
The proposal itself:
(1) introduces syntax for modifiers in types and defines how to type/kind check them,
(2) reserved such syntax for other uses in declarations and terms.
I think the proposal still has its merits only with (1), even though I lean towards accepting both parts of it.
Regards,