I just sent the email to Ben after reading through his paper, which clarified a lot of confusion. Here’s an related example I found meanwhile - on TR’s checks for function arity in interfaces