The closure being used as the task function in this example is formally isolated to the main actor. Under this proposal, the tasks will be synchronously enqueued on the main actor, which is FIFO, and then they'll switch immediately to counter, and since they all have the same priority, they'll run in their original order. Now, this proposal allows for optimization; since the closure isn't explicitly isolated to the main actor, Swift could skip enqueuing on the main actor and go direct to counter. That's actually still fine for this example unless Swift somehow does that inconsistently for different closures in the loop, which would be weird but technically possible. You could guarantee that doesn't happen by explicitly isolating the closure, in this case preferably to counter.
If the current function wasn't @MainActor, the closure would be formally non-isolated, and you'd have to explicitly isolate it (again, preferably to counter) to get an ordering guarantee. The upshot is that, if you want the ordering guarantee, you should be explicit about the isolation of your tasks.