Idris 2 ruined it for me.

Scientifically, it's cool of course, dependent linear types yaay.

Socially though, incompatible rewrite in Scheme should've been a separate project IMO; but since it's called "Idris 2", community attention faded away from the Haskell implementation "Idris 1". Which caused bad maintenance, neglect, stagnation, of a thing I tried and liked.