Okay, so a pretty common thing that type theory papers do is to add a special case for type checking a curried function saturated with all its arguments. Some examples of this in the literature are:
-
A quick look at impredicativity
In the paper's own words:
Treat applications as a whole: a function applied to a list of arguments
-
Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
This paper adds a special
Γ ⊢ A • e ⇒⇒ C ⊣ ∆judgment whose sole purpose is to type check a function against all of its arguments wholemeal instead of type checking the function piecemeal one argument application at a time:So we view every application as really being a spine consisting of a series of type applications followed by a term application, …
-
Implicit Polarized F: local type inference for impredicativity
This one's probably not as obvious, but the basic idea here is that you now have type signatures of the form
↑(a₀ → a₁ → … ↓r)where the↑denotes where the function's arguments are supposed to begin and the↓denotes where the function's arguments are supposed to end. So you're basically tracking at the type level where the argument list begins and ends. The original paper makes it sound more complicated than it is by making a big deal about "values" vs "computations" but that's really all that it boils down to; type-level tracking of argument lists.
Hell, even my recent post on keyword type checking is also riffing off this same idea (type check curried functions monolithically instead of one argument at a time).
So what you will see as you study the literature is that many type systems use a common trick of type checking curried functions as if they were not curried.