Idris feels mostly dead to me at this point. Which breaks my heart, because for a split second it had real momentum around it.

Not OP, but as Haskell-derived dependently-typed languages Idris and Agda are quite similar, so I suspect if they like one they’d like the other.