Consider the following (very simplified) example of constraining a datatype via a side-condition on its values:
data Transport = Car | Foot | Boat
total wheels : (transport : Transport) -> {auto hasWheels : transport = Car} -> Int
wheels Car {hasWheels = Refl} = 4
wheels Foot {hasWheels = Refl} impossible
wheels Boat {hasWheels = Refl} impossible
Is there any way I can leave out or summarise the impossible cases and still have Idris see the function as total? If I do leave a case out I get something like
Main.wheels is not total as there are missing cases
I also can't just have a catch-all case as the compiler doesn't know that the _ can't be Car so the second line doesn't type-check:
wheels Car {hasWheels = Refl} = 4
wheels _ {hasWheels = Refl} impossible
This gives
wheels _ is a valid case
I've looked through the ideas in this post about constraining datatypes but I don't see any approaches that help.
In the real code this is simplified from, there are a lot of cases which each need to be discharged separately, making it very unwieldy.
I looked more carefully into the approaches discussed in the question I already linked and some of them do actualy allow cases to be omitted completely.
I came up with the following that seems best suited to my actual use case where the real conditions are more complicated:
isCar : Transport -> Bool
isCar Car = True
isCar _ = False
BoolToType : Bool -> Type
BoolToType True = ()
BoolToType False = Void
total wheels
: (transport : Transport)
-> {auto hasWheels : BoolToType (isCar transport)}
-> Int
wheels Car = 4
However I don't really understand why Idris is happy to omit the impossible patterns here but not in my original code, so an answer that really explains what's going on would still be very helpful.