Я пытаюсь реализовать биномиальные кучи в 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 должен легко определить, что они равны. Что здесь не так?