I would argue that OO is polymorphism + innate object identity. Though the latter only matters if you have mutability; but then, whether OO without mutability is "true OO" is one of those deeply philosophical questions.
I find the dividing line in formalism; we can always find similarities with language-level features from OO, but OO is by definition an informal set of ideas about how programming is best done and understood, rooted deeply in empiricism, not formal theory and analysis.
If I can model your type/language model as a higher-kinded dependently typed lambda calculus (e.g. using Boehm-Berarducci encoding for non-turing complete recursive ADT definitions), then it's not OO -- it's functional programming, rediscovered.
Existential types are kind of like OO interfaces (allow storing a collection of things that only have in common that they implement the interface), and typeable can be used for casting them back to their base types.
The library in question is modeling relational theory at the language/type level. That's not remotely like an ORM.