I'm trying to implement Binomial Heaps in Idris, so I defined a type
data Bin = MSEnd | B0 Bin | B1 Bin
where MSEnd stands for "Most Significant End" (e.g. B0 (B1 (B1 MSEnd)) represents 6).
I also defined a function to add them together. I have tested this, and it works as expected
(as does the helper function succ, which increments a binary number).
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
However, in a different function whose type signature is dependent on this plus function, I get the compiler error
Type mismatch between
b1
and
plus b1 MSEnd
Based on the definition of plus, it seems like the Idris compiler should easily be able to determine that these are equal. What is wrong here?