Dear all, There is a debate which has been held in our heads for quite some time now. But we’ve never really had the conversation. This debate has been raised again in the context of proposal #281. But I’d rather make a separate thread about it. The question is the following: When I write f @t Am I using @ as a way to change an invisible argument into a visible argument? Or am I using @ to insert a type expression into a term expression? ------------------------------ The truth is that it’s doing both at the same time. So some of us have taken to believing that the One True Meaning™ of @ is to override (in)visibility. While others have taken to believing that the One True Meaning™ of @ is to insert types in term. And, in both cases, we believe the other part to be incidental. In favour of types-in-term, there is the pretty-printer for Core, which, if I’m not mistaken, uses @t to denote type applications (and all type applications are visible in Core, so there is no visibility override to be had). Whatever we think about this, it appears that the fact that this meaning ascription is implicit has caused some anguish. So I think that we should have this discussion explicitly for once. I chose to do so in a different thread than the #281 discussion, because this discussion stands on its own. Anyway, the floor is yours. /Arnaud