Misleading import error message when imports are duplicated with different casing

Description

import Std.Data.BitVec.Basic
import Std.Data.Bitvec.Basic -- ``Bitvec`` should have been ``BitVec``

Fails with

import Std.Data.Bitvec.Basic failed, environment already contains 'Std.BitVec.smod._cstage1' from Std.Data.BitVec.Basic

while it should have done nothing, or it should have failed with

no such file or directory (error code: 2): ....../Std/Data/Bitvec/Basic.lean

Note that import Std.Data.Bitvec.Basic alone does not fail, so it could be the case that there are two files, one importing BitVec and another importing ``Bitvec```. Both file would successfully build, but when another file imports both files, the above error would occur. Such behavior could be confusing.

Versions

Lean (version 4.2.0-rc4, commit 819b5eaceaa4, Release)
Ubuntu 20.04.6 LTS(WSL)
Std4: ab21923ce1717d48a8d3d17e77bf6cdd3122eed8

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the issue with the two imports shown in the report, and compare it with importing the misspelled path alone. Trace the import-resolution and duplicate-environment handling involved; done means the casing mistake produces the intended missing-file error or is safely ignored rather than a misleading duplicate-environment error.