How would the compiler determine, in this case, that the programmer didn't need the fancier to_lower case function?

At best the compiler could ASK the programmer about it.

It's possible to design a standard library which makes it obvious to the user when a function allocates memory under the hood, for instance by taking an allocator argument. That way it becames very clear what "simple" functions are potentially expensive, and writing potentially slow code should be much less convenient than writing potentially fast code so that users are pushed to writing fast code, same as Rust pushes them to write memory-safe code.

In Rust to_lowercase returns a String, which is an owned struct with heap allocated data, so it is reasonably clear that it allocates. In contrast, trim_start for example returns a reference to a string slice with the same lifetime as the source string, so again it is reasonably obvious from the type signature what's going on.

The mistake here really is trying to do case insensitive string comparison by converting both arguments to the same case, then comparing them with case-sensitivity. It is much better to compare them directly, but case-insensitively.

This is sorta Zig’s wheelhouse.

Roughly how would you write code to solve this particular problem in your ideal language?

Zig has a very simple and straightforward solution: Every standard library function which needs to allocate takes an allocator argument. That way it's immediately obvious what functions are potentially expensive. It's not even a magic compiler or language feature, just a standard library convention.

Just like I described, detailing the problem in the type system, simplifying the abstractions and proving correctness of code.

That's a lovely ideal, but could you write some pseudocode for this particular problem in such a language?

That is beside the point. I could produce something in Haskell, but the "magic" would all done in the compiler, so in the context of my original comment I see no reason why I should.

> At code level, you should be able to describe your problem in lots of details, use identities to simplify your logic, but leave the optimizations to the compiler.

1. As far as I'm aware, Haskell isn't able to do any of that at the code level. I'm interested in what a language that is able to do that would look like.

2. I'm curious as to what you consider an "optimization" to be left to the compiler, and what you consider part of the "problem". For example, does the compiler decide which implementation of a set to use?

3. I'm also wondering what you mean by "proving correctness." If you're alluding to formal verification, then that is notoriously hard to scale, which conflicts with the stated goal of making optimization easier to scale.

Some pseudocode would shed light on all these questions.

I guess I have to admit I punched above my pay grade. Because I can't think of a pseudocode that would shed light to those questions.