I suppose it's less useful as a standalone technique - I've used it before but not that heavily (e.g. in a library built around sequencing effects in a certain

I suppose it's less useful as a standalone technique - I've used it before but not that heavily (e.g. in a library built around sequencing effects in a certain way, where I've wanted to guarantee that one effect can't be called before another). Really we'd want a considerably more powerful type system - Idris 2's quantitative types and/or Rust's ownership, for example - before that particular technique really starts to shine. However, the general mindset is one I use all the time. For example, if I've written a state machine that is represented explicitly in the types, I might be able to encode some of the state transitions in the type system directly, so the compiler prevents me writing certain invalid transitions. For example, if state B can only be reached after state A, I might write the in-memory representation of B to contain an in-memory representation of A; this guarantees I must have passed something through state A to get anything in state B. Doesn't save you from everything - in particular it doesn't solve your "passing the token to the wrong instance of the object" problem - but any constraint on the state space is useful in my book. When the state machine gets sufficiently large, in my experience, the benefits of the restricted state space start outweighing the negatives of manual token shuffling. (I have a blog post brewing about this general class of techniques, but I don't know when it'll be ready.)