Types appear to match but fail

[LaltonDundy]

minimal code for replication:

module error

interface  Semigroup' a where
  total
  f : a -> a -> a
  total
  assoc_prf : (x , y, z : a) -> f x (f y z) = f (f x y) z

interface  Semigroup' a => Commutes  a where
  total
  commut_prf : (x,y : a) -> (f x y) = (f y x)

interface Semigroup' a => Monoid' a where
  id_elm : a
  total
  id_prf : (x : a) -> f id_elm x = x

id_elm_r : (Commutes a, Monoid' a) => (x : a) -> f x id_elm = x
id_elm_r x = replace {P = (\ v => v = x)} (commut_prf id_elm x) ?hole

Error that is produced:

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?

error.idr:19:14-69:
   |
19 | id_elm_r x = replace {P = (\ v => v = x)} (commut_prf id_elm x) ?hole
   |              ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of id_elm_r with expected type
        f x id_elm = x

When checking an application of function replace:
        Type mismatch between
                f id_elm x = f x id_elm (Type of commut_prf id_elm x)
        and
                f id_elm x = f x id_elm (Expected type)

        Specifically:
                Type mismatch between
                        f x id_elm
                and
                        f x id_elm

Idris2 states:

P is not a valid implicit argument in replace (commut_prf id_elm x) ?hole

At face value this appears to be a bug since of course f x id_elm is the same as f x id_elm . However, I feel like there is some kinks and quirks about interfaces in Idris that might be producing this error. Not sure where to go from here

[LaltonDundy]

Interfaces have names, would that be related?

[jfdm]

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.

[LaltonDundy]

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

[jfdm]

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 ;-)