Yes we are preparing (in the near future) to add a limited support
for uninterpreted String literals
For example, in a future version of Alloy4, you would be able to
write formulas like a.name = 'john' && b.name = 'peter'

However, the feature is not finished yet; when it's ready, we will announce it and provide
online examples and documentations for it (just like when we introduced the "seq" sequence type)

(In case you're curious, right now since there are no syntax yet for you
to create String atoms, that means the set of all String atoms is always empty,
and that's why your model says there's no instance)

Sincerely,
Felix Chang
Alloy4 Developer