依赖类型上的函数不是total，但idris认为它是total

Question

我有一个取决于PowerSource类型的Vehicle类型：

data PowerSource = Petrol | Pedal | Electric

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

和函数wheels。Tram是一个未处理的案例。

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

当我从REPL检查wheels的全面性时，

:total wheels
Main.wheels is Total

因为我没有在wheels中处理Tram类型，所以我不明白wheels怎么可能是total。我误解了“全部”是什么意思吗？

Answer 1

这是因为在wheels Motorcycle中，它把Motorcycle当作一个变量，因为它不是构造函数应用程序的好类型-- Motorcycle构造函数接受一个参数。

事实上，这通过了类型检查器，这是相当令人惊讶的，我认为这实际上是Idris设计中的一个(可修复的)错误。为了避免这种错误，我认为它应该只允许以小写字母开头的模式变量自动绑定，就像绑定类型变量一样。