Yeah I agree that Idris itself would be much too large, however you could write a much smaller Lambda Pi that could still enable a lot of nice features.