idris - Helper Function to Determine if Nat `mod` 5 == 0

Question

Xash provided me with a helpful answer on Function to Determine if Nat is Divisible by 5 at Compile-Time (that I re-named from my original long name):

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

A previous answer educated me how to run it on the REPL using the Refl argument:

-- 5 % 5 == 0, so it should compile
*Test> onlyModBy5 5 Refl
5 : Nat 

-- 7 % 5 == 2, so it should not compile
*Test> onlyModBy5 7 Refl
(input):1:12:When checking an application of function Main.onlyModBy5:
        Type mismatch between
                x = x (Type of Refl)
        and
                modNat 7 5 = 0 (Expected type)

        Specifically:
                Type mismatch between
                        2
                and
                        0

Then, I tried to define a helper function that would provide the second prf (proof) argument for conciseness. In other words, I'd prefer the caller of this function to not have to provide the Refl argument.

onlyModBy5Short : (n : Nat) -> Nat
onlyModBy5Short n = onlyModBy5 n Refl

But, it does not compile:

When checking right hand side of onlyModBy5Short with expected type
        Nat

When checking an application of function Main.onlyModBy5:
        Type mismatch between
                0 = 0 (Type of Refl)
        and
                modNat n 5 = 0 (Expected type)

        Specifically:
                Type mismatch between
                        0
                and
                        Prelude.Nat.modNatNZ, mod' n 4 SIsNotZ n n 4
Holes: Main.onlyModBy5Short

How, if possible, can this function be written?

Answer 1

You can make onlyModBy5's second argument an auto argument:

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

This works because for a given literal value of n, n `modNat` 5 can always be reduced, and so n `modNat` 5 = 0 will always reduce to 0 = 0 (in which case the constructor Refl has the right type) unless n is truly not divisible by 5.

Indeed, this will allow you to typecheck

foo : Nat
foo = onlyModBy5 25

but reject

bar : Nat
bar = onlyModBy5 4