Автоматический неявный аргумент перестает работать, когда типу присваивается имя

При написании этого ответа я заметил, что пока это работает как положено:

onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat
onlyModBy5 n = n

foo : Nat
foo = onlyModBy5 25

но как только я даю имя свойству, оно перестает работать:

Divides : Nat -> Nat -> Type
Divides n k = k `modNat` n = 0

onlyModBy5 : (n : Nat) -> {auto prf : 5 `Divides` n} -> Nat
onlyModBy5 n = n

foo : Nat
foo = onlyModBy5 25

теперь заполнение аргумента auto не выполняется

Can't find a value of type 
        Divides 5 25

Почему Идрис не может понять определение Divides?


idris leaky-abstraction
person Cactus    schedule 11.04.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Я не уверен, что это причина, но modNat не является тотальным. Это был бы хороший повод споткнуться об Идрис.

divides : Nat -> Nat -> Nat
divides n k = n `modNat` k

onlyModBy5 : (n : Nat) -> {auto prf : n `divides` 5  = 0 } -> Nat
onlyModBy5 n = n

foo : Nat
foo = onlyModBy5 25

По какой-то причине это тоже уже терпит неудачу (просто коснувшись один раз из исходной версии).

person Markus    schedule 11.04.2016