У Идриса проблемы с вложенными авто-имплицитами? - PullRequest
Новая
       22

У Идриса проблемы с вложенными авто-имплицитами?

0 голосов
/ 20 июня 2019

Я пишу интерфейс для частичных моноидов следующим образом: 

infixr 9 <>
interface PartialMonoid (m : Type) where
     compatible : m -> m -> Bool
    (<>) : (a : m) -> (b : m) -> {auto p : compatible a b = True} -> m

С простой реализацией в качестве доказательства концепции: 

data MyPos : Type where
   A : MyPos
   B : MyPos
   C : MyPos

op : (a : MyPos) -> (b : MyPos) -> Bool
op A A = True
op B B = True
op C C = True
op A B = True
op B A = True
op A C = True
op C A = True
op x y = False

PartialMonoid MyPos where
   compatible = op
   A <> A = A
   B <> B = B
   C <> C = C
   A <> B = B
   A <> C = C
   C <> A = C
   B <> A = B
   (<>) B C {p = Refl} impossible
   (<>) C B {p = Refl} impossible

Всякий раз, когда я пытаюсь оценить что-то вроде A <> B в REPL, я получаю ожидаемое поведение. Однако при оценке (например) (A <> B) <> A вместо ожидаемого A я получаю 

Type mismatch between
            MyPos (Type of A)
    and
            compatible A B = True (Expected type)

Это сбивает с толку меня, потому что если в REPL я делаю: 

:let x = (A <> B)
x <> A

тогда я получаю ожидаемое B.

Что здесь происходит? И если это какая-то проблема с моим кодом, а не ошибка, есть ли способ заставить такую ​​частичную моноидную операцию с неявным аргументом «совместимости» работать так, как можно было бы ожидать в Idris? (т.е. все идет гладко, пока вы не попытаетесь объединить два несовместимых элемента - например, B <> C выдает ошибку типа)

...