我正在尝试在 Idris 中实现二项式堆，所以我定义了一个类型
data Bin = MSEnd | B0 Bin | B1 Bin
其中MSEnd代表“最重要的结束”（例如B0 (B1 (B1 MSEnd))代表6）。
我还定义了一个函数来将它们加在一起。我已经对此进行了测试，它按预期工作（辅助函数也是如此succ，它增加了一个二进制数）。
plus : Bin -> Bin -> Bin
plus MSEnd b = b
plus b MSEnd = b
plus (B0 a) (B0 b) = B0 $ plus a b
plus (B0 a) (B1 b) = B1 $ plus a b
plus (B1 a) (B0 b) = B1 $ plus a b
plus (B1 a) (B1 b) = B0 . succ $ plus a b
但是，在类型签名依赖于此plus函数的不同函数中，我得到编译器错误
Type mismatch between
b1
and
plus b1 MSEnd
根据 的定义plus，Idris 编译器似乎应该能够轻松确定它们是否相等。这里有什么问题？