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.