我可以避免在Idris的全部函数中明确释放无效案例吗？

Question

考虑以下（非常简化的）示例，该示例通过在其值上附带条件来约束数据类型：

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

我有什么办法可以忽略或总结impossible个案例，而Idris仍然认为该函数是合计的？如果我不提案件，我会得到类似的信息

Main.wheels is not total as there are missing cases

我也不能只是一个包罗万象的案例，因为编译器不知道_不能是Car，所以第二行不进行类型检查：

wheels Car {hasWheels = Refl} = 4
wheels _ {hasWheels = Refl} impossible

这给

wheels _ is a valid case

我浏览了this post about constraining datatypes中的想法，但没有找到任何有用的方法。

在实际代码中，这已简化，很多情况下每种情况都需要分别处理，这非常麻烦。

Answer 1

我更仔细地研究了question I already linked中讨论的方法，其中一些确实确实允许完全省略情况。

我想出了以下似乎最适合我的实际用例的情况，其中实际条件更加复杂：

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

但是我并不真正理解为什么Idris很乐意在这里省略不可能的模式，而在我的原始代码中却没有，所以真正解释正在发生的事情的答案仍然会非常有帮助。