Using named implementations with scoped interface constraints results in confusing error

[philandstuff]

This seems related to #3135. This is my minimal test case:

[show2] Show Integer where
  show i = "5"

f : ({s:_} -> Show s => s -> String) -> Integer -> String
f g t = g @{show2} t

This fails to compile with No such variable g, when in fact g is right there in scope. Without the explicit named implementation, it compiles and behaves the way I expect (ie with the default Show implementation).

The error message is confusing.

I guess that named implementations are subject to the same restrictions as implicit parameters - ie you can't pass a named implementation to a non-top-level function?

I tried finding a workaround using where clauses, similar to #3135 and #3136 , but I couldn't get it to typecheck. I tried a few different variations on this theme:

[show2] Show Integer where
  show i = "5"

f : ({s:_} -> Show s => s -> String) -> Integer -> String
f g t = g' @{show2} t where
   g' : Show s => s -> String
   g' = g

Is there a way to work around this problem for the moment?

(Oh and in case you're wondering about my use case, I'm playing around trying to implement pure-profunctor lenses, which involve a lot of interface-constrained rank-2 polymorphism.)

[ahmadsalim]

Thanks for the report, and apologies for a late answer. I unfortunately do not know a useful workaround myself but maybe someone else in @idris-lang/contributors knows.

Otherwise, please try the mailing list.