If your spec were correct, TLC would not be able to handle it because
of a long-standing bug: it doesn't correctly handle parametrized
instantiation. I suspect that this bug is not hard to fix, but there
have always been more pressing issues to handle. It would make a nice
project for someone who wants to help.
However, your spec seems to have the same error that Stephan
pointed out in Bekir's example. If you didn't understand Stephan's
explanation, try the one at around 11 minutes 40 seconds of the 5th
TLA+ video lecture.
Leslie