Typesspec

Type Checking: Is This Operation Defined for These Operands?

One expression — `1 + "hello"` — asked of eight languages, with eight answers and four of them from statically checked languages that disagree with each other. The answer is a design decision, not a fact about types.

The question

What is a type checker actually doing when it decides whether 1 + "hello" is allowed?

Source→Lexing→Tokens→Parsing→AST→Semantics→Typed→IR→Optimize→Codegen→Machine code→Link→Execute

What the program is here

The annotated AST from [[annotated-ast]]: every identifier already carries a resolved symbol, and no expression yet carries a type. Checking turns it into a *typed AST* — the same shape, with a type on every expression node and a chosen operator implementation on every application. The question this form answers: for each operator or call, does a typing rule assign it a result type, and if several could, which one was meant?

What this phase may assume or do

The checker may assume [[name-resolution]] has run, so every name has a declaration and every declaration has a written or inferrable type. It may not assume reachability, evaluation order, or any value: an expression in a branch that provably never executes is checked identically to one on the hot path, because the judgment quantifies over all executions and not over the ones that happen.

Key points

Type checking asks one question per node: is there a rule that assigns this application a type, and if several apply, which was meant?
1 + "hello" gets at least four different answers from statically checked languages. The answer is a specification decision, not a consequence of being statically checked.
C and C++ accept 1 + "hello" as pointer arithmetic. The checker was right; the question of whether you meant it was never asked.
Checking is bidirectional: some expressions synthesize their type upward, others are checked against an expectation pushed down. Annotations are expectations to push down.
Coercion is a typing rule firing, not a rule being skipped. The design question is how many implicit conversions exist and whether they compose.
The cost of implicit conversion is that a reader cannot tell what a line does without knowing the whole conversion lattice.
Where the error is reported is a design decision with real cost; the checker that can cite the source of its expectation gives the better message.

One expression, eight answers

specEvery row above is required by the named language’s specification, not observed from one compiler, which is why the label is spec rather than implementation. The C and C++ row has one wrinkle worth knowing: 1 + "hello" is well-defined because the result stays inside the array, but 10 + "hello" computes a pointer more than one past the end and is undefined behaviour — see [[undefined-behavior]]. The type checker accepts both identically; the difference is not expressible in the type system. Clang emits -Wstring-plus-int for the first form as a courtesy, which is a diagnostic the standard does not require and which GCC does not produce.

1 + "hello" is the standard example, and the standard telling of it is wrong twice. It is usually presented as “dynamic languages fail at runtime, static languages fail at compile time”. Neither half survives contact with a compiler.

What + means for an integer and a string is a decision each language made separately, written into its specification, and the decisions do not line up with the static/dynamic split at all. Java and C# are statically checked and concatenate. Go and Rust are statically checked and reject. TypeScript is statically checked and — deliberately, to model the JavaScript it compiles to — concatenates. C and C++ accept the expression and do something that has nothing to do with either: "hello" is an array that decays to a pointer, so 1 + "hello" is pointer arithmetic, and its value is a pointer to the e.

That last one is worth sitting with, because it is the sharpest available illustration of what a type checker is and is not. The C++ checker did its job perfectly. There *is* a rule for int + const char*, the rule assigns the result type const char*, the derivation exists, and the program is well-typed. Whether the programmer meant it is not a question a type system was ever asked.

What each language answers, and the rule that decided itspec

Language	Result of `1 + "hello"`	Decided when	The rule responsible
Python 3spec	`TypeError: unsupported operand type(s) for +: 'int' and 'str'`	When the line executes	`int.__add__` returns NotImplemented, `str.__radd__` does not exist, so the data model requires `TypeError`
Rubyspec	`TypeError: String can't be coerced into Integer`	When the line executes	`Integer#+` calls `coerce` on its argument; `String` does not define it
JavaScriptspec	`"1hello"`	When the line executes, with no error	ApplyStringOrNumericBinaryOperator: if either primitive is a String, both are coerced to String and concatenated
TypeScriptspec	`"1hello"`, statically typed as `string`. No error.	At check time — as an acceptance	The `+` rule is written to model JavaScript: if either operand is `string`, the result is `string`. `1 - "hello"` is an error (TS2363)
Javaspec	`"1hello"`, statically typed as `String`	At compile time — as an acceptance	JLS 15.18.1: if either operand is of type `String`, `+` is string concatenation and the other operand is converted
C#spec	`"1hello"`	At compile time — as an acceptance	The `string operator +(object, string)` overload applies after boxing the `int`
C and C++spec	A `const char*` pointing at the `e`. Compiles; no diagnostic is required, though Clang offers `-Wstring-plus-int`.	At compile time — as an acceptance	Array-to-pointer decay makes `"hello"` a `const char*`; `int + pointer` is ordinary pointer arithmetic
C++ with `std::string`spec	`1 + std::string("hello")` — compile error: no matching `operator+`	At compile time — as a rejection	Overload resolution finds no viable candidate for `(int, std::string)`
Gospec	`invalid operation: mismatched types untyped int and untyped string`	At compile time — as a rejection	Binary operands must be of identical type, and no implicit conversion exists
Rustspec	`error[E0277]: cannot add` &str `to` {integer}``	At compile time — as a rejection	No `impl Add<&str> for i32` exists, so the trait bound is unsatisfied — see `[[ad-hoc-polymorphism]]`

Two directions, not one

The naive picture of checking is a single bottom-up pass: compute each child’s type, look up a rule, produce the parent’s type. That is *synthesis*, and it is half the algorithm. It works for 1 + 2 and fails immediately for an empty list literal, a lambda without parameter annotations, an overloaded call, or a numeric literal that could be any of six widths.

The other half is *checking*: the parent already knows what type it wants and pushes that expectation down. let xs: Vec<i64> = vec![] synthesizes nothing from vec![]; it checks vec![] against the expected Vec<i64> and succeeds. Modern checkers are explicitly bidirectional — every expression form is classified as one the checker synthesizes from or one it checks against, and the two modes alternate down the tree.

This is not academic tidiness. It is why annotations work where they work: an annotation is an expectation to push down, and the places a language demands one are exactly the places its rules cannot synthesize. It is also why moving a type annotation from a variable to a function parameter sometimes fixes an error and sometimes does nothing — you changed which direction the information flows.

The two modes, and where each is used

SYNTHESIS   Γ ⊢ e ⇒ T      "from e, work out T"
            literals, variables, applications of known functions,
            annotated expressions

CHECKING    Γ ⊢ e ⇐ T      "given T, verify e fits"
            lambdas, empty collections, `null`, numeric literals,
            struct literals with inferred field types

The bridge rule, used when a checked position holds a
synthesizable expression:

        Γ ⊢ e ⇒ S       S <: T
        ──────────────────────
             Γ ⊢ e ⇐ T

Read: to check e against T, synthesize its type S and
require that S be usable where a T was wanted — which is
the subsumption step of `[[subtyping]]`.

Coercion is a typing rule, not the absence of one

When a language accepts 1 + "hello" and produces "1hello", nothing was skipped. A rule fired that says: given int and String, convert the int and concatenate. The rule is in the specification, the checker applied it, and the derivation is complete. Coercion is not the type system being lax; it is the type system having a different rule than you expected.

Which is why the interesting question about any language is not “does it coerce” but how many implicit conversions does it have, and do they compose. C++ has integral promotion, integral conversion, floating-point conversion, pointer conversion, boolean conversion, user-defined conversion operators and converting constructors, and overload resolution ranks sequences of them — which is how a call ends up selecting a candidate nobody expected. Go has almost none, deliberately, which is why int and int64 will not add and everybody complains for a week and then stops.

The cost of implicit conversion is not correctness in the small; it is that the reader cannot determine what a line does locally. f(x) in a language with user-defined conversions may construct a temporary, call a conversion operator, and select a different overload than the one on the line above, all invisibly. That readability cost is the real bill, and it is paid by everyone who reads the code, forever, in exchange for convenience paid once by whoever wrote it.

Deleting a “redundant” cast

Before

process(static_cast<long>(count));

After

process(count);

Legal only when

Only if exactly one process overload is viable both before and after the change, and it is the same one. When count is already long, or process has a single parameter type that count converts to unambiguously, the cast contributed nothing and removing it preserves the selected callee and therefore the behavior.

Illegal when

When the cast was doing overload resolution: with process(int) and process(long) both declared and count an int, the cast selects the long overload and removing it selects the int one — a different function, silently, with no diagnostic. The same trap exists in Java with remove(int) versus remove(Object) on List, where an unhelpful cast changes “remove at index” into “remove this value”.

Which node gets blamed

implementationDiagnostic behaviour is the least standardised part of any checker and changes between releases. Rust’s E0277 output, Clang’s overload-candidate listing and TypeScript’s “Type X is not assignable to type Y” chains all improved substantially over the 2018–2025 period, and the same program produces materially different messages across versions of the same compiler. Never memorise a message; memorise which node the checker chose to blame and why.

A checker that finds no applicable rule has to report *somewhere*, and the somewhere is a genuine design problem rather than a formatting detail. The naive answer — blame the node where the rule failed — is frequently the wrong line. In f(g(x)) with a mismatch, the failure surfaces at the call to f, while the mistake was in g’s return type three files away.

Bidirectional checking helps here in a way that pure inference does not: because an expectation was pushed down from an annotation, the checker can report at the leaf and cite the annotation as the source of the expectation. “Expected string because of the annotation on line 4, found number here.” Whole-program inference has no annotation to cite, which is the root of the error-quality problem discussed in [[type-inference]] and [[unification]].

The practical craft is covered by [[diagnostic-quality]], and it comes down to three things a good checker does: report the *expected* type and where the expectation came from, report the *found* type at the narrowest span that produced it, and stop cascading — one root cause should not print nine errors. A checker that reports every downstream node whose type became unknown has turned one mistake into a wall of text.

Errors are better when the checker can name the source of its expectation, which is a direct argument for annotating public boundaries.
Error recovery in a type checker means assigning a poison or error type and continuing, so one mistake yields one message rather than a cascade — the same discipline as [[error-recovery]] in a parser.
A checker that ranks candidate overloads should say *why each candidate failed*, not just “no matching function”. The C++ and Rust toolchains both learned this the expensive way.
Blame in a gradual system is a further problem: when a check fails at a typed/untyped boundary, which side is at fault? Blame tracking is the answer, and most production gradual systems do not implement it — see [[gradual-typing]].

How it works

The steps, in the order the compiler takes them.

Walk the annotated AST. At each node, decide from the node’s form whether to synthesize a type or check against one pushed down from the parent.
For a literal, synthesize the literal’s type — or, in languages with polymorphic literals, a fresh type variable with a constraint ([[unification]]).
For a variable, look the name up in the environment and return its type — the environment being the [[type-environment]], backed by the same table as [[symbol-table]].
For an operator application, gather the operand types, then look for a rule or an overload candidate: exact match first, then match through the language’s permitted implicit conversions, ranked.
If exactly one candidate is best, record the result type and the chosen implementation on the node. If several tie, report ambiguity; if none apply, report a mismatch.
Insert any coercion the rule required as an explicit node in the tree, so that lowering emits the conversion rather than rediscovering it.
On failure, assign the node an error type that is compatible with everything, so that checking continues without cascading.

How it breaks

What the engineer observes when it goes wrong — not what goes wrong internally.

The program compiles and does something unrelated to what was written: 1 + "hello" in C++ yields a pointer into a string literal, and the value flows onward as a plausible-looking const char*.
A cast added to silence a warning changes which overload is selected, and a different function runs with no diagnostic anywhere.
One genuine mistake produces forty errors, because the checker propagated an unknown type instead of poisoning the node, and the real message is number thirty-one.
The error is reported in a file the engineer has never opened, because the mismatch surfaced at a call site rather than at the definition whose type changed.
An implicit numeric conversion silently narrows a value — long to int, i64 to i32, number to a 32-bit bitwise operation — and a large value wraps three layers away from the conversion.
A checker accepts a JSON-derived value as a domain type because a deserializer was typed any or interface{}, and every rule downstream fired on a promise nobody kept.

When it helps

Reading an unfamiliar language’s surprising behaviour: find the operator’s rule in the specification rather than reasoning from “static” or “dynamic”, which predicts nothing here.
Deciding whether to add an implicit conversion to a DSL or config language. The rule is easy to write and the readability cost lands on everyone afterwards.
Debugging an overload-resolution surprise: the question is always which candidates were viable and how their conversion sequences ranked, and both toolchains will tell you if asked.
Designing error messages for a checker or validator of your own, where “expected X because of Y, found Z here” is the whole difference between a usable and unusable tool.

When it hurts

Reasoning about *values* from the checker’s conclusions. The checker proved a rule applies; it did not prove the number is in range, the string is a valid URL, or the index is inside the array.
Assuming the checker’s acceptance means the author’s intent was captured. Every row in the matrix above is a case where the derivation exists and the intent may not.
Treating type checking as the place to enforce business rules. Encoding “an order must have at least one line” in the type system is possible in a few languages and expensive in all of them.

What it costs

Every one of these is paid by something.

Rich implicit conversion buys concise call sites and pays in readability for every later reader, plus overload-resolution rules complex enough that the language specification needs pages for them and users still get surprises.
Rejecting all implicit conversion (Go’s position) buys local readability and pays in explicit conversion noise on every numeric boundary, which pushes some programmers toward a single width and some toward casts that hide real narrowing.
Bidirectional checking buys much better error messages and the ability to type lambdas and empty literals, and pays in a checker that must classify every expression form into two modes and keep them consistent as the language grows.
Error recovery via poison types buys a full list of independent errors in one run, and pays in false negatives: a poisoned node accepts everything, so a real second error inside it goes unreported until the first is fixed.

What else you could do

What a different compiler or language does instead, and when that is better.

Check nothing statically and dispatch on value tags at runtime, reporting the mismatch when it occurs. This is not weaker checking, only later checking — see [[static-vs-dynamic-typing]].
Check by unification and constraint solving rather than by rule lookup, which is what [[hindley-milner]] does and what removes the annotation burden at the cost of blame quality.
Check with an external tool over an unannotated language — a soft-typing analyser or a dialyzer-style success-typing system, which reports only definite errors and stays silent where it cannot decide.
Push the check to a schema at the boundary and leave the interior unchecked, which is what most services actually do regardless of language, and which fails differently: earlier for the data, not at all for the code.

See it for yourself

The flag, dump or tool that shows you this directly.

clang -Xclang -ast-dump file.cpp prints the AST with a type on every expression node and shows exactly where an ImplicitCastExpr was inserted — the coercions the checker added are visible as tree nodes.
For overload surprises: clang++ -fdiagnostics-show-template-tree and, more bluntly, deleting candidates one at a time until the error changes.
tsc --noEmit with --strict, then hover in an editor: the reported type of 1 + "hello" is string, which is the fastest way to convince someone the matrix above is real.
go vet and go build on the same expression, plus gotype-style checking through go/types if you want the checker’s own view programmatically.
rustc --explain E0277 for the trait-bound form of the same rejection, which spells out that the language has no rule rather than that the types are “wrong”.
Compiler Explorer with all of C++, Rust, Go and TypeScript open on the same expression — the fastest possible demonstration that the answer is a language decision.

Plausible wrong readings

Stated the way a confident engineer states them.

“Statically typed languages reject 1 + "hello".” Java, C#, TypeScript, C and C++ all accept it, three of them by concatenating and two by doing pointer arithmetic. The split is per-language, not per-category.
“TypeScript catches 1 + "hello".” It types it as string on purpose, to match the JavaScript it emits. It catches 1 - "hello", which is a different rule.
“A coercion means the type system gave up.” A rule fired. Read the rule; the specification will name it.
“The compiler accepted it, so it means what I intended.” It means a derivation exists. The C++ pointer-arithmetic case is the cleanest demonstration that those are different claims.
“Adding a cast is harmless if it compiles.” A cast is an input to overload resolution. It can change which function runs, with no warning.

Misconceptions

The claim, and what is actually true.

A type error means the types are wrong.

It means no rule applies. Whether the types are “wrong” is a judgment about intent that the checker has no access to — and in the C++ pointer case, a rule applies to something clearly unintended.

Implicit conversions are a legacy mistake.

They are a deliberate ergonomics-for-locality trade. Numeric promotion in C++ makes mixed-width arithmetic writable; Go’s refusal makes every line readable. Both positions are defended in their language’s design rationale.

The checker runs after parsing and before anything else, in one pass.

Real checkers interleave with [[name-resolution]], may run several passes for mutual recursion ([[declaration-order]]), and in languages with [[compile-time-evaluation]] may need to *run* code mid-check to decide a type.

More compile errors means a stricter type system.

It may mean worse cascading. One mistake producing forty messages is a diagnostics failure, and the fix is poison types, not a weaker system.

Go deeper

The same idea at increasing depth. Stop wherever it stops being useful.

overview

A type checker walks the tree and asks, at each operation, whether the language has a rule for these operand types. If it does, the node gets the rule’s result type. If it does not, that is a type error. The surprising part is how much the rules differ: 1 + "hello" is a runtime error in Python, a string in JavaScript, Java, C# and TypeScript, a compile error in Go and Rust, and pointer arithmetic in C and C++. Every one of those is required by that language’s specification. There is no universal answer to hold in your head — only the habit of asking which rule fired.

practical

Two habits pay for themselves. First, when a checker surprises you, find the rule rather than arguing with the tool; every mainstream language specifies its operator behaviour precisely, and rustc --explain, the JLS index and the C++ overload-resolution rules will all tell you what happened. Second, be suspicious of casts. A cast is not a comment addressed to the compiler — it is an input to overload resolution and to conversion ranking, and adding or deleting one can change which function is called. If a cast is required to make code compile, write down why in a comment; if you cannot say why, the cast is hiding a real mismatch that will surface later as a narrowed value or the wrong callee.

advanced

The design tension in checking is between syntax-directedness and expressiveness. A syntax-directed rule set — at most one rule per expression form — gives a linear, deterministic algorithm and clean errors. Subsumption ([[subtyping]]) and overloading ([[ad-hoc-polymorphism]]) both break it: the first because it applies to every expression, the second because several candidates may apply. Real checkers recover determinism by restricting where the non-directed rules may fire, which is exactly what bidirectional typing is for: subsumption is permitted only at the synthesis-to-checking bridge, and overload resolution is permitted only at application nodes with a ranking function to break ties. Once you see checking as “restore syntax-directedness by construction”, the odd rules in every language’s specification — where a lambda needs an annotation, why generic inference on an overloaded call is fragile, why C++ has a two-phase name lookup — stop being arbitrary.

How much this depends on

Nothing in this domain is true of every compiler. These say how much.

specJava’s string-concatenation rule for + is JLS 15.18.1, and it applies at compile time based on the *static* type of the operands, which is why Object o = "x"; 1 + o does not concatenate. C#’s behaviour comes from an overload on object, so it does box. Two statically checked languages, similar surface behaviour, different mechanisms — and the difference shows up as soon as a variable is declared with a supertype.

specIn C and C++, a string literal has array type and decays to a pointer, so 1 + "hello" is pointer arithmetic with a well-defined result. This is required by the standards, not a compiler quirk. 10 + "hello" is undefined behaviour because it forms a pointer more than one past the end; the type checker cannot distinguish the two cases, so no diagnostic is required for either.

specTypeScript’s + rule deliberately mirrors ECMAScript: a string operand makes the result string. This is a design decision recorded in the TypeScript specification-in-practice and preserved across the 1.x–5.x line precisely so that typed code and the JavaScript it emits agree. Arithmetic operators other than + require numeric operands and do error.

implementationWhere a checker chooses to report an error, how many errors it cascades, and how it ranks overload candidates are implementation decisions that change between releases of the same compiler. The mechanism described here — poison types to stop cascades, expectation provenance for better messages — is what mainstream checkers converged on, not something any specification requires.

If you were asked this in an interview

What does 1 + "hello" do in C++? Why is that not a type error?
Name two statically checked languages that disagree about 1 + "hello", and explain what that tells you about the static/dynamic framing.
What is bidirectional type checking, and which expression forms force you into it?
You add a cast to fix a compile error and the program starts behaving differently. What class of bug is that?

Connections

Computer Architectureinteger-overflow signed-integers

API Designvalidation-errors

Backendbusiness-validation transport-validation

Domains that do not exist yet

Programming Languages & Runtime Internals — How a dynamic language dispatches an operator on value tags
The Python and JavaScript rows of the matrix are decided by the runtime’s dispatch protocol — __add__/__radd__, ToPrimitive — which is the runtime’s subject. This lesson needs only the observable answer and the rule that requires it.

Runtime gain2

Compile cost2

Debuggability4

Implementation3

Context dependence5

Checking itself is cheap in a rule-lookup design — roughly one pass over the tree — and becomes expensive only when overload resolution or constraint solving is involved. Context dependence is maximal: this lesson exists largely to demonstrate that the same expression has different, specification-mandated answers in different languages, so nothing here transfers without checking the spec.