依赖类型的功能不是全部的，但 idris 认为它​​是全部的

Question

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

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。我是不是误解了 'total' 的意思？

Answer 1

这是因为在 wheels Motorcycle 中它将 Motorcycle 视为变量，因为它作为构造函数应用程序的类型不正确 - Motorcycle 构造函数采用参数。

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