Cannot prove alterations to a sequence of objects in Dafny 4

This method is not able to be verified when called within Main().

method closeCarPark(Spaces: seq<ParkingSpace>) returns (newSpaces: seq<ParkingSpace>)
      modifies set space | space in Spaces
   {
      var i := 0;

      while i < |Spaces|
         invariant 0 <= i <= |Spaces|
      {

         Spaces[i].setOccupied(0);

         i := i + 1;
      }

      return Spaces;
   }

How im calling that:

carPark.Spaces := carPark.closeCarPark(carPark.Spaces);

My parking space constructor:

class ParkingSpace {    var SpaceID: int    var Occupied: int    var Reservation: string    var Location: string    var Car: Car?    ghost var repr: set<object>
    
       constructor(id: int, filled: int, reservation: string, location: string) 
          requires id != 0
          requires filled == 0 || filled == 1
          requires (location == "Regular" || location == "Subscription") && location != ""
          requires (reservation == "None" || |reservation| == 7) && reservation != "" 
          requires forall i :: 0 <= i < |reservation| ==> ('a' <= reservation[i] <= 'z' || 'A' <= reservation[i] <= 'Z' || '0' <= reservation[i] <= '9')    {
          SpaceID := id;
          Occupied := filled;
          Reservation := reservation;
          Location := location;
          Car := null;
    
          this.repr := this.repr + {this};    }
    
       method setOccupied(count: int) 
            modifies this
            ensures this.Occupied == count;
        {
            this.Occupied := count;
        }
    
    }

I get an error informing me that the declaration could not be proved. More specifically, removing 'modifies Spaces' and the code which changes the objects property enables verification, why cant it prove that Spaces is being Modified?

Sets and seqs are immutable in Dafny regardless of versions. Classes are not immutable and are expected to be heap objects so you have to specify that they will be modified.

class ParkingSpace {
    var Occupied: int;
    ghost var repr: set<object>

    constructor(val: int)
    {
        this.Occupied := val;
        this.repr := this.repr + {this};
    }

    method setOccupied(count: int) 
        modifies this
        ensures this.Occupied == count;
    {
        this.Occupied := count;
    }
}

//Edit:
method closeCarPark(Spaces: seq<ParkingSpace>) returns (newSpaces: seq<ParkingSpace>)
        requires forall i :: 0 <= i < |Spaces| ==> Spaces[i].Occupied != 0;
      modifies set space | space in Spaces
      ensures forall i :: 0 <= i < |Spaces| ==> Spaces[i].Occupied == 0
   {
      var i := 0;

      while i < |Spaces|
        invariant 0 <= i <= |Spaces|
        invariant forall k :: 0 <= k < i ==> Spaces[k].Occupied == 0
      {

         Spaces[i].setOccupied(0);

         i := i + 1;
      }

      return Spaces;
   }

Edit: To your second question, modifies is not an assertion to be proved. It is a permission that allows a method to modify a set of heap objects. In Dafny, you can make an assertion that a value as changed with the old() operator. You can also just assert that a value is different. In Dafny, the requirements are all that it knows. So I made a version where it requires the occupied to start out as not zero and then we can verify that closeCarPark sets all the values to 0.