[a-saleh]

I think I mostly liked those type-systems that lean towards dependent, but not go all the way.

Purescript might be favourite? Even by default you get more power than i.e. vanilla Haskell, with row-types. But then you can get type-level list, typelevel string, even typelevel regex! And you use these through type-classes in a kind of logic-programming way.