If I want to define a show function inside a Main module, I have to prepend the module name explicitly like this:
module Main
Main.show : Nat -> String
Main.show Z = ""
Main.show (S n) = "I" ++ (Main.show n)
Otherwise I get the error Can't disambiguate name: Main.show, Prelude.Show.show. Is there a way to tell Idris that my current module has priority, to avoid writing Main. everywhere? I'd be fine writing Prelude.Show.show to refer to the implementation outside of my module, but I want to just write show to refer to Main.show since I'm mostly working with that inside my module.
First of all, you only need to prepend the Main. on the recursive function call, where Idris doesn't know if you mean Main.show or Prelude.Show.show:
show : Nat -> String
show Z = ""
show (S n) = "I" ++ (Main.show n)
But there is no way to prioritize functions. I guess this is sane as you would otherwise need to track all names in all namespaces to understand the code correctly. However, there is the %hide <func> directive that removes access to a function. To still access it in other circumstances you could first rename it:
module Main
PLshow : Show ty => ty -> String
PLshow = Prelude.Show.show
%hide Prelude.Show.show
show : Nat -> String
show Z = ""
show (S n) = "I" ++ (show n)
foo : String
foo = PLshow 'a'