1. The subsumption rule is elegant, but doesn't answer the pragmatic question: for what use-cases is a naive structural type system (familiar to a large populat

1. The subsumption rule is elegant, but doesn't answer the pragmatic question: for what use-cases is a naive structural type system (familiar to a large population of developers) insufficient? Logic theory has type towers, but for 99% of the use-cases values and types are interesting, rarely kinds. Not even sure if 'type of kinds' has a name by itself. Possibly constraints are an answer, but the constraint system feels ad-hoc. To rephrase, how would one describe Cue type system as a generalization of a naive structural type system? 2. Not sure what you mean by 'idempotent', perhaps 'pure' or 'no side-effects'? There is plenty of non-turing complete computations that can be done with pure functions.