As part of our software toolkit at a major financial institution
we have a library for relational algebra.
This library is written in C++ and the type checking of the operations on the relations is very dynamic; all relations have the same static type.
Of course, relational algebra operations have stringent type constraints,
and since we believe in static typing, we would prefer these to be checked at compile time.

We have managed to get full static type checking of the relational code,
using some modern extensions to the Haskell type system, such as
closed type families, type level strings, user-defined kinds, and custom type errors.
The static type checking incurs no runtime overhead compared to the dynamically checked library.

Some effort has gone into making the use of the typed library similar to the dynamically typed version.
We have also tried to produce good error messages when something is wrong.