better error/warning reporting when variable in pattern starts from a capital letter

[andreykl]

Example is from TTD book

data PowerSource = Pedal | Petrol | Electicity

data Vehicle : PowerSource -> Type where
  Unicyle : Vehicle Pedal
  Bicycle : Vehicle Pedal
  Motocycle : (fuel : Nat) -> Vehicle Petrol
  Car : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol
  Tram : Vehicle Electicity
  ElectricCar : Vehicle Electicity

total
wheels : Vehicle power -> Int
wheels Unicyle = 1
wheels Bicycle = 2
wheels Motocycle = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4

Idris says wheels is total, but not all cases are checked.
It is possible that order of cases has the influence, but i'm not sure.
It is possible related with #1917

[esmolanka]

The Motocycle pattern in wheels function is missing an argument, therefore it was parsed as a variable that basically captures everything except the cases Unicycle and Bicycle. So the function is indeed total. You can have a look on what was in fact parsed with :def wheels in REPL.

Parsing is confusing and probably have to be somehow fixed in this case (by throwing an error or a warning), but totality checker is correct.

[andreykl]

Thank you for your comment. Indeed.