[ new,pragma ] add %ensure_identity

[CodingCellist]

Description

This came up during in-person discussion with Ohad Kammar, during the 2026 May IDM: sometimes, it is useful to be able to annotate a function which should reduce to the identity function, but where one wants a warning if it did not.

Currently, the message prints 3 times for some reason, but otherwise appears to work!

TODO

• Figure out why the message prints thrice, and fix that.
  • Done, thanks to Z-snails ([ new,pragma ] add %ensure_identity #3785 (comment))

Self-check

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md
• I confirm that this contribution did not involve GenerativeAI nor Large Language Models.

[dunhamsteve]

Can we add this to source/reference/pragmas.rst, too?

[Z-snails]

The identity optimisation pass is run multiple times, since replacing a function with id can allow later functions to be detected as id. See

Idris2/src/Compiler/Inline.idr

Line 564 in 6a54860

export

[stefan-hoeck]

Very nice! Will this result in an error with --Werror?

[CodingCellist]

Can we add this to source/reference/pragmas.rst, too?

Will do! Didn't know that was a thing, so thanks for pointing it out! : )

---

The identity optimisation pass is run multiple times, since replacing a function with id can allow later functions to be detected as id. See

Idris2/src/Compiler/Inline.idr

Line 564 in 6a54860

export

Oh duh, it's the transform 3 call, presumably. Thank you! : D
I even remember noticing that call when I was working out where the identity optimisation actually happens. Clearly I just immediately forgot it again ^^;
But that would raise the warning three times, so it might just be expected behaviour?

---

Very nice! Will this result in an error with --Werror?

Just checked. Yes it will! : D

$ idris2 --check -Werror TestEnsureId.idr
1/1: Building TestEnsureId (TestEnsureId.idr)
Error: TestEnsureId.notId was explicitly annotated as reducing to the
identity function, but the compiler did not optimise it as such.

Error: TestEnsureId.notId was explicitly annotated as reducing to the
identity function, but the compiler did not optimise it as such.

Error: TestEnsureId.notId was explicitly annotated as reducing to the
identity function, but the compiler did not optimise it as such.

[CodingCellist]

I added some code to track the number of transformation passes in the warning message itself. I think this is helpful, but if it clutters things too much, I'm happy to revert that commit : )

[dunhamsteve]

The identity optimisation pass is run multiple times, since replacing a function with id can allow later functions to be detected as id.

So, with a warning on each pass, we might get two failures followed by a success? Is there a way to check and warn at the end.

E.g. we do this manually by doing :di foo and seeing if the runtime tree is x => x shaped, maybe we can do that after the compilation of runtime tree finishes?

[CodingCellist]

Is there a way to check and warn at the end.

Possibly, but I'm not sure. I don't know whether the name gets transformed/mangled as part of the other optimisations, but if it doesn't we could track the name as part of the EnsureIdFailed warning, to spot if an optimisation succeeded.

Don't know how I would write a test to trigger that, however...