@jaror will this interact with any future proposals towards DH? I’m worried that this increase the pile of chores one would have to do to finally reach the goal of implementing them, similarly to how it happened with LinearTypes (and multiplicity polymorphism ftm) themselves.