Types appear to match but fail about idris-dev HOT 4 OPEN

essentially, at the type-level names that are not capitalised are treated (greedily) as implicit arguments.
This is why you saw the Idris1 error message:

error.idr:18:54-59:
   |
18 | id_elm_r : (Commutes a, Monoid' a) => (x : a) -> f x id_elm = x
   |                                                      ~~~~~~
id_elm is bound as an implicit
        Did you mean to refer to error.id_elm?

There are two approaches, in Idris1 either you ensure the thing in the type is capitalised, or that the thing is suitably qualified.
I haven't looked at your example in Idris2.

PS

Ahhhh Thank you so much!

I've been using Idris for a while, and the colouring still sometimes escapes me! We should really be a bit better with the annotations here as some people might not be readily aware of semantic highlighting (nor what the highlighting is supposed to represent). PRs on Idris1 and Idris2 are welcome ;-)

from idris-dev.

Interfaces have names, would that be related?

from idris-dev.

The key question here, is what are the colour of the things Idris is complaining about!

Idris' supports semantic highlighting and tells us about what things are!

If you look at the error message for line 18, Idris does explicitly give a hint to what is going on here.

But first check the colour's in Idris' output.

from idris-dev.

Ahhhh Thank you so much!

I am getting non-italic purple vs non-italic green; so its a variable against a function according to the link.

Guess I must have have named an implicit function with that variable name or something

from idris-dev.