The Hahn-Banach theorem is rightly seen as one of the Big Theorems in functional analysis. Indeed, it can be said to be where functional analysis really starts. But as it's one of those "there exists …" theorems that doesn't give you any information as to how to find it; indeed, it's quite usual when teaching it to introduce the separable case first (which is reasonably constructive) before going on to the full theorem. So it's real use is in situations where just knowing the functional exists is enough – if you can write down a functional that does the job then there's no need for the Hahn-Banach Theorem.
So my question is: what's a good example of a space where you need the Hahn-Banach theorem?
Ideally the space itself shouldn't be too difficult to express, and normed vector spaces are preferable to non-normed ones (a good non-normed vector space would still be nice to know but would be of less use pedagogically).
Edit: It seems wrong to accept one of these answers as "the" answer so I'm not going to do that. If forced, I would say that $\ell^\infty$ is the best example: it's probably the easiest non-separable space to think about and, as I've learnt, it does need the Hahn-Banach theorem.
Incidentally, one thing that wasn't said, and which I forgot about when asking the question, was that such an example is by necessity going to be non-separable since countable Hahn-Banach is provable merely with induction.
Best Answer
I'd like to summarize the answer that has developed from Eric Shechter's book, via Mark Meckes, plus the remark from Gerald Edgar. Since it's not really my answer, I'm making this a community answer.
The Hahn-Banach theorem is really the Hahn-Banach axiom. Like the axiom of choice, Hahn-Banach cannot be proved from ZF. What Hahn and Banach proved is that AC implies HB. The converse is not true: Logicians have constructed axiom sets that contradict HB, and they have constructed reasonable axioms strictly between AC and HB. So a version of Andrew's question is, is there a natural Banach space that requires the HB axiom? For the question, let's take HB to say that every Banach space $X$ embeds in its second dual $X^{**}$.
As Shechter explains, Shelah showed the relative consistency of ZF + DC + BP (dependent choice plus Baire property). As he also explains, these axioms imply that $(\ell^\infty)^* = \ell^1$. This is contrary to the Hahn-Banach theorem as explained in the next point. A striking way to phrase the conclusion is that $\ell^1$ and its dual $\ell^\infty$ become reflexive Banach spaces.
$c_0$ is the closed subspace of $\ell^\infty$ consisting of sequences that converge to 0. The quotient $\ell^\infty/c_0$ is an eminently natural Banach space in which the norm of a sequence is $\max(\lim \sup,-\lim \inf)$. (Another example is $c$, the subspace of convergent sequences. In $\ell^\infty/c$, the norm is half of $\lim \sup - \lim \inf$.) The inner product between $\ell^1$ and $c_0$ is non-degenerate, so in Shelah's axiom system, $(\ell^\infty/c_0)^* = 0$. Without the Hahn-Banach axiom, the Banach space $\ell^\infty/c_0$ need not have any non-zero bounded functionals at all.