Does Standard ML validate (CBV) eta equivalence?
@xuq01's guess is (extremely surprisingly!) wrong. The CBV eta rule described in the question is sound in Standard ML: the value v is contextually equivalent to fn x =&gt; v x. 

There are two caveats to this.


First, in specific implementations this equivalence might not be sound: in SML/NJ, you could use Unsafe.cast to detect physical equality of function values. However, unsafe features are not part of the standard. 
Second, eta with functions and sums interacts in a slightly subtle way, due to clausal definitions and incomplete pattern matching. In particular, the definitions:

fun f (SOME x) (SOME y) = x + y


and

val g = fn (SOME x) =&gt; (fn (SOME y) =&gt; x + y)


are not contextually equivalent. This is because the call f NONE will return a function, and g NONE will raise an error. 

- f NONE;
val it = fn : int option -&gt; int

- g NONE;
uncaught exception Match [nonexhaustive match failure]
raised at: stdIn:2.32


The reason this happens is operationally obvious, and of course a call-by-push-value/polarization setup makes this choice explicable. But if you really want to seriously understand clausal definitions, you are led to the idea that clausal definitions should be primary, and the usual term formers should be derived notions. See Abel, Pientka, Thibodeau and Setzer's Copatterns: programming infinite structures by observations for an example of a polarized calculus in this style. (See also Paul Levy's Jumbo Lambda-Calculus, for another calculus based on this observation.)