Also the Dependent Haskell work of Richard Eisenberg I'd argue is more important as an attempt to shrink the language than add expressive power. The main thing it does is combine existing language features, which only yields more constructs insofar as the old features had friction. You can think of it roughly as taking the convex hull (or probably better bounding parallelepiped) of the existing feature space.

Seen in this light, I've never such a thing attempted at this scale (GHC's size and GHC/Haskell's age), and very much commend it. Hope other things can do the same thing someday.