If you redefine what others mean to fit your particular point, you will obviously be correct, yet you'll have failed to be correct to the intended meaning used by other people.

Using your definition of bug, take for example a function in an untyped language. Assuming a bug free implementation of the language, I can say that no matter what code I write, it will always be bug free, because the code will always do exactly what the code specifies, and the function made no statement to any particular behavior.

So if you define your "sort" to be a function that does what your Idris type specification defined it to do, yes your sort will be correct to it, assuming a bug free implementation of Idris and its type system, and that the type checker asserted it to be correct.

And yet, for the intended behavior to the users of the program and the objective it was meant to achieve it's very possible that your sort function doesn't work.

Or in other words take this Python code:

    def sort(array):
      return array

    print(sort([2,1,3]))
    [2,1,3]

Is this a bug? Or did I just mislabel the name of this function?

I feel like that's the gist of your argument. You're saying: it behaved correctly to the extent that I have formally specified it, which in the case of Python I have not formally specified anything so all behavior are valid and correct.

But what good is that?