Function on dependent type is not total, but idris thinks that it's total

Question

I have a Vehicle type depending on a PowerSource type:

data PowerSource = Petrol | Pedal | Electric

data Vehicle : PowerSource -> Type where
  Unicycle : Vehicle Pedal
  Motorcycle : (fuel: Nat) -> Vehicle Petrol
  Tram: (battery : Nat) -> Vehicle Electric

and a function wheels. Tram is an unhandled case.

wheels : Vehicle power -> Nat
wheels Unicycle = 1
wheels Motorcycle = 2

When I check the total-ness of wheels from the REPL,

:total wheels
Main.wheels is Total

As I did not handle the Tram type in wheels, I don't understand how wheels can be total. Am I misunderstanding what 'total' mean?

Edwin Brady Edwin Brady · Accepted Answer · 2017-07-11T17:06:10

This is because in wheels Motorcycle it's treating Motorcycle as a variable, because it isn't well typed as a constructor application - Motorcycle the constructor takes an argument.

The fact that this gets past the type checker is quite surprising, and I think this is actually a (fixable) mistake in the design of Idris. To avoid this kind of error, I think it should only allow pattern variables to be automatically bound if they begin with a lower case letter, in much the same way as type variables are bound.

Function on dependent type is not total, but idris thinks that it's total

1 Answers