Idris interpreting nonlinear argument as linear

109 views Asked by At

I'm working from the TDD with idris book using Idris2, and in Chapter 6 we write a function that adds a dynamic amount of numbers to each other. This is my impl with only Ints:

AdderType : (numargs : Nat) -> Type
AdderType Z = Int
AdderType (S k) = Int -> AdderType k

adder : (numargs : Nat) -> Int -> AdderType numargs
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)

Note that the (S k) case of adder returns a lambda. I tried to just add next to the arguments of adder:

adder : (numargs : Nat) -> Int -> AdderType numargs
adder Z acc = acc
adder (S k) acc next = adder k (next + acc)

But when I try to compile this idris2 gives me the following error.

Error: 
While processing right hand side of adder. 
Trying to use linear name next in non-linear context.

 24 | adder : (numargs : Nat) -> Int -> AdderType numargs
 25 | adder 0 acc = acc
 26 | adder (S k) acc next = adder k (next + acc)
                                      ^^^^

Why does idris2 decide that next is linear in this case without me explicitly saying it is? Is this a bug?

Note: If I do the same for the more generic impl listed in the book:

AdderType : (numargs : Nat) -> Type -> Type
AdderType Z numType = numType
AdderType (S k) numType = (next : numType) -> AdderType k numType

adder : Num numType => (numargs : Nat) -> numType -> AdderType numargs numType
adder Z acc = acc
adder (S k) acc next = adder k (next + acc)

I get the following error:

Error: While processing left hand side of adder. Unsolved holes:

Tri.{argTy:4060} introduced at:
/home/stefan/dev/tdd-idris/Tri.idr:25:1--25:6
 21 | AdderType (S k) numType = (next : numType) -> AdderType k numType
 22 |
 23 | adder : Num numType => (numargs : Nat) -> numType -> AdderType numargs numType
 24 | adder Z acc = acc
 25 | adder (S k) acc next = adder k (next + acc)
      ^^^^^
0

There are 0 answers