bug in new code generator: recursive + inline + duplicate typeclass

[digama0]

inductive AssocList (α : Type u) (β : Type v) where
  | nil
  | cons (key : α) (value : β) (tail : AssocList α β)

namespace AssocList
variable {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m]

@[inline] protected def forIn [Monad m]
    (as : AssocList α β) (init : δ) (f : (α × β) → δ → m (ForInStep δ)) : m δ :=
  match as with
  | nil => pure init
  | cons k v es => do
    match (← f (k, v) init) with
    | ForInStep.done d  => pure d
    | ForInStep.yield d => es.forIn d f

instance : ForIn m (AssocList α β) (α × β) where
  forIn := AssocList.forIn

maximum recursion depth reached in the code generator
function inline stack:
AssocList.forIn

The given code is buggy for two reasons: It has an @[inline] attribute even though it is recursive, and the forIn function takes two instances of [Monad m] (one from the variable line and one from the declaration). These interact in some way to cause the stack overflow in the inliner.

[leodemoura]

We had similar incorrect annotations in the Init package. This is why I included the "function inline stack" in the error message in the new code generator We can revise the error message and suggest the user must remove the [inline] annotation from AssocList.forIn.

[digama0]

Would it be possible to give an error at the @[inline] attribute itself? Or is there a reason you would want to put @[inline] on recursive decls?

[leodemoura]

Would it be possible to give an error at the @[inline] attribute itself? Or is there a reason you would want to put @[inline] on recursive decls?

I considered adding the check, but gave up for now since the current code generator accepts it.
But, we have [inlineIfReduce] which is allowed in recursive declarations but it is harder to misuse because the compiler only inlines the code if the case can be reduced. Example:

@[inlineIfReduce]
def List.toArrayAux : List α → Array α → Array α
  | nil,       r => r
  | cons a as, r => toArrayAux as (r.push a)

If we decide to implement the check at declaration time, we should probably do it inside the code generator where we have access to all information: mutual recursion, recursion in computationally relevant parts, etc.

[digama0]

I think it would be good to give an error here if by some conservative check you can ensure that inlining will run away, which by my understanding would be any recursion at all (a loop in the call graph). You could also do a similar analysis for inlineIfReduce but it's a bit harder: for example, I believe this would run away even with inlineIfReduce:

@[inlineIfReduce] partial def loop (xs : List A) : List A :=
  match xs with
  | [] => []
  | x :: xs => loop (x :: xs)

[leodemoura]

I think it would be good to give an error here if by some conservative check you can ensure that inlining will run away, which by my understanding would be any recursion at all (a loop in the call graph). You could also do a similar analysis for inlineIfReduce but it's a bit harder: for example, I believe this would run away even with inlineIfReduce:

Yes, these are useful improvements, but I will not be implementing them in the near future. For now, we will have to survive with the "function inline stack" error message. I found it very effective.

[digama0]

👍