Thank you for spelling this out; comments like these make this website worthwhile. You've enlightened at least one person today.
You hinted that there's more to QTT (or its implementation in Idris?) than this. Could you elaborate a bit on what these other features are, and what their purpose is?
You hinted that there's more to QTT (or its implementation in Idris?) than this. Could you elaborate a bit on what these other features are, and what their purpose is?