Gödel's speed-up theorem implies that some proofs can get significantly shortened when allowing extra axioms. There are concrete examples of this phenomenon for instance when moving from Peano arithmetic (PA) to PA + consistency(PA), or when moving from PA to second-order arithmetic, see for instance this question.

However, I am not aware of concrete examples of such a dramatic shortening when moving from constructive logic to classical logic.

So, is there a known example of a statement that is both true in constructive and classical logic, that has a reasonably short proof in classical logic, but such that any proof in constructive logic would be gigantic (and thus not "human-readable")?

Ideally, an example would be a statement that would feel "concrete enough" for the average mathematician, i.e. a statement involving numbers, graphs, algebraic structures, etc. (Friedman's examples on Kruskal's tree theorem fit the bill)

(I would also be interested in an example that has a simple proof in classical logic, that is not yet known to be true in constructive logic but such that a proof, if it exists, must be gigantic.)