What's an example of a space that needs the Hahn-Banach Theorem? 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.
 A: 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.
A: There is another logical tidbit here.
Hahn-Banach (HB) is strictly weaker than Axiom of Choice (AC), meaning--under the assumption of consistence as usual--in ZF, AC implies HB but not the other way around.  Another intermediate theorem of functional analysis is the Krein-Milman theorem: "A compact convex nonempty set in a locally convex space has an extreme point"  Call it KM.  In ZF, AC implies KM but not the other way around.  And the interesting point is that, taken both together, we do get AC.  So in ZF, HB+KM implies and is implied by AC.
A: I don't fully understand what you're asking, but the one proof I know of the fact that (up to topological isomorphism) the only complete Archimedean fields are $\mathbb{C}$ and $\mathbb{R}$ uses the Hahn-Banach theorem.
A: I'm not sure exactly what you have in mind by "need the Hahn-Banach theorem".  One standard example of something pretty concrete for which Hahn-Banach in some form is needed is to show that there are linear functionals on $\ell^\infty$ which are not represented by elements of $\ell^1$.  It's a standard exercise to show that $\ell^1$ acts as the dual of sequences converging to 0; since that is a proper closed subspace of $\ell^\infty$, Hahn-Banach produces further linear functionals on $\ell^\infty$.
This is closely related to the subject of Banach limits.
A: The Gelfand-Naimark theorem says that any $C^\ast$-algebra is isomorphic to a norm closed $\ast$-subalgebra of $B(H)$ for a suitable Hilbert space $H$. In order to prove this theorem, it is imperative that our $C^\ast$-algebra have states, which uses the Hahn-Banach theorem.
One can also use the Hahn-Banach theorem instead of Tychonoff's theorem to construct $\beta X$, the Stone-Cech compactification of $X$. This is closely related to @Mark Meckes' answer.
A: If $G$ is a group, Bavard showed that the stable commutator length vanishes on $[G,G]$ if and only if $G$ admits no nontrivial "homogeneous quasimorphisms". These functions (on the space of group $1$-boundaries) are constructed using the Hahn-Banach theorem, but are usually very hard (or impossible) to write down explicitly.
Another example: let $M$ be a triangulated manifold, and suppose we orient every edge of every simplex in such a way that the orientations come from a "total order" on each triangle. We would like to assign positive "lengths" to each edge in such a way that on each triangle, the sum of the values on the "short edges" is equal to the value on the "long edge" (where "short" and "long" are defined according to the orientations). The (finite-dimensional!) Hahn-Banach theorem tells us we can do this if and only if every oriented loop in the 1-skeleton is homologically essential; i.e. "homological positivity" can be improved to "chain positivity". Of course the finite-dimensional Hahn-Banach theorem is just a psychological crutch, but versions of this construction in other categories need the "real" Hahn-Banach theorem (applied to certain spaces of de Rham currents).
A: The simplest example I know are the real numbers as vector space over the rationals.
The Hahn-Banach theorem asserts the existence of additive functionals other than standard addition,
For instance, $f$ with $f(1)=1, f(\pi)=0$.
