Totality checker inconsistency when using Inf

[JavierGelatti]

Problem

Sometimes the totality checker validates a function as total when it's not.
In particular, this happens when using Inf in the return type, combined with having the recursive path inside a lambda expression passed to another function.

Steps to reproduce

The following example typechecks:

total
neverReturn : Inf Void
neverReturn = ($) (\_ => neverReturn) ()

This makes it possible to prove Void:

total
boom : Void
boom = Force neverReturn

Additional notes

When Inf is not used as part of the return type of neverReturn, the behavior is correct:

total
neverReturn : Void
-- ^^^^^^^^ Correctly reports error:
-- neverReturn is not total, possibly not terminating due to recursive path Main.neverReturn
neverReturn = ($) (\_ => neverReturn) ()

The same thing happens if we inline $:

total
neverReturn : Inf Void
-- ^^^^^^^^ Correctly reports error:
-- neverReturn is not total, possibly not terminating due to recursive path Main.neverReturn
neverReturn = (\_ => neverReturn) ()

Or if we replace $ with a hole:

total
neverReturn : Inf Void
-- ^^^^^^^^ Correctly reports error:
-- neverReturn is not total, possibly not terminating due to recursive path Main.neverReturn
neverReturn = ?apply_hole (\_ => neverReturn) ()

Or if we use $ with its infix notation:

total
neverReturn : Inf Void
-- ^^^^^^^^ Correctly reports error:
-- neverReturn is not total, possibly not terminating due to recursive path Main.neverReturn
neverReturn = (\_ => neverReturn) $ ()

📝 My Idris version is Idris 2, version 0.7.0-c74f54c12.

[gallais]

I'd say that's a duplicate of #806

[JavierGelatti]

Yeah, sounds like the same thing, plus the way Delay is auto-inserted in this case 🤔

I'm not sure about the actual rules for implicit Delays, but that could explain the differences in the behavior of the examples I included in "Additional notes".