> How can you do a compile time check on data that has not entered the system?
You would have to supply proof that your types are correct; when you have a value who's type you'll only know at run time, you'll need to perform case analysis to bring additional info about the value's type into scope in the respective branches. To make concrete what I'm describing here, I'll use Idris's ++ (concatenation) as an example, which provides an inductive proof for the length of the resulting vector:
(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
(++) [] ys = ys
(++) (x::xs) ys = x :: xs ++ ys
The first line is the type signature, which claims that the length of the resulting vector is the sum of the lengths of the two argument vectors.
The second line pattern matches on the null/empty constructor of the vector, and then returns ys. By pattern matching on the null constructor, we know that m == 0. We also know that n == length ys (whatever that may be). We know that 0 + x = x, so if we apply that to this case, we know that:
length ([] ++ ys)
== length [] + length ys
== 0 + length ys
== length ys
== n
== m + n (because we know m==0, and 0+n==n)
... so the compiler is happy here.
The third and final line pattern matches on the non-empty (or cons, if you're a fan of Lisp) constructor. If this pattern applies, then we can make use of the fact that length (x::xs) == 1 + length xs. Of course, that that implies length xs < length (x::xs). That permits us to apply our induction hypothesis to the (xs ++ ys) sub expression, which tells that length (xs ++ ys) == length xs + length ys. Putting all of that together, we see that
length (x :: xs ++ ys)
== 1 + length (xs ++ ys)
== 1 + length xs + length ys
== 1 + (m - 1) + length ys
== m + length ys
== m + n
That concludes our proof by induction[1].
Note that this proof is checked completely at compile time, and that it is still valid in the face of types which we won't know until we run our program.
That's what dependent types give you.
Here's an example that would not compile:
(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
(++) [] ys = ys
(++) (x::xs) ys = x :: x :: xs ++ ys {- !!! note that I cons x here *twice* -}
In conclusion, your library sounds like it could be an excellent way to provide smart constructors; at the same time, it's important to not conflate smart constructors with dependent types. I would urge you to continue developing your library, though I would recommend switching the name to something that's more indicative of what it actually does. That would have the additional benefit of not confusing people who read your project description and are hearing about dependent types for the first time.
[1]: https://en.wikipedia.org/wiki/Mathematical_induction