The constructive axiom of choice is fine.
It's quite subtle, Per Martin-Löf:
"There is therefore a need to investigate how the constructive axiom of choice, validated by the Brouwer-Heyting-Kolmogorov interpretation, is related to Zermelo’s axiom of choice ..."
https://michaelt.github.io/martin-lof/One-hundred-years-of-Z...