If you're talking about the restricted/smart constructor approach that I think is exemplified by this library, i.e. the approach that hides the construction of

If you're talking about the restricted/smart constructor approach that I think is exemplified by this library, i.e. the approach that hides the construction of a type behind a mandatory verification function, it's a pattern that's been around for a long time. OOP constructors are perhaps the best known example, although they often through an exception on invalid input rather than represent this at the type level with an Option/Maybe type or Either type. I personally think that this approach (with the type level tracking) is indeed woefully underused (and is an easy-to-understand-and-implement win in most codebases) and would usually chalk it up to lack of familiarity in the community. That being said, there are definitely domains that can make this approach (without the help of general dependent types) cumbersome to the point that I would consider scrapping it. One example of this is doing statistics and collection types. Most statistical operations operate over a collection of values. This is easily supplied by a standard collection type such as List or Vector. A significant chunk require a non-empty collection of values (think aggregate statistics such as mean). A type such as NonEmptyList or NonEmptyVector comes in handy here along with the corresponding verification function. A smaller chunk require collections of at least two elements (e.g. a sample estimate of standard deviation). Now you need a separate AtLeast2ElemList with a separate verification function. Estimates of higher statistical moments that are used with ever-decreasing frequency the higher you go up require at least 3, 4, etc. elements in a collection. Now you need an AtLeast3ElemList, an AtLeast4ElemList, etc. set of types with all their corresponding distinct verification functions. That's a lot of pain for little gain. In practice I usually personally handle this with covering 90% of cases with a collection and NonEmptyCollection type and then in those other cases have the aggregation function take a general collection and return an optional value rather than enforce GreaterThanN-ness at the input type. This is where dependent types could step in and have a single function AtLeastNElems with a single corresponding verification function and cut down on this madness. Which brings me to general dependent types. If you're talking about general dependent types, the answer is the ergonomics are hard and best practices are still nascent. Coq, Agda, ATS, and Idris are all examples of dependently typed languages, but none of them are close to mainstream. Part of that is because they just haven't had close to the resources devoted to them that mainstream languages have had. Part of that is because some aspects of using them are still somewhat open programmer UX problems. Because you can write any sort of total function in a type signature you have to worry about a couple of things. 1. Compile times. You're doing complex stuff with complex types. It will always be true that you can create pathologically long compile times (this is true in most type systems far weaker than dependent types). What will make or break your type system is if the pathological cases come up regularly in normal code (sad case) or if a user has to create some really messed up code in order to hit those cases (happy case). This is even harder to get right if you give users a ton of rope when it comes to types. 2. If you're not careful not only can you verify, you must verify. It is often the case in a dependently typed language that you will use part of a type to provide a value used in a computation. E.g. a type of GreaterThanX might embed a comparison function that then gets used later in the computation of a value. Most languages have some notion of a "BelieveMeThisIsTrue" value which can be of any type and blows up at runtime if it actually ends up getting called. This functions as an escape hatch that lets you circumvent any type checks because you can always submit this value and have everything type check. You might hope that whenever the burden of verification gets too high, you can just submit "BelieveMeThisIsTrue" if you're sure that some property is true and omit any necessary checks. However, if you've embedded a value-level computation that you are planning to use later on in the type, then "BelieveMeThisIsTrue" will blow up your whole program, e.g. when you go to use the comparison function you've embedded in your GreaterThanX type. This means that you gotta make sure that verification is pretty easy or that it's pretty hard to end up forcing mandatory verification with absolutely no escape hatch. Both are hard problems. Dependent types are extremely exciting, but finding the best way of using them in practice is still something of a research problem. So far the nicest applications of them have been in restricted domains where you don't get the full power of dependent types, which limits their expressiveness, but makes it a lot easier to get the programmer ergonomics right See projects such as LiquidHaskell (https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/) or Cryptol (https://cryptol.net/ https://cryptol.net/).