idrisleaky-abstraction

Auto implicit arg stops working when type is given a name

While writing this answer, I noticed that while this works as expected:

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

foo : Nat
foo = onlyModBy5 25

but as soon as I give a name to the property it stops working:

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

now filling the auto arg fails with

Can't find a value of type 
        Divides 5 25

Why is Idris unable to see through Divides's definition?

Solution

  • I am not sure if this is the reason, but modNat is not total. That would be a good reason to trip idris.

    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

    For some reason this already fails as well (just indirecting once from the original version).