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 Int
s:
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)
^^^^^