A first-order structure $M$ is Leibnizian, if any two distinct elements $a,b\in M$ satisfy different $1$-types; that is, if there is some formula $\varphi$ such that $M\models\varphi(a)$ and $M\models\neg\varphi(b)$. Thus, a Leibnizian model is one in which you can distinguish any two elements by properties expressible in the language, or to put it differently, a Leibnizian model is one in which indiscernibles are identical.
In contrast, a structure $M$ is pointwise definable, if every individual element $a\in M$ is definable in $M$, so that there is some formula $\varphi(x)$ which is satisfied in $M$ only at $x=a$.
Every pointwise definable model is Leibnizian, of course, since elements can be distinguished by their defining characteristics. But in general, the concepts are distinct:
A Leibnizian model with non-definable elements (infinite language). In the language with infinitely many constant symbols $c_0,c_1,\ldots$, consider a model $M$ interpreting them all differently and having exactly one additional point, which is not the interpretation of any constant. This model is Leibnizian, since for any two points, one of them is one of the constants and hence definable. But the single extra point is not definable in $M$, because any formula $\varphi$ uses only finitely many of the constant symbols, and hence cannot define that point, because in the reduct of the model to the language of $\varphi$, there are automorphisms that permute all the other points not named by a constant in $\varphi$. Note that most of the elements of this model are definable. (Alternatively, one could take an elementary extension of the model and note that all the unnamed points will be automorphic.)
A Leibnizian model with no definable elements (infinite language). Consider the model $\langle 2^\omega,U_s\rangle_{s\in 2^{<\omega}}$, where the domain is Cantor space $2^\omega$, the set of all infinite binary sequences, and the predicate $U_s(z)$ holds exactly when $z$ begins with the finite string $s$. So this is Cantor space with predicates for the basic open sets. The model is Leibnizian, since any two distinct $y,z$ in Cantor space must disagree on some $U_s$. But the model has no definable elements at all, because any formula $\varphi(x)$ uses only finitely many predicates $U_s$, and the reduction of the model to that language has numerous automorphisms with no fixed points: one can flip bits on any coordinate beyond the length of any $s$ that appears in $\varphi$.
A Leibnizian model with non-definable elements (finite language). Consider the language with just one unary function symbol $S$, and form the CandyLand model (named by Arden Koehler), which has one lollipop of every finite size, plus one infinite lollipop stick. More precisely, the model has infinitely many base point elements $x_1,x_2,x_3,\ldots$ plus one more $x_\infty$, such that none of them is in the range of $S$, and furthermore, the function $S$ applied to base point $x_n$ iterates for exactly $n$ steps before finding a fixed point, and where $S^k(x_\infty)$ never repeats. $$x_1\neq S(x_1)=S^2(x_1),\qquad x_n\neq S^k(x_n)\neq S^n(x_n)=S^{n+1}(x_n)\quad(k<n)$$ So $x_n$ is the base of a size $n$ lollipop. Note that every element on a finite lollipop is definable by the number of times that $S$ may be applied in reverse and the number of forward iterates necessary to reach the fixed point. So those points can be distinguished from any other in the model; and any two distinct points on the infinite lollipop can be distinguished by their height, the number of times $S$ can be reversed from them. So the model is Leibnizian. But meanwhile, none of the elements on the infinite lollipop is definable. To see this, use a compactness/upward Löwenheim-Skolem argument to find an elementary extension of $M$ that has at least one additional infinite lollipop with a base point, and then note that the two infinite lollipops are automorphic, and so contain no definable elements. (Alternatively, one can show that the structure admits elimination of quantifiers down to the language of $S$ together with the predicates $H_n(x)$ that assert that $x$ has height $n$, meaning that $S$ can be inverted exactly $n$ times but not more from $x$, but no quantifier-free assertion in this language can define the base point of the infinite lollipop.)
My question is whether we can have it all:
Question. Is there a first-order structure $M$ in a finite language, such that $M$ is Leibnizian, but has no definable elements?
Having an elementary example would help to clarify a certain issue on which Arden Koehler, a graduate student in my seminar this semester, is writing.