[tel]

Yeah, less power means greater inference. You can model liquid types in a DT language I believe, but you'll never have the same convenience.

[vilhelm_s]

"Dependent types" is a quite broad term. The Liquid types people certainly call their work dependent types, even though it has a different flavour than e.g. Coq or Agda.

[tel]

Yes, that's true—I lapsed in terminology. Maybe calling it ITT would be better? There's a lot of ambiguity there, of course. And less marketing.