Why isn't equality involving “mods” not typecheck in Idris?

Question

Why the following typecheck will not look:

v1 : mod 3 2 = 1
v1 = Refl

But it will look great:

v2 : 3 - 2 = 1
v2 = Refl

Answer 1

This is due to the addiction of the function mod(thanks to @AntonTrunov's explanation ). These are polymorphic and default constant numbers Integers.

Idris> :t mod
mod : Integral ty => ty -> ty -> ty
Idris> :t 3
3 : Integer
Idris> :t mod 3 2
mod 3 2 : Integer

For Integera type function is modnot common.

Use instead modNatNZ, so all types are perfectly validated and work.

v1 : modNatNZ 3 2 SIsNotZ = 1
v1 = Refl