The current formulation is intended to capture something a bit different: namely, resources of the same kind (in the RM sense) are of the same type (in the QTT sense), even if they have different values (in the RM sense). One might understand the set of possible resource values for a particular resource kind as the set of members of a sum type defined by the kind (which commits to the logic that ultimately defines the set of values with which resources could actually be created).
While your proposal – as I understand it – should be of equivalent expressive power in terms of application construction (as compared to the current ruleset), it would have us forfeit the ability to make this type/instance distinction in the “resource linear logic”. This means that we would need to build the linear logic for the type level on top, e.g. have rules for summing up the value
fields of various Spacebucks resources and checking that the sum of the value
fields for consumed Spacebucks is equal to the sum of the value
fields for created Spacebucks. This is possible, but it seems inelegant to me – we already have a programmable linear logic, why not use it? – and will create additional complexity in the shielded case (we would have to implement another layer of homomorphic value encryption).
n.b. I can understand that ephemeral resources are awkward to use for some constraint-passing purposes at the moment, but I think we can fix that problem in a different way, which I outlined here. Even if we don’t take that approach, I don’t think we need to go so far as to ditch precise control of the linear logic in order to fix the developer ergonomics.
Does this help clarify the design intention? I admit that the connection to QTT is little more than “we read the QTT paper, read the Zcash specs, and figured out how to mesh them together in some way that seemed reasonable, gave us a type/instance distinction, and preserved the nice homomorphic commitments from Zcash” – we haven’t ever formalized what this “resource linear logic” is really supposed to be at a slightly higher level of abstraction, and I think the project of doing so may prove quite rewarding.