Make final parameter of Acc an index

[Taneb]

Suggested by @TOTBWF during my investigation on Mikan compatibility. This makes induction proofs pass Mikan's termination checker, and doesn't seem to break anything with Agda.

[gallais]

Does that impact the generated code? It looks to me like acc would now be storing its index
and may not be erasable anymore?

[Taneb]

You're right, it doesn't look like MAlonzo is able to erase Acc any more :(

[JacquesCarette]

But maybe this is still the 'right' Acc?

[gallais]

Would marking x as erased bring back the compilation to performant Acc-free code?

[TOTBWF]

Mikan has dropped support for erasure, so that would somewhat defeat the purpose.

That being said, I agree with @JacquesCarette: this non-regular parameter is a bit dubious. Unfortunately, it seems like Barras' thesis has bit-rotted off the internet, but I don't see a way to use his encoding to construct an index that forcing analysis would be able to erase. (I actually don't even know if his encoding works for higher-order datatypes like Acc, but that's a separate can of worms!)

[Taneb]

I did a not really scientific benchmark of actually running a program that heavily uses Acc that I had lying around, and I don't see any significant changes in runtime between index and parameter. So maybe even though MAlonzo can't get rid of it, GHC can?