Addition of %tcinline may hang compilation

[buzden]

Steps to Reproduce

Consider the following seemingly equivalent definitions:

%default total

incAll : Stream Nat -> Stream Nat
incAll (x::xs) = S x :: incAll xs

incAll' : Stream Nat -> Stream Nat
incAll' = \(x::xs) => S x :: incAll' xs

Now, add %tcinline to each definition.

Expected Behavior

The same behaviour on both definitions, either successful typechecking (preferrable), or some meaningful error.

Observed Behavior

Addition of %tcinline to the first function typechecks, addition to the second function hangs the compiler taking up all available memory.

Simplified examples also show the same hanging behaviour:

%tcinline
zs : Stream Nat -> Stream Nat
zs xs = Z :: zs xs

%tcinline
zs' : Stream Nat
zs' = Z :: zs'

I suspect that the first function typechecks due to #2737, but this is no more than a guess.

[AntonPing]

I tested these four examples:

%default total

%tcinline
incAll : Stream Nat -> Stream Nat
incAll (x::xs) = S x :: incAll xs

-- %tcinline -- uncomment this, your compiler will hang forever
incAll' : Stream Nat -> Stream Nat
incAll' = \(x::xs) => S x :: incAll' xs

-- %tcinline -- uncomment this, your compiler will hang forever
zs : Stream Nat -> Stream Nat
zs xs = Z :: zs xs

-- %tcinline -- uncomment this, your compiler will hang forever
zs' : Stream Nat
zs' = Z :: zs'

the first one doesn't hang compilation. Other three examples hangs compilation.
The problem seems occured in file Core/Normalise/Eval.idr, and if you change fuel := Nothing to fuel := Just 1000 in Core/Value.idr.

export
tcOnly : EvalOpts
tcOnly = { tcInline := True, fuel := Just 1000 } withArgHoles

The third and fourth examples compile without problem. But the second examples still hangs compilation.
I'm trying to look into it, it seems related to file Core/Termination/CallGraph.idr.

[AntonPing]

I made a fix of it. A pull request is opened: #3257
see the pull request description for the details.