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

Question

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)

Answer 1

This can be achieved by introducing new VehicleType data type and by adding one more parameter to Vehicle like this:

data VehicleType = BicycleT | CarT | BusT

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

You should somehow encode in type difference between constructors. If you want more type safety you need to add more information to types. Then you can use it to implement refuel function:

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

Replacing

refuel (Car fuel) x        = Car (fuel + x)

with

refuel (Car fuel) x        = Bus (fuel + x)

leads to next type error:

Type checking ./Fuel.idr
Fuel.idr:14:8:When checking right hand side of refuel with expected type
        Vehicle Petrol CarT

Type mismatch between
        Vehicle Petrol BusT (Type of Bus fuel)
and
        Vehicle Petrol CarT (Expected type)

Specifically:
        Type mismatch between
                BusT
        and
                CarT

Answer 2

Another possibility is to do what you want externally. It might be an option when you cannot change the original type, e.g. if it comes from a library. Or if you do not want to clutter your type with too many extra indices which you might want to add to state more properties.

Let us reuse the VehicleType type introduced by @Shersh:

data VehicleType = BicycleT | CarT | BusT

Now, let's define a function which tells us which constructor was used to construct a vehicle. It allows us to state our property quit consice:

total
vehicleType : Vehicle t -> VehicleType
vehicleType Bicycle = BicycleT
vehicleType (Car _) = CarT
vehicleType (Bus _) = BusT

And now we can say that refuel preserves the type of a vehicle:

total
refuelPreservesVehicleType : vehicleType (refuel v x) = vehicleType v
refuelPreservesVehicleType {v = (Car _)} = Refl
refuelPreservesVehicleType {v = (Bus _)} = Refl