Idris: totality check fails when trying to re-implement fromInteger for Nat

user_7318794 0
Viewed 173

I have the following code:

module Test
  data Nat' = S' Nat' | Z'
  Num Nat' where
    x * y = ?hole
    x + y = ?hole
    fromInteger x = if x < 1 then Z' else S' (fromInteger (x - 1))

I get an error message about the last line:

Test.idr:6:5:
Prelude.Interfaces.Test.Nat' implementation of Prelude.Interfaces.Num, method fromInteger is
possibly not total due to recursive path Prelude.Interfaces.Test.Nat' implementation of
Prelude.Interfaces.Num, method fromInteger --> Prelude.Interfaces.Test.Nat' implementation of
Prelude.Interfaces.Num, method fromInteger

The function should always give a result, because eventually the argument of fromInteger will become small enough to pick the first case. But Idris does not seem to understand this. What is wrong with this function, and how can I fix this error?

totality idris static-analysis recursion
1 Answers
Related