Error: cannot establish the existence of LHS values that satisfy the such-that predicate

Here is example code that produces this error:

method PickKey<K, V>(m: map<K, V>) returns (ret: K) {
  var k :| k in m;
  return k;
}

When a such-that (:|) initialization is used, Dafny must be able to establish that there is at least one value that satisfies the predicate given on the RHS. That is, in this case, it must prove assert exists k :: k in m;. But for this example, if the map m is empty, there is no such value, so the error message results.

If you add a precondition that the map is non-empty, then the error is gone:

method PickKey<K, V>(m: map<K, V>) returns (ret: K) 
  requires |m.Keys| > 0
{
  var k :| k in m;
  return k;
}