The first system we came up with was heavily influenced by four things: those pesky “inexhaustive pattern match” warnings in ML, John Reynolds’ work on intersection types that solved a deep problem for us, abstract interpretation, and order-sorted typing that was investigated for logic programming at the time. Since we (that is, Tim Freeman and I) didn’t see anything on the horizon satisfying (a), (b), and (c), we called them just “refinement types”. With a crystal ball, we should have called them “datasort refinements”, and that’s what I like to use now. “Index refinements” (the work with Hongwei Xi) were also designed to satisfy (a), (b), and (c), so they are an example of “type refinement” (the research program), but distinct from “refinement types” in their original meaning as datasort refinements.

General subset types aren’t quite an example of what we meant, because type checking with arbitrary subset types is both undecidable and impractical. But subset types {x:T|P(x)} could satisfy our goals as long as P is drawn from a tractable domain and the whole system that includes them hangs together.

I’ve only read an earlier version of the second paper, so take this with double the usual grains of salt, but I’m pretty sure it doesn’t have datasort refinements. They talk about “refinements on data constructors”, but I would say they’re translating refinement types (or index refinements) into refinement types. If you look at slist2 in the introduction, it still has {x:T|e} types; it’s just formulated differently than their slist1. (slist2 is very close to Xi’s DML. The difference is that in DML, you’d index slist2 by its smallest element, rather than talk about “head xs” inside e; you also need some kind of hack to get the effect of indexing SNil by +∞.) In fact, you can’t express the sortedness of a list with just datasorts; you’d need as many datasorts as you have integers.

They also don’t have subtyping; without subtyping, datasorts wouldn’t be worth much.

Atkey, Johann, and Ghani relate type refinements and dependent inductive types in When is a Type Refinement an Inductive Type?. More recently, Sekiyama, Nishida, and Igarashi move statically and dynamically between datasort refinements and index refinements in Manifest Contracts for Datatypes. I’m not sure if either of those quite fit the bill of what you’ve been wondering, but they’re both great papers in any case.

The confusion makes sense—datasort refinements are identifying subsets, index refinements are also identifying subsets. But the techniques involved in using the two are so different. I agree with you: it’s worth keeping the nomenclature clear.

CMU’s invention of “type refinement” as a notion for a wide range of stuff including datasort refinements didn’t catch on. It’s possible that trying to simultaneously rename “refinement type” to “datasort refinement” *and* introduce a new term “type refinement” was doomed, but why did “refinement type” have to get mutated in place?

(By a strange coincidence, I was just thinking about whether indexed types *are* refinement types in the current sense. Or, rather, whether refinement types are indexed types. I think they probably are, via singletons and the guarded/asserting types from my thesis, but I haven’t worked it out, so I’m just blowing smoke, so far.)