Idris totality check

Question

I am compiling the following simple program using Idris2.

import Data.Fin

%default total

negate : {k:_} -> Fin k -> Fin k
subt : {k:_} -> Fin k -> Fin k -> Fin k
add : {k:_} -> Fin k -> Fin k -> Fin k

mult : {k:_} -> Fin k -> Fin k -> Fin k
mult FZ b = FZ
mult (FS a) b = add b $ mult (weaken a) b

However, the compiler spits an error:

Error: mult is not total, possibly not terminating due to recursive
path Main.mult -> Main.mult -> Main.mult

Isn't the recursive call on input a which is smaller than (FS a)? Why is the totality check failing?

Thanks!

Answer 1

I don't know why the compiler doesn't realize that weaken a is smaller than FS a, although I suspect that the problem is weaken.

You can work around it by asserting that weaken a is smaller than FS a:

module Misc

import Data.Fin

%default total

add : Fin k -> Fin k -> Fin k
add a b = ?add_rhs

mult : Fin k -> Fin k -> Fin k
mult FZ _ = FZ
mult a@(FS a') b = add b $ mult (assert_smaller a (weaken a')) b

Do note that under the usual definition of addition and multiplication on integers, the result could be larger than k. I assume your add implementation will take care of this.