Why doesn't equality involving "mod" not typecheck in Idris?

4
votes

Why won't the following typecheck:

v1 : mod 3 2 = 1
v1 = Refl

Yet this will typecheck fine:

v2 : 3 - 2 = 1
v2 = Refl
1
dependent-typeidris

1 Answers

5
votes

It happens due to partiality of mod function (thanks to @AntonTrunov clarification). It's polymorphic and by default numeral constants are 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 Integer type mod function is not total.

Instead use modNatNZ function so everything type checks perfectly and works.

v1 : modNatNZ 3 2 SIsNotZ = 1
v1 = Refl