Search code examples
dependent-typeidris

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

Why won't the following typecheck:

v1 : mod 3 2 = 1
v1 = Refl

Yet this will typecheck fine:

v2 : 3 - 2 = 1
v2 = Refl
Solution

  • 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