How Can I Check For A Value Not Being In A Set?

Question

I'm trying to use TLA+ to model a system. This is a simplified version of the model I'm trying to build; I'm posting the simplified version because I think it's adequate to demonstrate my question:

---- MODULE demonstrate_question ----

VARIABLE msg_queue

vars == <<msg_queue>>

request == {"request"}
response == {"response"}

InsertToQueue(message, queue) ==
    queue \union message

RemoveFromQueue(message, queue) ==
    queue \ message

IsMessageInQueue(message, queue) ==
    message \in queue

MessageNotInQueue(message, queue) ==
(* Also tried ~(IsMessageInQueue(message, queue)); also failed *)
    message \notin queue

NewMessage(message, queue) ==
(* Also tried /\ message \notin queue; failed *)
    MessageNotInQueue(message,msg_queue)

Init ==
    /\ msg_queue = {} 


RequestReceived(message) ==
    /\ NewMessage(message, msg_queue)
    /\ msg_queue' = InsertToQueue(message, msg_queue)

Next ==
    \/ RequestReceived(request)

Spec == Init \/ [][Next]_vars    
====

When I attempt to check the model I get this error:

The exception was a java.lang.RuntimeException
: Attempted to compare the set {"request"} with the value:
"request"

And the stack trace points to the NewMessage call inside RequestReceived. In fact I can comment out the NewMessage call and there's no error. I want the NewMessage call to insure it's not a message I've already got in the queue.

Any suggestions of what I might do to check to see if a particular value is not in a set? I'm testing this with VSCode and I have the feeling that either VSCode or the TLC model checker is caching some things but I'm not sure that factors in here.