How to constraint input type and output type to be the same?

I am going through Type driven development with Idris from Manning. An example is given that teaches how to restrict a function to a given type in a family of types. We have Vehicle type that uses PowerSource that is either Pedal or Petrol and we need to write a function refill that typechecks only for vehicles that use petrol as their powersource.

The below code works, but does not guarantee that refilling a Car will produce a Car and not a Bus. How do I need to change the signature of the refill function to only allow producing Car when given a Car and producing Bus when given Bus?

data PowerSource
  = Pedal
  | Petrol

data Vehicle : PowerSource -> Type 
  where
    Bicycle : Vehicle Pedal
    Car : (fuel : Nat) -> Vehicle Petrol
    Bus : (fuel : Nat) -> Vehicle Petrol

refuel : Vehicle Petrol -> Nat -> Vehicle Petrol
refuel (Car fuel) x        = Car (fuel + x)
refuel (Bus fuel) x        = Bus (fuel + x)