Mostly when I read about impredicativity I see people bemoaning its downsides.
But it's not clear to me why I would want impredicativity in the first place.
Impredicativity is useful for analyzing impredicative systems. And impredicative Pi types can be used to encode recursive datatypes without going up a universe. However, from what I understand Cedille has to go through a few contortions to have induction principles over impredicative encodings of datatypes.